isSheaf_of_isTerminal — Mathlib

English

Same statement as above: the constant presheaf on a terminal object is a sheaf.

Русский

То же утверждение: константный прешиф на терминальном объекте — шейф.

LaTeX

$$$\\text{IsSheaf } J (\\mathrm{const}\\! _{\\_} X) \\text{ if } IsTerminal(X).$$$

Lean4

theorem isSheaf_of_isTerminal {X : A} (hX : IsTerminal X) :
    Presheaf.IsSheaf J ((CategoryTheory.Functor.const _).obj X) := fun _ _ _ _ _ _ =>
  ⟨hX.from _, fun _ _ _ => hX.hom_ext _ _, fun _ _ => hX.hom_ext _ _⟩

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