The category of rings
Content created by Egbert Rijke and Fredrik Bakke.
Created on 2023-09-11.
Last modified on 2024-10-05.
module ring-theory.category-of-rings where
Imports
open import category-theory.categories open import category-theory.large-categories open import foundation.universe-levels open import ring-theory.isomorphisms-rings open import ring-theory.precategory-of-rings
Idea
The large category Ring-Category of
rings is the large category consisting of rings and
ring homomorphisms.
Definitions
The large category of rings
is-large-category-Ring-Large-Category : is-large-category-Large-Precategory Ring-Large-Precategory is-large-category-Ring-Large-Category = is-equiv-iso-eq-Ring Ring-Large-Category : Large-Category lsuc (_⊔_) large-precategory-Large-Category Ring-Large-Category = Ring-Large-Precategory is-large-category-Large-Category Ring-Large-Category = is-large-category-Ring-Large-Category
The small categories of rings
Ring-Category : (l : Level) → Category (lsuc l) l Ring-Category = category-Large-Category Ring-Large-Category
Recent changes
- 2024-10-05. Fredrik Bakke. chore: a few typos in algebra (#1187).
- 2024-03-11. Fredrik Bakke. Refactor category theory to use strictly involutive identity types (#1052).
- 2023-09-12. Egbert Rijke. Beyond foundation (#751).
- 2023-09-11. Egbert Rijke. The categories of rings and commutative rings (#750).