This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.
The category of commutative rings
module commutative-algebra.category-of-commutative-rings where
Imports
open import category-theory.categories open import category-theory.large-categories open import commutative-algebra.isomorphisms-commutative-rings open import commutative-algebra.precategory-of-commutative-rings open import foundation.universe-levels
Idea
The large category
Commutative-Ring-Category of
commutative rings is the large
category consistsing of commutative rings and
ring homomorphisms.
Definitions
The large category of commutative rings
is-large-category-Commutative-Ring-Large-Category : is-large-category-Large-Precategory Commutative-Ring-Large-Precategory is-large-category-Commutative-Ring-Large-Category = is-equiv-iso-eq-Commutative-Ring Commutative-Ring-Large-Category : Large-Category lsuc (_⊔_) large-precategory-Large-Category Commutative-Ring-Large-Category = Commutative-Ring-Large-Precategory is-large-category-Large-Category Commutative-Ring-Large-Category = is-large-category-Commutative-Ring-Large-Category
The small categories of commutative rings
Commutative-Ring-Category : (l : Level) → Category (lsuc l) l Commutative-Ring-Category = category-Large-Category Commutative-Ring-Large-Category