Theorems · Theorem · category theory

TopCat.Presheaf.IsSheaf.section_ext

∀ {X : TopCat} {A : Type u_1} [inst : CategoryTheory.Category.{u, u_1} A] {FC : A → A → Type u_2} {CC : A → Type u}
  [inst_1 : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory A FC]
  [CategoryTheory.Limits.HasLimits A] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget A)]
  [(CategoryTheory.forget A).ReflectsIsomorphisms] {F : TopCat.Presheaf A X},
  F.IsSheaf →
    ∀ {U : (TopologicalSpace.Opens ↑X)ᵒᵖ} {s t : CategoryTheory.ToType (F.obj U)},
      (∀ x ∈ Opposite.unop U,
          ∃ V,
            ∃ (hV : V ≤ Opposite.unop U),
              x ∈ V ∧
                (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE hV).op)) s =
                  (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE hV).op)) t) →
        s = t

Defined in

Mathlib.Topology.Sheaves.Sheaf

Cited by

5 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryFunLikeCategoryTheory.ConcreteCategoryCategoryTheory.Limits.HasLimitsCategoryTheory.Limits.PreservesLimitsCategoryTheory.Functor.ReflectsIsomorphisms