preservesTerminal_of_isSheaf_for_empty

English

If a presheaf F is a sheaf for the empty presieve at the initial object, then F preserves the terminal object through the empty limit cone.

Русский

Если пресшеаф F- является шейфом для пустого пресивера на начальном объекте, то F сохраняет терминальный объект через пустой предел.

LaTeX

$$$\\text{PreservesLimit}(\\text{empty }, F)$$$

Lean4

/-- If `F` is a presheaf which satisfies the sheaf condition with respect to the empty presieve on the
initial object, then `F` preserves terminal objects.
-/
theorem preservesTerminal_of_isSheaf_for_empty (hI : IsInitial I) : PreservesLimit (Functor.empty.{0} Cᵒᵖ) F :=
  have := hI.hasInitial
  (preservesTerminal_of_iso F
    ((F.mapIso (terminalIsoIsTerminal (terminalOpOfInitial initialIsInitial)) ≪≫
      (F.mapIso (initialIsoIsInitial hI).symm.op) ≪≫
        (terminalIsoIsTerminal (isTerminal_of_isSheafFor_empty_presieve I F hF)).symm)))

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