Theorems · Definition · category theory

TopCat.Presheaf.IsSheafUniqueGluing

{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {FC : C → C → Type u_2} →
      {CC : C → Type u_3} →
        [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] →
          [CategoryTheory.ConcreteCategory C FC] → {X : TopCat} → TopCat.Presheaf C X → Prop

The sheaf condition in terms of unique gluings. A presheaf F : Presheaf C X satisfies this sheaf condition if and only if, for every compatible family of sections sf : Π i : ι, F.obj (op (U i)), there exists a unique gluing s : F.obj (op (iSup U)). We prove this to be equivalent to the usual one below in TopCat.Presheaf.isSheaf_iff_isSheafUniqueGluing

Defined in

Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing

Cited by

3 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryFunLikeCategoryTheory.ConcreteCategory