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
    @[inline, reducible]

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

    Instances For

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

      Instances For
        @[inline, reducible]

        The glued scheme of a glued space.

        Instances For
          @[inline, reducible]

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

          Instances For
            @[inline, reducible]

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

            Instances For
              theorem AlgebraicGeometry.Scheme.GlueData.ι_jointly_surjective (D : AlgebraicGeometry.Scheme.GlueData) (x : (CategoryTheory.GlueData.glued D.toGlueData).toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace) :
              i y, (AlgebraicGeometry.Scheme.GlueData.ι 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).

              Instances For

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

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

                Instances For
                  def AlgebraicGeometry.Scheme.GlueData.Rel (D : AlgebraicGeometry.Scheme.GlueData) (a : (i : D.J) × (CategoryTheory.GlueData.U D.toGlueData i).toPresheafedSpace) (b : (i : D.J) × (CategoryTheory.GlueData.U D.toGlueData i).toPresheafedSpace) :

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

                  Instances For
                    theorem AlgebraicGeometry.Scheme.GlueData.ι_eq_iff (D : AlgebraicGeometry.Scheme.GlueData) (i : D.J) (j : D.J) (x : (CategoryTheory.GlueData.U D.toGlueData i).toPresheafedSpace) (y : (CategoryTheory.GlueData.U D.toGlueData j).toPresheafedSpace) :
                    (CategoryTheory.GlueData.ι D.toGlueData i).val.base x = (CategoryTheory.GlueData.ι D.toGlueData j).val.base y AlgebraicGeometry.Scheme.GlueData.Rel D { fst := i, snd := x } { fst := j, snd := y }
                    theorem AlgebraicGeometry.Scheme.GlueData.isOpen_iff (D : AlgebraicGeometry.Scheme.GlueData) (U : Set (AlgebraicGeometry.Scheme.GlueData.glued D).toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace) :
                    IsOpen U ∀ (i : D.J), IsOpen ((AlgebraicGeometry.Scheme.GlueData.ι D i).val.base ⁻¹' U)
                    def AlgebraicGeometry.Scheme.OpenCover.gluedCoverT' {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) (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.

                    Instances For
                      @[simp]
                      theorem AlgebraicGeometry.Scheme.OpenCover.gluedCoverT'_fst_fst {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) (x : 𝒰.J) (y : 𝒰.J) (z : 𝒰.J) :
                      CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.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
                      @[simp]
                      theorem AlgebraicGeometry.Scheme.OpenCover.gluedCoverT'_fst_snd {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) (x : 𝒰.J) (y : 𝒰.J) (z : 𝒰.J) :
                      CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.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
                      @[simp]
                      theorem AlgebraicGeometry.Scheme.OpenCover.gluedCoverT'_snd_fst {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) (x : 𝒰.J) (y : 𝒰.J) (z : 𝒰.J) :
                      CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.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
                      @[simp]
                      theorem AlgebraicGeometry.Scheme.OpenCover.gluedCoverT'_snd_snd {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) (x : 𝒰.J) (y : 𝒰.J) (z : 𝒰.J) :
                      CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.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
                      @[simp]

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

                      Instances For

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

                        Instances For
                          def AlgebraicGeometry.Scheme.OpenCover.glueMorphisms {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) {Y : AlgebraicGeometry.Scheme} (f : (x : 𝒰.J) → AlgebraicGeometry.Scheme.OpenCover.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.

                          Instances For