The precategory of rings
Content created by Egbert Rijke and Fredrik Bakke.
Created on 2023-05-06.
Last modified on 2023-09-26.
module ring-theory.precategory-of-rings where
Imports
open import category-theory.large-precategories open import category-theory.precategories open import foundation.universe-levels open import ring-theory.homomorphisms-rings open import ring-theory.rings
Idea
The (large) precategory of rings consists of rings and ring homomorphisms.
Definitions
The large precategory of rings
Ring-Large-Precategory : Large-Precategory lsuc _⊔_ obj-Large-Precategory Ring-Large-Precategory = Ring hom-set-Large-Precategory Ring-Large-Precategory = hom-set-Ring comp-hom-Large-Precategory Ring-Large-Precategory {X = R} {S} {T} = comp-hom-Ring R S T id-hom-Large-Precategory Ring-Large-Precategory {X = R} = id-hom-Ring R associative-comp-hom-Large-Precategory Ring-Large-Precategory {X = R} {S} {T} {U} = associative-comp-hom-Ring R S T U left-unit-law-comp-hom-Large-Precategory Ring-Large-Precategory {X = R} {S} = left-unit-law-comp-hom-Ring R S right-unit-law-comp-hom-Large-Precategory Ring-Large-Precategory {X = R} {S} = right-unit-law-comp-hom-Ring R S
The precategory or rings of universe level l
Ring-Precategory : (l : Level) → Precategory (lsuc l) l Ring-Precategory = precategory-Large-Precategory Ring-Large-Precategory
Recent changes
- 2023-09-26. Fredrik Bakke and Egbert Rijke. Maps of categories, functor categories, and small subprecategories (#794).
- 2023-09-10. Egbert Rijke and Fredrik Bakke. Cyclic groups (#723).
- 2023-05-13. Fredrik Bakke. Remove unused imports and fix some unaddressed comments (#621).
- 2023-05-06. Egbert Rijke. Collecting some easily defined precategories (#598).