Theorems · Definition · category theory

TopCat.Presheaf.whiskerIsoMapGenerateCocone

{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X : TopCat} →
      (F : TopCat.Presheaf C X) →
        {ι : Type u_2} →
          (U : ι → TopologicalSpace.Opens ↑X) →
            {Y : TopologicalSpace.Opens ↑X} →
              (hY : Y = iSup U) →
                CategoryTheory.Limits.Cone.whisker (TopCat.Presheaf.generateEquivalenceOpensLe U hY).op.functor
                    (CategoryTheory.Functor.mapCone F (TopCat.Presheaf.SheafCondition.opensLeCoverCocone U).op) ≅
                  CategoryTheory.Functor.mapCone F
                    (CategoryTheory.Sieve.generate (TopCat.Presheaf.presieveOfCoveringAux U Y)).arrows.cocone.op

Given a family of opens opensLeCoverCocone U is essentially the natural cocone associated to the sieve generated by the presieve associated to U with indexing category changed using the above equivalence.

Defined in

Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category