English
The category CommRingCat has a strict terminal object; specifically, the terminal object can be realized via the unit type PUnit with a unique morphism from any object commuting as a strict terminal, as shown by a construction using PUnit.
Русский
У категории CommRingCat существует строгий терминальный объект; он реализован через единичный тип PUnit и уникальные морфизмы из любого объекта.
LaTeX
$$$\exists X:\text{CommRingCat} \, IsTerminal X \, \text{and } X \text{ is strict}$$$
Lean4
instance commRingCat_hasStrictTerminalObjects : HasStrictTerminalObjects CommRingCat.{u} :=
by
apply hasStrictTerminalObjects_of_terminal_is_strict (CommRingCat.of PUnit)
intro X f
refine ⟨ofHom ⟨1, rfl, by simp⟩, ?_, ?_⟩
· ext
· ext x
have e : (0 : X) = 1 := by rw [← f.hom.map_one, ← f.hom.map_zero]
replace e : 0 * x = 1 * x := congr_arg (· * x) e
rw [one_mul, zero_mul, ← f.hom.map_zero] at e
exact e
