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