zIsInitial — Mathlib

English

Let R be any commutative ring. There exists a unique ring homomorphism from the integers ℤ to R, and this universal property characterizes ℤ as the initial object in the category of commutative rings.

Русский

Пусть R — произвольное коммутативное кольцо. Существует единственный кольцевой гомоморфизм ℤ в R; это свойство характеризует ℤ как начальный объект в категории коммутативных колец.

LaTeX

$$$\\forall R \\;\\text{(CommRing)}\\,\\exists!\\ f: \\mathbb{Z} \\to R,\\ f \\text{ is a ring hom}$$$

Lean4

/-- `ℤ` is the initial object of `CommRingCat`. -/
def zIsInitial : IsInitial (CommRingCat.of ℤ) :=
  IsInitial.ofUnique (h := fun R => ⟨⟨ofHom <| Int.castRingHom R⟩, fun a => hom_ext <| a.hom.ext_int _⟩)

Похожие утверждения