Theorems · Theorem · category theory

TopCat.Presheaf.isGluing_iff_pairwise

∀ {X : TopCat} {F : TopCat.Presheaf (Type u_4) X} {ι : Type u_5} {U : ι → TopologicalSpace.Opens ↑X}
  {sf : (i : ι) → CategoryTheory.ToType (F.obj (Opposite.op (U i)))}
  {s : CategoryTheory.ToType (F.obj (Opposite.op (iSup U)))},
  F.IsGluing U sf s ↔
    ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ),
      (CategoryTheory.ConcreteCategory.hom
            ((CategoryTheory.Functor.mapCone F (CategoryTheory.Pairwise.cocone U).op).π.app i))
          s =
        TopCat.Presheaf.objPairwiseOfFamily sf i

Defined in

Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing

Cited by

0 results in Mathlib

Foundations

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