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 cyclic rings
module ring-theory.category-of-cyclic-rings where
Imports
open import category-theory.categories open import category-theory.full-large-subprecategories open import category-theory.large-categories open import category-theory.large-precategories open import foundation.universe-levels open import order-theory.large-posets open import ring-theory.category-of-rings open import ring-theory.cyclic-rings open import ring-theory.homomorphisms-cyclic-rings open import ring-theory.precategory-of-rings
Idea
The large category of cyclic rings¶ is the large category consisting of cyclic rings and ring homomorphisms.
Note that we already showed that there is at most one ring homomorphism between
any two cyclic rings, so it follows that the large category of cyclic rings is
in fact a large poset. The large poset of cyclic
rings is constructed in the file
ring-theory.poset-of-cyclic-rings.
Definition
The precategory of cyclic rings as a full subprecategory of the precategory of rings
Cyclic-Ring-Full-Large-Subprecategory : Full-Large-Subprecategory (λ l → l) Ring-Large-Precategory Cyclic-Ring-Full-Large-Subprecategory = is-cyclic-prop-Ring
The large precategory of cyclic rings
Cyclic-Ring-Large-Precategory : Large-Precategory lsuc (_⊔_) Cyclic-Ring-Large-Precategory = large-precategory-Full-Large-Subprecategory ( Ring-Large-Precategory) ( Cyclic-Ring-Full-Large-Subprecategory)
The large category of cyclic rings
abstract is-large-category-Cyclic-Ring-Large-Category : is-large-category-Large-Precategory Cyclic-Ring-Large-Precategory is-large-category-Cyclic-Ring-Large-Category = is-large-category-large-precategory-is-large-category-Full-Large-Subprecategory ( Ring-Large-Precategory) ( Cyclic-Ring-Full-Large-Subprecategory) ( is-large-category-Ring-Large-Category) Cyclic-Ring-Large-Category : Large-Category lsuc (_⊔_) large-precategory-Large-Category Cyclic-Ring-Large-Category = Cyclic-Ring-Large-Precategory is-large-category-Large-Category Cyclic-Ring-Large-Category = is-large-category-Cyclic-Ring-Large-Category
The small categories of cyclic rings
Cyclic-Ring-Category : (l : Level) → Category (lsuc l) l Cyclic-Ring-Category = category-Large-Category Cyclic-Ring-Large-Category
Properties
The large category of cyclic rings is a large poset
is-large-poset-Cyclic-Ring-Large-Category : is-large-poset-Large-Category Cyclic-Ring-Large-Category is-large-poset-Cyclic-Ring-Large-Category = is-prop-hom-Cyclic-Ring