isTerminalΩ₀ — Mathlib

English

The main nontrivial result: h.Ω₀ is a terminal object.

Русский

Главный нетривиальный результат: h.Ω₀ является терминальным объектом.

LaTeX

$$IsTerminal (h.Ω₀)$$

Lean4

/-- The main non-trivial result: `h.Ω₀` is actually a terminal object. -/
noncomputable def isTerminalΩ₀ : IsTerminal (h.Ω₀ : C) :=
  IsTerminal.ofUniqueHom (fun X ↦ h.π (𝟙 X))
    (fun X π' ↦
      by
      have : IsPullback (𝟙 X) π' (π' ≫ h.Ω₀.arrow) h.Ω₀.arrow :=
        {
          isLimit' :=
            ⟨PullbackCone.IsLimit.mk _ (fun s ↦ s.fst) (by simp)
                (fun s ↦ by rw [← cancel_mono h.Ω₀.arrow, ← s.condition, Category.assoc])
                (fun s m hm _ ↦ by simpa using hm)⟩ }
      rw [← cancel_mono h.Ω₀.arrow, h.uniq this, ← (h.isPullback (𝟙 X)).w, Category.id_comp])

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