Initial rings

Content created by Egbert Rijke, Fredrik Bakke and Gregor Perčič.

Created on 2023-09-21.
Last modified on 2023-09-26.

module ring-theory.initial-rings where

open import category-theory.initial-objects-large-categories

open import foundation.universe-levels

open import ring-theory.category-of-rings
open import ring-theory.rings

Idea

The initial ring is a ring R that satisfies the universal property that for any ring S, the type

  hom-Ring R S

of ring homomorphisms from R to S is contractible.

In elementary-number-theory.ring-of-integers we will show that ℤ is the initial ring.

Definitions

module _
  {l : Level} (R : Ring l)
  where

  is-initial-Ring : UUω
  is-initial-Ring = is-initial-obj-Large-Category Ring-Large-Category R

Recent changes

• 2023-09-26. Fredrik Bakke and Egbert Rijke. Maps of categories, functor categories, and small subprecategories (#794).
• 2023-09-21. Egbert Rijke and Gregor Perčič. The classification of cyclic rings (#757).