Theorems · Definition · category theory

TopCat.Presheaf.IsCompatible

{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)))) → Prop

A family of sections sf is compatible, if the restrictions of sf i and sf j to U i ⊓ U j agree, for all i and j

Defined in

Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing

Cited by

10 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryFunLikeCategoryTheory.ConcreteCategory