Theorems · Definition · category theory

TopCat.Presheaf.SheafCondition.pairwiseCoconeIso

{X : TopCat} →
  {ι : Type u_2} →
    (U : ι → TopologicalSpace.Opens ↑X) →
      (CategoryTheory.Pairwise.cocone U).op ≅
        (CategoryTheory.Limits.Cone.postcomposeEquivalence
                (CategoryTheory.NatIso.op (TopCat.Presheaf.SheafCondition.pairwiseDiagramIso U))).functor.obj
          (CategoryTheory.Limits.Cone.whisker (TopCat.Presheaf.SheafCondition.pairwiseToOpensLeCover U).op
            (TopCat.Presheaf.SheafCondition.opensLeCoverCocone U).op)

The cocone Pairwise.cocone U with cocone point iSup U over Pairwise.diagram U is isomorphic to the cocone opensLeCoverCocone U (with the same cocone point) after appropriate whiskering and postcomposition.

Defined in

Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Cited by

0 results in Mathlib

Foundations

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