The category of cyclic rings
Content created by Egbert Rijke, Fredrik Bakke and Gregor Perčič.
Created on 2023-09-21.
Last modified on 2024-03-11.
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
See also
Table of files related to cyclic types, groups, and rings
Recent changes
- 2024-03-11. Fredrik Bakke. Refactor category theory to use strictly involutive identity types (#1052).
- 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).