isInitialIffObj — Mathlib

English

An equivalence between IsInitial X and IsInitial (G.obj X) when G preserves and reflects the empty diagram.

Русский

Эквивалентность IsInitial X и IsInitial(G.obj X) при сохранении/отражении пустого диаграммного предела.

LaTeX

$$$\\text{IsInitial}(X) \\simeq \\text{IsInitial}(G(X)).$$$

Lean4

/-- A functor that preserves and reflects initial objects induces an equivalence on `IsInitial`. -/
def isInitialIffObj [PreservesColimit (Functor.empty.{0} C) G] [ReflectsColimit (Functor.empty.{0} C) G] (X : C) :
    IsInitial X ≃ IsInitial (G.obj X) where
  toFun := IsInitial.isInitialObj G X
  invFun := IsInitial.isInitialOfObj G X
  left_inv := by cat_disch
  right_inv := by cat_disch

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