Documentation

Mathlib.AlgebraicGeometry.Gluing

Gluing Schemes #

Given a family of gluing data of schemes, we may glue them together.

Main definitions #

Main results #

Implementation details #

All the hard work is done in AlgebraicGeometry/PresheafedSpace/Gluing.lean where we glue presheafed spaces, sheafed spaces, and locally ringed spaces.

A family of gluing data consists of

  1. An index type J
  2. A scheme U i for each i : J.
  3. A scheme V i j for each i j : J. (Note that this is J × J → Scheme rather than J → J → Scheme to connect to the limits library easier.)
  4. An open immersion f i j : V i j ⟶ U i for each i j : ι.
  5. A transition map t i j : V i j ⟶ V j i for each i j : ι. such that
  6. f i i is an isomorphism.
  7. t i i is the identity.
  8. V i j ×[U i] V i k ⟶ V i j ⟶ V j i factors through V j k ×[U j] V j i ⟶ V j i via some t' : V i j ×[U i] V i k ⟶ V j k ×[U j] V j i.
  9. t' i j k ≫ t' j k i ≫ t' k i j = 𝟙 _.

We can then glue the schemes U i together by identifying V i j with V j i, such that the U i's are open subschemes of the glued space.

Instances For
    @[reducible, inline]

    The glue data of locally ringed spaces associated to a family of glue data of schemes.

    Equations
    Instances For

      (Implementation). The glued scheme of a glue data. This should not be used outside this file. Use AlgebraicGeometry.Scheme.GlueData.glued instead.

      Equations
      Instances For
        @[reducible, inline]

        The glued scheme of a glued space.

        Equations
        • D.glued = D.glued
        Instances For
          @[reducible, inline]

          The immersion from D.U i into the glued space.

          Equations
          • D i = D i
          Instances For
            @[reducible, inline]
            abbrev AlgebraicGeometry.Scheme.GlueData.isoLocallyRingedSpace (D : AlgebraicGeometry.Scheme.GlueData) :
            D.glued.toLocallyRingedSpace D.toLocallyRingedSpaceGlueData.glued

            The gluing as sheafed spaces is isomorphic to the gluing as presheafed spaces.

            Equations
            Instances For
              theorem AlgebraicGeometry.Scheme.GlueData.ι_isoLocallyRingedSpace_inv (D : AlgebraicGeometry.Scheme.GlueData) (i : D.J) :
              CategoryTheory.CategoryStruct.comp (D.toLocallyRingedSpaceGlueData i) D.isoLocallyRingedSpace.inv = D i
              theorem AlgebraicGeometry.Scheme.GlueData.ι_jointly_surjective (D : AlgebraicGeometry.Scheme.GlueData) (x : D.glued.toPresheafedSpace) :
              ∃ (i : D.J) (y : (D.U i).toPresheafedSpace), (D i).val.base y = x

              The pullback cone spanned by V i j ⟶ U i and V i j ⟶ U j. This is a pullback diagram (vPullbackConeIsLimit).

              Equations
              Instances For

                The following diagram is a pullback, i.e. Vᵢⱼ is the intersection of Uᵢ and Uⱼ in X.

                Vᵢⱼ ⟶ Uᵢ | | ↓ ↓ Uⱼ ⟶ X

                Equations
                Instances For
                  def AlgebraicGeometry.Scheme.GlueData.isoCarrier (D : AlgebraicGeometry.Scheme.GlueData) :
                  D.glued.toPresheafedSpace D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.glued

                  The underlying topological space of the glued scheme is isomorphic to the gluing of the underlying spaces

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    @[simp]
                    theorem AlgebraicGeometry.Scheme.GlueData.ι_isoCarrier_inv (D : AlgebraicGeometry.Scheme.GlueData) (i : D.J) :
                    CategoryTheory.CategoryStruct.comp (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData i) D.isoCarrier.inv = (D i).val.base
                    def AlgebraicGeometry.Scheme.GlueData.Rel (D : AlgebraicGeometry.Scheme.GlueData) (a : (i : D.J) × (D.U i).toPresheafedSpace) (b : (i : D.J) × (D.U i).toPresheafedSpace) :

                    An equivalence relation on Σ i, D.U i that holds iff 𝖣 .ι i x = 𝖣 .ι j y. See AlgebraicGeometry.Scheme.GlueData.ι_eq_iff.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      theorem AlgebraicGeometry.Scheme.GlueData.ι_eq_iff (D : AlgebraicGeometry.Scheme.GlueData) (i : D.J) (j : D.J) (x : (D.U i).toPresheafedSpace) (y : (D.U j).toPresheafedSpace) :
                      (D i).val.base x = (D j).val.base y D.Rel i, x j, y
                      theorem AlgebraicGeometry.Scheme.GlueData.isOpen_iff (D : AlgebraicGeometry.Scheme.GlueData) (U : Set D.glued.toPresheafedSpace) :
                      IsOpen U ∀ (i : D.J), IsOpen ((D i).val.base ⁻¹' U)
                      theorem AlgebraicGeometry.Scheme.GlueData.openCover_f (D : AlgebraicGeometry.Scheme.GlueData) (x : D.glued.toPresheafedSpace) :
                      D.openCover.f x = .choose

                      The open cover of the glued space given by the glue data.

                      Equations
                      • D.openCover = { J := D.J, obj := D.U, map := D, f := fun (x : D.glued.toPresheafedSpace) => .choose, Covers := , IsOpen := }
                      Instances For
                        def AlgebraicGeometry.Scheme.OpenCover.gluedCoverT' {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x : 𝒰.J) (y : 𝒰.J) (z : 𝒰.J) :
                        CategoryTheory.Limits.pullback CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.fst

                        (Implementation) the transition maps in the glue data associated with an open cover.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          theorem AlgebraicGeometry.Scheme.OpenCover.gluedCoverT'_fst_fst_assoc {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x : 𝒰.J) (y : 𝒰.J) (z : 𝒰.J) {Z : AlgebraicGeometry.Scheme} (h : 𝒰.obj y Z) :
                          CategoryTheory.CategoryStruct.comp (𝒰.gluedCoverT' x y z) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h)) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h)
                          @[simp]
                          theorem AlgebraicGeometry.Scheme.OpenCover.gluedCoverT'_fst_fst {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x : 𝒰.J) (y : 𝒰.J) (z : 𝒰.J) :
                          CategoryTheory.CategoryStruct.comp (𝒰.gluedCoverT' x y z) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.fst) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd
                          theorem AlgebraicGeometry.Scheme.OpenCover.gluedCoverT'_fst_snd_assoc {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x : 𝒰.J) (y : 𝒰.J) (z : 𝒰.J) {Z : AlgebraicGeometry.Scheme} (h : 𝒰.obj z Z) :
                          CategoryTheory.CategoryStruct.comp (𝒰.gluedCoverT' x y z) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h)) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h)
                          @[simp]
                          theorem AlgebraicGeometry.Scheme.OpenCover.gluedCoverT'_fst_snd {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x : 𝒰.J) (y : 𝒰.J) (z : 𝒰.J) :
                          CategoryTheory.CategoryStruct.comp (𝒰.gluedCoverT' x y z) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.snd
                          theorem AlgebraicGeometry.Scheme.OpenCover.gluedCoverT'_snd_fst_assoc {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x : 𝒰.J) (y : 𝒰.J) (z : 𝒰.J) {Z : AlgebraicGeometry.Scheme} (h : 𝒰.obj y Z) :
                          CategoryTheory.CategoryStruct.comp (𝒰.gluedCoverT' x y z) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h)) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h)
                          @[simp]
                          theorem AlgebraicGeometry.Scheme.OpenCover.gluedCoverT'_snd_fst {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x : 𝒰.J) (y : 𝒰.J) (z : 𝒰.J) :
                          CategoryTheory.CategoryStruct.comp (𝒰.gluedCoverT' x y z) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.fst) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd
                          theorem AlgebraicGeometry.Scheme.OpenCover.gluedCoverT'_snd_snd_assoc {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x : 𝒰.J) (y : 𝒰.J) (z : 𝒰.J) {Z : AlgebraicGeometry.Scheme} (h : 𝒰.obj x Z) :
                          CategoryTheory.CategoryStruct.comp (𝒰.gluedCoverT' x y z) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h)) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h)
                          @[simp]
                          theorem AlgebraicGeometry.Scheme.OpenCover.gluedCoverT'_snd_snd {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x : 𝒰.J) (y : 𝒰.J) (z : 𝒰.J) :
                          CategoryTheory.CategoryStruct.comp (𝒰.gluedCoverT' x y z) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.snd) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.fst
                          theorem AlgebraicGeometry.Scheme.OpenCover.glued_cover_cocycle_fst {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x : 𝒰.J) (y : 𝒰.J) (z : 𝒰.J) :
                          CategoryTheory.CategoryStruct.comp (𝒰.gluedCoverT' x y z) (CategoryTheory.CategoryStruct.comp (𝒰.gluedCoverT' y z x) (CategoryTheory.CategoryStruct.comp (𝒰.gluedCoverT' z x y) CategoryTheory.Limits.pullback.fst)) = CategoryTheory.Limits.pullback.fst
                          theorem AlgebraicGeometry.Scheme.OpenCover.glued_cover_cocycle_snd {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x : 𝒰.J) (y : 𝒰.J) (z : 𝒰.J) :
                          CategoryTheory.CategoryStruct.comp (𝒰.gluedCoverT' x y z) (CategoryTheory.CategoryStruct.comp (𝒰.gluedCoverT' y z x) (CategoryTheory.CategoryStruct.comp (𝒰.gluedCoverT' z x y) CategoryTheory.Limits.pullback.snd)) = CategoryTheory.Limits.pullback.snd
                          theorem AlgebraicGeometry.Scheme.OpenCover.glued_cover_cocycle {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x : 𝒰.J) (y : 𝒰.J) (z : 𝒰.J) :
                          CategoryTheory.CategoryStruct.comp (𝒰.gluedCoverT' x y z) (CategoryTheory.CategoryStruct.comp (𝒰.gluedCoverT' y z x) (𝒰.gluedCoverT' z x y)) = CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.fst)
                          @[simp]
                          theorem AlgebraicGeometry.Scheme.OpenCover.gluedCover_t' {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x : 𝒰.J) (y : 𝒰.J) (z : 𝒰.J) :
                          𝒰.gluedCover.t' x y z = 𝒰.gluedCoverT' x y z
                          @[simp]
                          theorem AlgebraicGeometry.Scheme.OpenCover.gluedCover_f {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x : 𝒰.J) (y : 𝒰.J) :
                          𝒰.gluedCover.f x y = CategoryTheory.Limits.pullback.fst
                          @[simp]
                          theorem AlgebraicGeometry.Scheme.OpenCover.gluedCover_t {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x : 𝒰.J) (y : 𝒰.J) :
                          𝒰.gluedCover.t x y = (CategoryTheory.Limits.pullbackSymmetry (𝒰.map x) (𝒰.map y)).hom
                          @[simp]
                          theorem AlgebraicGeometry.Scheme.OpenCover.gluedCover_U {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) :
                          ∀ (a : 𝒰.J), 𝒰.gluedCover.U a = 𝒰.obj a
                          @[simp]
                          theorem AlgebraicGeometry.Scheme.OpenCover.gluedCover_J {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) :
                          𝒰.gluedCover.J = 𝒰.J
                          @[simp]
                          theorem AlgebraicGeometry.Scheme.OpenCover.gluedCover_V {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) :
                          ∀ (x : 𝒰.J × 𝒰.J), 𝒰.gluedCover.V x = match x with | (x, y) => CategoryTheory.Limits.pullback (𝒰.map x) (𝒰.map y)

                          The glue data associated with an open cover. The canonical isomorphism 𝒰.gluedCover.glued ⟶ X is provided by 𝒰.fromGlued.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            def AlgebraicGeometry.Scheme.OpenCover.fromGlued {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) :
                            𝒰.gluedCover.glued X

                            The canonical morphism from the gluing of an open cover of X into X. This is an isomorphism, as witnessed by an IsIso instance.

                            Equations
                            Instances For
                              @[simp]
                              theorem AlgebraicGeometry.Scheme.OpenCover.ι_fromGlued {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x : 𝒰.J) :
                              CategoryTheory.CategoryStruct.comp (𝒰.gluedCover x) 𝒰.fromGlued = 𝒰.map x
                              instance AlgebraicGeometry.Scheme.OpenCover.fromGlued_stalk_iso {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x : 𝒰.gluedCover.glued.toPresheafedSpace) :
                              Equations
                              • =
                              theorem AlgebraicGeometry.Scheme.OpenCover.fromGlued_open_map {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) :
                              IsOpenMap 𝒰.fromGlued.val.base
                              Equations
                              • =
                              def AlgebraicGeometry.Scheme.OpenCover.glueMorphisms {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) {Y : AlgebraicGeometry.Scheme} (f : (x : 𝒰.J) → 𝒰.obj x Y) (hf : ∀ (x y : 𝒰.J), CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (f x) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd (f y)) :
                              X Y

                              Given an open cover of X, and a morphism 𝒰.obj x ⟶ Y for each open subscheme in the cover, such that these morphisms are compatible in the intersection (pullback), we may glue the morphisms together into a morphism X ⟶ Y.

                              Note: If X is exactly (defeq to) the gluing of U i, then using Multicoequalizer.desc suffices.

                              Equations
                              Instances For
                                theorem AlgebraicGeometry.Scheme.OpenCover.ι_glueMorphisms_assoc {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) {Y : AlgebraicGeometry.Scheme} (f : (x : 𝒰.J) → 𝒰.obj x Y) (hf : ∀ (x y : 𝒰.J), CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (f x) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd (f y)) (x : 𝒰.J) {Z : AlgebraicGeometry.Scheme} (h : Y Z) :
                                @[simp]
                                theorem AlgebraicGeometry.Scheme.OpenCover.ι_glueMorphisms {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) {Y : AlgebraicGeometry.Scheme} (f : (x : 𝒰.J) → 𝒰.obj x Y) (hf : ∀ (x y : 𝒰.J), CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (f x) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd (f y)) (x : 𝒰.J) :
                                CategoryTheory.CategoryStruct.comp (𝒰.map x) (𝒰.glueMorphisms f hf) = f x
                                theorem AlgebraicGeometry.Scheme.OpenCover.hom_ext {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) {Y : AlgebraicGeometry.Scheme} (f₁ : X Y) (f₂ : X Y) (h : ∀ (x : 𝒰.J), CategoryTheory.CategoryStruct.comp (𝒰.map x) f₁ = CategoryTheory.CategoryStruct.comp (𝒰.map x) f₂) :
                                f₁ = f₂