The precategory of rings

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-05-06.
Last modified on 2024-09-23.

module ring-theory.precategory-of-rings where

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) (_⊔_)
Ring-Large-Precategory =
  make-Large-Precategory
    ( Ring)
    ( hom-set-Ring)
    ( λ {l1} {l2} {l3} {R} {S} {T} → comp-hom-Ring R S T)
    ( λ {l} {R} → id-hom-Ring R)
    ( λ {l1} {l2} {l3} {l4} {R} {S} {T} {U} → associative-comp-hom-Ring R S T U)
    ( λ {l1} {l2} {R} {S} → left-unit-law-comp-hom-Ring R S)
    ( λ {l1} {l2} {R} {S} → right-unit-law-comp-hom-Ring R S)

The precategory of rings at a universe level

Ring-Precategory : (l : Level) → Precategory (lsuc l) l
Ring-Precategory = precategory-Large-Precategory Ring-Large-Precategory

Recent changes

• 2024-09-23. Fredrik Bakke. Some typos, wording improvements, and brief prose additions (#1186).
• 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-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).