isInitial

Mathlib.Algebra.Category.Ring.Constructions

URI: https://scilib.ai/kg/mathlib#CommRingCat.isInitial

Lean4

/-- `ULift.{u} ℤ` is initial in `CommRingCat`. -/
def isInitial : IsInitial (CommRingCat.of (ULift.{u} ℤ)) :=
  IsInitial.ofUnique (h := fun R ↦
    ⟨⟨ofHom <| (Int.castRingHom R).comp ULift.ringEquiv.toRingHom⟩, fun _ ↦
      by
      ext : 1
      rw [←
        RingHom.cancel_right (f := (ULift.ringEquiv.{0, u} (R := ℤ)).symm.toRingHom) (hf :=
          ULift.ringEquiv.symm.surjective)]
      apply RingHom.ext_int⟩)

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru