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


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.


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

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

Recent changes