Theorems · Theorem · category theory

CategoryTheory.Presieve.preservesTerminal_of_isSheaf_for_empty

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : C} (F : CategoryTheory.Functor Cᵒᵖ (Type w)),
  CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows Empty.elim fun a => Empty.instIsEmpty.elim a) →
    ∀ (hI : CategoryTheory.Limits.IsInitial I),
      CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty Cᵒᵖ) F

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.

Defined in

Mathlib.CategoryTheory.Sites.Preserves

Cited by

1 results in Mathlib

Foundations

Depth 72 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.Category