Documentation

Mathlib.AlgebraicGeometry.Cover.Directed

Locally directed covers #

A locally directed P-cover of a scheme X is a cover 𝒰 with an ordering on the indices and compatible transition maps 𝒰ᵢ ⟶ 𝒰ⱼ for i ≤ j such that every x : 𝒰ᵢ ×[X] 𝒰ⱼ comes from some 𝒰ₖ for a k ≤ i and k ≤ j.

Gluing along directed covers is easier, because the intersections 𝒰ᵢ ×[X] 𝒰ⱼ can be covered by a subcover of 𝒰. In particular, if 𝒰 is a Zariski cover, X naturally is the colimit of the 𝒰ᵢ.

Many natural covers are naturally directed, most importantly the cover of all affine opens of a scheme.

source
class AlgebraicGeometry.Scheme.Cover.LocallyDirected {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 : Cover (precoverage P) X) [CategoryTheory.Category.{u_2, u_1} 𝒰.I₀] :
Type (max (max u u_1) u_2)

A directed P-cover of a scheme X is a cover 𝒰 with an ordering on the indices and compatible transition maps 𝒰ᵢ ⟶ 𝒰ⱼ for i ≤ j such that every x : 𝒰ᵢ ×[X] 𝒰ⱼ comes from some 𝒰ₖ for a k ≤ i and k ≤ j.

Instances
    source
    def AlgebraicGeometry.Scheme.Cover.trans {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 : Cover (precoverage P) X) [CategoryTheory.Category.{u_2, u_1} 𝒰.I₀] [𝒰.LocallyDirected] {i j : 𝒰.I₀} (hij : i ⟶ j) :
    𝒰.X i ⟶ 𝒰.X j

    The transition maps of a directed cover.

    Equations
    Instances For
      source
      @[simp]
      theorem AlgebraicGeometry.Scheme.Cover.trans_map {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 : Cover (precoverage P) X) [CategoryTheory.Category.{u_2, u_1} 𝒰.I₀] [𝒰.LocallyDirected] {i j : 𝒰.I₀} (hij : i ⟶ j) :
      CategoryTheory.CategoryStruct.comp (𝒰.trans hij) (𝒰.f j) = 𝒰.f i
      source
      @[simp]
      theorem AlgebraicGeometry.Scheme.Cover.trans_id {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 : Cover (precoverage P) X) [CategoryTheory.Category.{u_2, u_1} 𝒰.I₀] [𝒰.LocallyDirected] (i : 𝒰.I₀) :
      𝒰.trans (CategoryTheory.CategoryStruct.id i) = CategoryTheory.CategoryStruct.id (𝒰.X i)
      source
      @[simp]
      theorem AlgebraicGeometry.Scheme.Cover.trans_comp {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 : Cover (precoverage P) X) [CategoryTheory.Category.{u_2, u_1} 𝒰.I₀] [𝒰.LocallyDirected] {i j k : 𝒰.I₀} (hij : i ⟶ j) (hjk : j ⟶ k) :
      𝒰.trans (CategoryTheory.CategoryStruct.comp hij hjk) = CategoryTheory.CategoryStruct.comp (𝒰.trans hij) (𝒰.trans hjk)
      source
      theorem AlgebraicGeometry.Scheme.Cover.exists_lift_trans_eq {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 : Cover (precoverage P) X) [CategoryTheory.Category.{u_2, u_1} 𝒰.I₀] [𝒰.LocallyDirected] {i j : 𝒰.I₀} (x : ↥(CategoryTheory.Limits.pullback (𝒰.f i) (𝒰.f j))) :
      ∃ (k : 𝒰.I₀) (hki : k ⟶ i) (hkj : k ⟶ j) (y : ↥(𝒰.X k)), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.lift (𝒰.trans hki) (𝒰.trans hkj) ⋯).base) y = x
      source
      theorem AlgebraicGeometry.Scheme.Cover.property_trans {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 : Cover (precoverage P) X) [CategoryTheory.Category.{u_2, u_1} 𝒰.I₀] [𝒰.LocallyDirected] {i j : 𝒰.I₀} (hij : i ⟶ j) :
      P (𝒰.trans hij)
      source
      def AlgebraicGeometry.Scheme.Cover.intersectionOfLocallyDirected {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 : Cover (precoverage P) X) [CategoryTheory.Category.{u_2, u_1} 𝒰.I₀] [𝒰.LocallyDirected] [P.IsStableUnderBaseChange] [P.HasOfPostcompProperty P] (i j : 𝒰.I₀) :
      Cover (precoverage P) (CategoryTheory.Limits.pullback (𝒰.f i) (𝒰.f j))

      If 𝒰 is a directed cover of X, this is the cover of 𝒰ᵢ ×[X] 𝒰ⱼ by {𝒰ₖ} where k ≤ i and k ≤ j.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem AlgebraicGeometry.Scheme.Cover.intersectionOfLocallyDirected_f {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 : Cover (precoverage P) X) [CategoryTheory.Category.{u_2, u_1} 𝒰.I₀] [𝒰.LocallyDirected] [P.IsStableUnderBaseChange] [P.HasOfPostcompProperty P] (i j : 𝒰.I₀) (k : (k : 𝒰.I₀) × (k ⟶ i) × (k ⟶ j)) :
        (𝒰.intersectionOfLocallyDirected i j).f k = CategoryTheory.Limits.pullback.lift (𝒰.trans k.snd.1) (𝒰.trans k.snd.2) ⋯
        source
        def AlgebraicGeometry.Scheme.Cover.functorOfLocallyDirected {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 : Cover (precoverage P) X) [CategoryTheory.Category.{u_2, u_1} 𝒰.I₀] [𝒰.LocallyDirected] :
        CategoryTheory.Functor 𝒰.I₀ Scheme

        The canonical diagram induced by a locally directed cover.

        Equations
        Instances For
          source
          @[simp]
          theorem AlgebraicGeometry.Scheme.Cover.functorOfLocallyDirected_obj {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 : Cover (precoverage P) X) [CategoryTheory.Category.{u_2, u_1} 𝒰.I₀] [𝒰.LocallyDirected] (i : 𝒰.I₀) :
          𝒰.functorOfLocallyDirected.obj i = 𝒰.X i
          source
          @[simp]
          theorem AlgebraicGeometry.Scheme.Cover.functorOfLocallyDirected_map {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 : Cover (precoverage P) X) [CategoryTheory.Category.{u_2, u_1} 𝒰.I₀] [𝒰.LocallyDirected] {X✝ Y✝ : 𝒰.I₀} (hij : X✝ ⟶ Y✝) :
          𝒰.functorOfLocallyDirected.map hij = 𝒰.trans hij
          source
          instance AlgebraicGeometry.Scheme.Cover.instIsLocallyDirectedI₀CompFunctorOfLocallyDirectedForget {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 : Cover (precoverage P) X) [CategoryTheory.Category.{u_2, u_1} 𝒰.I₀] [𝒰.LocallyDirected] :
          (𝒰.functorOfLocallyDirected.comp forget).IsLocallyDirected
          source
          def AlgebraicGeometry.Scheme.Cover.coconeOfLocallyDirected {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 : Cover (precoverage P) X) [CategoryTheory.Category.{u_2, u_1} 𝒰.I₀] [𝒰.LocallyDirected] :
          CategoryTheory.Limits.Cocone 𝒰.functorOfLocallyDirected

          The canonical cocone with point X on the functor induced by the locally directed cover 𝒰. If 𝒰 is an open cover, this is colimiting (see OpenCover.isColimitCoconeOfLocallyDirected).

          Equations
          Instances For
            source
            @[simp]
            theorem AlgebraicGeometry.Scheme.Cover.coconeOfLocallyDirected_pt {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 : Cover (precoverage P) X) [CategoryTheory.Category.{u_2, u_1} 𝒰.I₀] [𝒰.LocallyDirected] :
            𝒰.coconeOfLocallyDirected.pt = X
            source
            @[simp]
            theorem AlgebraicGeometry.Scheme.Cover.coconeOfLocallyDirected_ι_app {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 : Cover (precoverage P) X) [CategoryTheory.Category.{u_2, u_1} 𝒰.I₀] [𝒰.LocallyDirected] (i : 𝒰.I₀) :
            𝒰.coconeOfLocallyDirected.ι.app i = 𝒰.f i
            source
            instance AlgebraicGeometry.Scheme.Cover.instCategoryI₀Pullback₁ {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} [P.IsStableUnderBaseChange] (𝒰 : Cover (precoverage P) X) [CategoryTheory.Category.{u_2, u_1} 𝒰.I₀] {Y : Scheme} (f : Y ⟶ X) :
            CategoryTheory.Category.{u_2, u_1} (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀
            Equations
            source
            instance AlgebraicGeometry.Scheme.Cover.locallyDirectedPullbackCover {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} [P.IsStableUnderBaseChange] (𝒰 : Cover (precoverage P) X) [CategoryTheory.Category.{u_2, u_1} 𝒰.I₀] [𝒰.LocallyDirected] {Y : Scheme} (f : Y ⟶ X) :
            LocallyDirected (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰)
            Equations
            • One or more equations did not get rendered due to their size.
            source
            instance AlgebraicGeometry.Scheme.OpenCover.instIsOpenImmersionTrans {X : Scheme} (𝒰 : X.OpenCover) [CategoryTheory.Category.{u_2, u_1} 𝒰.I₀] [Cover.LocallyDirected 𝒰] {i j : 𝒰.I₀} (f : i ⟶ j) :
            IsOpenImmersion (Cover.trans 𝒰 f)
            source
            instance AlgebraicGeometry.Scheme.OpenCover.instIsOpenImmersionMapI₀FunctorOfLocallyDirected {X : Scheme} (𝒰 : X.OpenCover) [CategoryTheory.Category.{u_2, u_1} 𝒰.I₀] [Cover.LocallyDirected 𝒰] {i j : 𝒰.I₀} (f : i ⟶ j) :
            IsOpenImmersion ((Cover.functorOfLocallyDirected 𝒰).map f)
            source
            def AlgebraicGeometry.Scheme.OpenCover.glueMorphismsOfLocallyDirected {X : Scheme} (𝒰 : X.OpenCover) [CategoryTheory.Category.{u_2, u_1} 𝒰.I₀] [Cover.LocallyDirected 𝒰] {Y : Scheme} (g : (i : 𝒰.I₀) → 𝒰.X i ⟶ Y) (h : ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), CategoryTheory.CategoryStruct.comp (Cover.trans 𝒰 hij) (g j) = g i) :
            X ⟶ Y

            If 𝒰 is a directed open cover of X, to glue morphisms {gᵢ : 𝒰ᵢ ⟶ Y} it suffices to check compatibility with the transition maps. See OpenCover.isColimitCoconeOfLocallyDirected for this result stated in the language of colimits.

            Equations
            Instances For
              source
              @[simp]
              theorem AlgebraicGeometry.Scheme.OpenCover.map_glueMorphismsOfLocallyDirected {X : Scheme} (𝒰 : X.OpenCover) [CategoryTheory.Category.{u_2, u_1} 𝒰.I₀] [Cover.LocallyDirected 𝒰] {Y : Scheme} (g : (i : 𝒰.I₀) → 𝒰.X i ⟶ Y) (h : ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), CategoryTheory.CategoryStruct.comp (Cover.trans 𝒰 hij) (g j) = g i) (i : 𝒰.I₀) :
              CategoryTheory.CategoryStruct.comp (𝒰.f i) (𝒰.glueMorphismsOfLocallyDirected g ⋯) = g i
              source
              @[simp]
              theorem AlgebraicGeometry.Scheme.OpenCover.map_glueMorphismsOfLocallyDirected_assoc {X : Scheme} (𝒰 : X.OpenCover) [CategoryTheory.Category.{u_2, u_1} 𝒰.I₀] [Cover.LocallyDirected 𝒰] {Y : Scheme} (g : (i : 𝒰.I₀) → 𝒰.X i ⟶ Y) (h : ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), CategoryTheory.CategoryStruct.comp (Cover.trans 𝒰 hij) (g j) = g i) (i : 𝒰.I₀) {Z : Scheme} (h✝ : Y ⟶ Z) :
              CategoryTheory.CategoryStruct.comp (𝒰.f i) (CategoryTheory.CategoryStruct.comp (𝒰.glueMorphismsOfLocallyDirected g ⋯) h✝) = CategoryTheory.CategoryStruct.comp (g i) h✝
              source
              def AlgebraicGeometry.Scheme.OpenCover.isColimitCoconeOfLocallyDirected {X : Scheme} (𝒰 : X.OpenCover) [CategoryTheory.Category.{u_2, u_1} 𝒰.I₀] [Cover.LocallyDirected 𝒰] :
              CategoryTheory.Limits.IsColimit (Cover.coconeOfLocallyDirected 𝒰)

              If 𝒰 is an open cover of X that is locally directed, X is the colimit of the components of 𝒰.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def AlgebraicGeometry.Scheme.OpenCover.glueMorphismsOverOfLocallyDirected {S : Scheme} {X : CategoryTheory.Over S} (𝒰 : X.left.OpenCover) [CategoryTheory.Category.{u_2, u_1} 𝒰.I₀] [Cover.LocallyDirected 𝒰] {Y : CategoryTheory.Over S} (g : (i : 𝒰.I₀) → 𝒰.X i ⟶ Y.left) (h : ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), CategoryTheory.CategoryStruct.comp (Cover.trans 𝒰 hij) (g j) = g i) (w : ∀ (i : 𝒰.I₀), CategoryTheory.CategoryStruct.comp (g i) Y.hom = CategoryTheory.CategoryStruct.comp (𝒰.f i) X.hom) :
                X ⟶ Y

                If 𝒰 is a directed open cover of X, to glue morphisms {gᵢ : 𝒰ᵢ ⟶ Y} over S it suffices to check compatibility with the transition maps.

                Equations
                Instances For
                  source
                  @[simp]
                  theorem AlgebraicGeometry.Scheme.OpenCover.map_glueMorphismsOverOfLocallyDirected_left {S : Scheme} {X : CategoryTheory.Over S} (𝒰 : X.left.OpenCover) [CategoryTheory.Category.{u_2, u_1} 𝒰.I₀] [Cover.LocallyDirected 𝒰] {Y : CategoryTheory.Over S} (g : (i : 𝒰.I₀) → 𝒰.X i ⟶ Y.left) (h : ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), CategoryTheory.CategoryStruct.comp (Cover.trans 𝒰 hij) (g j) = g i) (w : ∀ (i : 𝒰.I₀), CategoryTheory.CategoryStruct.comp (g i) Y.hom = CategoryTheory.CategoryStruct.comp (𝒰.f i) X.hom) (i : 𝒰.I₀) :
                  CategoryTheory.CategoryStruct.comp (𝒰.f i) (𝒰.glueMorphismsOverOfLocallyDirected g ⋯ w).left = g i
                  source
                  @[simp]
                  theorem AlgebraicGeometry.Scheme.OpenCover.map_glueMorphismsOverOfLocallyDirected_left_assoc {S : Scheme} {X : CategoryTheory.Over S} (𝒰 : X.left.OpenCover) [CategoryTheory.Category.{u_2, u_1} 𝒰.I₀] [Cover.LocallyDirected 𝒰] {Y : CategoryTheory.Over S} (g : (i : 𝒰.I₀) → 𝒰.X i ⟶ Y.left) (h : ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), CategoryTheory.CategoryStruct.comp (Cover.trans 𝒰 hij) (g j) = g i) (w : ∀ (i : 𝒰.I₀), CategoryTheory.CategoryStruct.comp (g i) Y.hom = CategoryTheory.CategoryStruct.comp (𝒰.f i) X.hom) (i : 𝒰.I₀) {Z : Scheme} (h✝ : Y.left ⟶ Z) :
                  CategoryTheory.CategoryStruct.comp (𝒰.f i) (CategoryTheory.CategoryStruct.comp (𝒰.glueMorphismsOverOfLocallyDirected g ⋯ w).left h✝) = CategoryTheory.CategoryStruct.comp (g i) h✝
                  source
                  def AlgebraicGeometry.Scheme.Cover.LocallyDirected.ofIsBasisOpensRange {X : Scheme} {𝒰 : X.OpenCover} [Preorder 𝒰.I₀] (hle : ∀ {i j : 𝒰.I₀}, i ≤ j ↔ Hom.opensRange (𝒰.f i) ≤ Hom.opensRange (𝒰.f j)) (H : TopologicalSpace.Opens.IsBasis (Set.range fun (i : 𝒰.I₀) => Hom.opensRange (𝒰.f i))) :
                  LocallyDirected 𝒰

                  If 𝒰 is an open cover such that the images of the components form a basis of the topology of X, 𝒰 is directed by the ordering of subset inclusion of the images.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    theorem AlgebraicGeometry.Scheme.Cover.LocallyDirected.ofIsBasisOpensRange_le_iff {X : Scheme} {𝒰 : X.OpenCover} [Preorder 𝒰.I₀] (hle : ∀ {i j : 𝒰.I₀}, i ≤ j ↔ Hom.opensRange (𝒰.f i) ≤ Hom.opensRange (𝒰.f j)) (i j : 𝒰.I₀) :
                    i ≤ j ↔ Hom.opensRange (𝒰.f i) ≤ Hom.opensRange (𝒰.f j)
                    source
                    theorem AlgebraicGeometry.Scheme.Cover.LocallyDirected.ofIsBasisOpensRange_trans {X : Scheme} {𝒰 : X.OpenCover} [Preorder 𝒰.I₀] (hle : ∀ {i j : 𝒰.I₀}, i ≤ j ↔ Hom.opensRange (𝒰.f i) ≤ Hom.opensRange (𝒰.f j)) (H : TopologicalSpace.Opens.IsBasis (Set.range fun (i : 𝒰.I₀) => Hom.opensRange (𝒰.f i))) {i j : 𝒰.I₀} (hij : i ≤ j) :
                    Cover.trans 𝒰 (CategoryTheory.homOfLE hij) = IsOpenImmersion.lift (𝒰.f j) (𝒰.f i) ⋯
                    source
                    def AlgebraicGeometry.Scheme.directedAffineCover (X : Scheme) :
                    X.OpenCover

                    The directed affine open cover of X given by all affine opens.

                    Equations
                    Instances For
                      source
                      @[simp]
                      theorem AlgebraicGeometry.Scheme.directedAffineCover_f (X : Scheme) (U : ↑X.affineOpens) :
                      X.directedAffineCover.f U = (↑U).ι
                      source
                      @[simp]
                      theorem AlgebraicGeometry.Scheme.directedAffineCover_X (X : Scheme) (U : ↑X.affineOpens) :
                      X.directedAffineCover.X U = ↑↑U
                      source
                      @[simp]
                      theorem AlgebraicGeometry.Scheme.directedAffineCover_I₀ (X : Scheme) :
                      X.directedAffineCover.I₀ = ↑X.affineOpens
                      source
                      instance AlgebraicGeometry.Scheme.instPreorderI₀DirectedAffineCover {X : Scheme} :
                      Preorder X.directedAffineCover.I₀
                      Equations
                      source
                      instance AlgebraicGeometry.Scheme.instLocallyDirectedIsOpenImmersionDirectedAffineCover {X : Scheme} :
                      Cover.LocallyDirected X.directedAffineCover
                      Equations
                      source
                      @[simp]
                      theorem AlgebraicGeometry.Scheme.directedAffineCover_trans {X : Scheme} {U V : ↑X.affineOpens} (hUV : U ≤ V) :
                      Cover.trans X.directedAffineCover (CategoryTheory.homOfLE hUV) = X.homOfLE hUV