hasStrictTerminalObjects_of_terminal_is_strict

English

If there exists a strict terminal object I such that every morphism f: I ⟶ A is an isomorphism, then C has strict terminal objects.

Русский

Если существует строгий терминальный объект I, такой что каждый морфизм f: I ⟶ A является изоморфизмом, тогда в C существуют строгие терминальные объекты.

LaTeX

$$$(\\forall A, f: I \\to A, IsIso f) \\Rightarrow HasStrictTerminalObjects C$$$

Lean4

/-- If `C` has an object such that every morphism *from* it is an isomorphism, then `C`
has strict terminal objects. -/
theorem hasStrictTerminalObjects_of_terminal_is_strict (I : C) (h : ∀ (A) (f : I ⟶ A), IsIso f) :
    HasStrictTerminalObjects C :=
  {
    out := fun {I' A} f hI' =>
      haveI := h A (hI'.from _ ≫ f)
      ⟨⟨inv (hI'.from I ≫ f) ≫ hI'.from I, hI'.hom_ext _ _, by rw [assoc, IsIso.inv_hom_id]⟩⟩ }

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