The category of cyclic rings
Content created by Egbert Rijke, Fredrik Bakke and Gregor Perčič.
Created on 2023-09-21.
Last modified on 2023-11-27.
module ring-theory.category-of-cyclic-rings where
Imports
open import category-theory.categories open import category-theory.isomorphisms-in-large-precategories open import category-theory.large-categories open import category-theory.large-precategories open import foundation.fundamental-theorem-of-identity-types open import foundation.subtype-identity-principle open import foundation.universe-levels open import order-theory.large-posets open import ring-theory.cyclic-rings open import ring-theory.homomorphisms-cyclic-rings open import ring-theory.isomorphisms-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 large precategory of cyclic rings
Cyclic-Ring-Large-Precategory : Large-Precategory lsuc _⊔_ obj-Large-Precategory Cyclic-Ring-Large-Precategory = Cyclic-Ring hom-set-Large-Precategory Cyclic-Ring-Large-Precategory = hom-set-Cyclic-Ring comp-hom-Large-Precategory Cyclic-Ring-Large-Precategory {X = R} {Y = S} {Z = T} = comp-hom-Cyclic-Ring R S T id-hom-Large-Precategory Cyclic-Ring-Large-Precategory {X = R} = id-hom-Cyclic-Ring R associative-comp-hom-Large-Precategory Cyclic-Ring-Large-Precategory {X = R} {Y = S} {Z = T} {W = U} = associative-comp-hom-Cyclic-Ring R S T U inv-associative-comp-hom-Large-Precategory Cyclic-Ring-Large-Precategory {X = R} {Y = S} {Z = T} {W = U} = inv-associative-comp-hom-Cyclic-Ring R S T U left-unit-law-comp-hom-Large-Precategory Cyclic-Ring-Large-Precategory {X = R} {Y = S} = left-unit-law-comp-hom-Cyclic-Ring R S right-unit-law-comp-hom-Large-Precategory Cyclic-Ring-Large-Precategory {X = R} {Y = S} = right-unit-law-comp-hom-Cyclic-Ring R S
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 R = fundamental-theorem-id ( is-torsorial-Eq-subtype ( is-torsorial-iso-Ring (ring-Cyclic-Ring R)) ( is-prop-is-cyclic-Ring) ( ring-Cyclic-Ring R) ( id-iso-Ring (ring-Cyclic-Ring R)) ( is-cyclic-Cyclic-Ring R)) ( iso-eq-Large-Precategory Cyclic-Ring-Large-Precategory R) 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
See also
Table of files related to cyclic types, groups, and rings
Recent changes
- 2023-11-27. Fredrik Bakke. Refactor categories to carry a bidirectional witness of associativity (#945).
- 2023-10-21. Egbert Rijke. Rename
is-contr-totaltois-torsorial(#871). - 2023-10-09. Egbert Rijke. Navigation tables for all files related to cyclic types, groups, and rings (#823).
- 2023-09-26. Fredrik Bakke and Egbert Rijke. Maps of categories, functor categories, and small subprecategories (#794).
- 2023-09-21. Egbert Rijke and Gregor Perčič. The classification of cyclic rings (#757).