hasStrictInitialObjects_of_initial_is_strict

English

If there exists an initial object I such that every morphism f: A → ⊥_C is an isomorphism, then C has strict initial objects.

Русский

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

LaTeX

$$$(\\forall A, f: A \\to \\bot_C, IsIso f) \\Rightarrow HasStrictInitialObjects C$$$

Lean4

/-- If `C` has an initial object such that every morphism *to* it is an isomorphism, then `C`
has strict initial objects. -/
theorem hasStrictInitialObjects_of_initial_is_strict [HasInitial C] (h : ∀ (A) (f : A ⟶ ⊥_ C), IsIso f) :
    HasStrictInitialObjects C :=
  {
    out := fun {I A} f hI =>
      haveI := h A (f ≫ hI.to _)
      ⟨⟨hI.to _ ≫ inv (f ≫ hI.to (⊥_ C)), by rw [← assoc, IsIso.hom_inv_id], hI.hom_ext _ _⟩⟩ }

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