Theorems · Definition · category theory

TopCat.Presheaf.generateEquivalenceOpensLe

{X : TopCat} →
  {ι : Type u_2} →
    (U : ι → TopologicalSpace.Opens ↑X) →
      {Y : TopologicalSpace.Opens ↑X} →
        Y = iSup U →
          ((CategoryTheory.ObjectProperty.FullSubcategory fun f =>
              (CategoryTheory.Sieve.generate (TopCat.Presheaf.presieveOfCoveringAux U Y)).arrows f.hom) ≌
            TopCat.Presheaf.SheafCondition.OpensLeCover U)

Given a family of opens U and an open Y equal to the union of opens in U, we may take the presieve on Y associated to U and the sieve generated by it, and form the full subcategory (subposet) of opens contained in Y (over Y) consisting of arrows in the sieve. This full subcategory is equivalent to OpensLeCover U, the (poset) category of opens contained in some U i.

Defined in

Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover

Cited by

6 results in Mathlib

Foundations

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