Theorems · Definition · category theory

TopCat.Presheaf.IsCompatible.sectionPairwise

{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)))} →
          F.IsCompatible U sf → ↑((CategoryTheory.Pairwise.diagram U).op.comp F).sections

Given a compatible family of sections over open sets, extend it to a section of the functor (Pairwise.diagram U).op ⋙ F.

Defined in

Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing

Cited by

2 results in Mathlib

Foundations

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