subsingleton_of_isInitial — Mathlib

English

If X is initial, then Subobject X is a subsingleton.

Русский

Если X является начальным, то Subobject X является подподобъектом-одиночного класса.

LaTeX

$$IsInitial X → Subsingleton (Subobject X)$$

Lean4

theorem subsingleton_of_isInitial {X : C} (hX : IsInitial X) : Subsingleton (Subobject X) :=
  by
  suffices ∀ (S : Subobject X), S = .mk (𝟙 _) from ⟨by simp [this]⟩
  intro S
  obtain ⟨A, i, _, rfl⟩ := S.mk_surjective
  have fac : hX.to A ≫ i = 𝟙 X := hX.hom_ext _ _
  let e : A ≅ X :=
    { hom := i
      inv := hX.to A
      hom_inv_id := by rw [← cancel_mono i, assoc, fac, id_comp, comp_id]
      inv_hom_id := fac }
  exact mk_eq_mk_of_comm i (𝟙 X) e (by simp [e])

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