initial_iff_fiber_empty — Mathlib

English

An object is initial if and only if its fiber is empty.

Русский

Объект начальный тогда и только тогда, когда его фибер пуст.

LaTeX

$$$\\mathrm{Category}(C) \\land \\mathrm{PreGaloisCategory}(C) \\Rightarrow \\bigl\\forall X,\\mathrm{IsInitial}(X) \\iff \\mathrm{F.obj}(X)\\text{ пустой} \\bigr)$$$

Lean4

/-- An object is initial if and only if its fiber is empty. -/
theorem initial_iff_fiber_empty (X : C) : Nonempty (IsInitial X) ↔ IsEmpty (F.obj X) :=
  by
  rw [(IsInitial.isInitialIffObj F X).nonempty_congr]
  haveI : PreservesFiniteColimits (forget FintypeCat) :=
    by
    change PreservesFiniteColimits FintypeCat.incl
    infer_instance
  haveI : ReflectsColimit (Functor.empty.{0} _) (forget FintypeCat) :=
    by
    change ReflectsColimit (Functor.empty.{0} _) FintypeCat.incl
    infer_instance
  exact Concrete.initial_iff_empty_of_preserves_of_reflects (F.obj X)

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