Theorems · Definition · category theory

TopCat.Presheaf.IsGluing

{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)] →
          [inst_2 : CategoryTheory.ConcreteCategory C FC] →
            {X : TopCat} →
              (F : TopCat.Presheaf C X) →
                {ι : Type u_4} →
                  (U : ι → TopologicalSpace.Opens ↑X) →
                    ((i : ι) → CategoryTheory.ToType (F.obj (Opposite.op (U i)))) →
                      CategoryTheory.ToType (F.obj (Opposite.op (iSup U))) → Prop

A section s is a gluing for a family of sections sf if it restricts to sf i on U i, for all i

Defined in

Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing

Cited by

11 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryFunLikeCategoryTheory.ConcreteCategory