Documentation

Mathlib.AlgebraicGeometry.Pullbacks

Fibred products of schemes #

In this file we construct the fibred product of schemes via gluing. We roughly follow [Har77] Theorem 3.3.

In particular, the main construction is to show that for an open cover { Uᵢ } of X, if there exist fibred products Uᵢ ×[Z] Y for each i, then there exists a fibred product X ×[Z] Y.

Then, for constructing the fibred product for arbitrary schemes X, Y, Z, we can use the construction to reduce to the case where X, Y, Z are all affine, where fibred products are constructed via tensor products.

def AlgebraicGeometry.Scheme.Pullback.v {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X Z) (g : Y Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i : 𝒰.J) (j : 𝒰.J) :

The intersection of Uᵢ ×[Z] Y and Uⱼ ×[Z] Y is given by (Uᵢ ×[Z] Y) ×[X] Uⱼ

Equations
  • One or more equations did not get rendered due to their size.
Instances For

    The canonical transition map (Uᵢ ×[Z] Y) ×[X] Uⱼ ⟶ (Uⱼ ×[Z] Y) ×[X] Uᵢ given by the fact that pullbacks are associative and symmetric.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[reducible, inline]

      The inclusion map of V i j = (Uᵢ ×[Z] Y) ×[X] Uⱼ ⟶ Uᵢ ×[Z] Y

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        The map ((Xᵢ ×[Z] Y) ×[X] Xⱼ) ×[Xᵢ ×[Z] Y] ((Xᵢ ×[Z] Y) ×[X] Xₖ)((Xⱼ ×[Z] Y) ×[X] Xₖ) ×[Xⱼ ×[Z] Y] ((Xⱼ ×[Z] Y) ×[X] Xᵢ) needed for gluing

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          theorem AlgebraicGeometry.Scheme.Pullback.t'_fst_fst_snd_assoc {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X Z✝) (g : Y Z✝) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i : 𝒰.J) (j : 𝒰.J) (k : 𝒰.J) {Z : AlgebraicGeometry.Scheme} (h : Y Z) :
          theorem AlgebraicGeometry.Scheme.Pullback.t'_snd_fst_snd_assoc {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X Z✝) (g : Y Z✝) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i : 𝒰.J) (j : 𝒰.J) (k : 𝒰.J) {Z : AlgebraicGeometry.Scheme} (h : Y Z) :
          theorem AlgebraicGeometry.Scheme.Pullback.cocycle_fst_fst_fst {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X Z) (g : Y Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i : 𝒰.J) (j : 𝒰.J) (k : 𝒰.J) :
          theorem AlgebraicGeometry.Scheme.Pullback.cocycle_fst_fst_snd {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X Z) (g : Y Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i : 𝒰.J) (j : 𝒰.J) (k : 𝒰.J) :
          theorem AlgebraicGeometry.Scheme.Pullback.cocycle_snd_fst_fst {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X Z) (g : Y Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i : 𝒰.J) (j : 𝒰.J) (k : 𝒰.J) :
          theorem AlgebraicGeometry.Scheme.Pullback.cocycle_snd_fst_snd {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X Z) (g : Y Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i : 𝒰.J) (j : 𝒰.J) (k : 𝒰.J) :
          @[simp]
          @[simp]
          theorem AlgebraicGeometry.Scheme.Pullback.gluing_V {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X Z) (g : Y Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] :
          ∀ (x : 𝒰.J × 𝒰.J), (AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).V x = match x with | (i, j) => AlgebraicGeometry.Scheme.Pullback.v 𝒰 f g i j
          @[simp]
          theorem AlgebraicGeometry.Scheme.Pullback.gluing_t' {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X Z) (g : Y Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i : 𝒰.J) (j : 𝒰.J) (k : 𝒰.J) :

          Given Uᵢ ×[Z] Y, this is the glued fibered product X ×[Z] Y.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For

            The first projection from the glued scheme into X.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For

              The second projection from the glued scheme into Y.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                def AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X Z) (g : Y Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (s : CategoryTheory.Limits.PullbackCone f g) (i : 𝒰.J) (j : 𝒰.J) :
                CategoryTheory.Limits.pullback ((𝒰.pullbackCover s.fst).map i) ((𝒰.pullbackCover s.fst).map j) (AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).V (i, j)

                (Implementation) The canonical map (s.X ×[X] Uᵢ) ×[s.X] (s.X ×[X] Uⱼ) ⟶ (Uᵢ ×[Z] Y) ×[X] Uⱼ

                This is used in gluedLift.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For

                  The lifted map s.X ⟶ (gluing 𝒰 f g).glued in order to show that (gluing 𝒰 f g).glued is indeed the pullback.

                  Given a pullback cone s, we have the maps s.fst ⁻¹' Uᵢ ⟶ Uᵢ and s.fst ⁻¹' Uᵢ ⟶ s.X ⟶ Y that we may lift to a map s.fst ⁻¹' Uᵢ ⟶ Uᵢ ×[Z] Y.

                  to glue these into a map s.X ⟶ Uᵢ ×[Z] Y, we need to show that the maps agree on (s.fst ⁻¹' Uᵢ) ×[s.X] (s.fst ⁻¹' Uⱼ) ⟶ Uᵢ ×[Z] Y. This is achieved by showing that both of these maps factors through gluedLiftPullbackMap.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For

                    (Implementation) The canonical map (W ×[X] Uᵢ) ×[W] (Uⱼ ×[Z] Y) ⟶ (Uⱼ ×[Z] Y) ×[X] Uᵢ = V j i where W is the glued fibred product.

                    This is used in lift_comp_ι.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For

                      We show that the map W ×[X] Uᵢ ⟶ Uᵢ ×[Z] Y ⟶ W is the first projection, where the first map is given by the lift of W ×[X] Uᵢ ⟶ Uᵢ and W ×[X] Uᵢ ⟶ W ⟶ Y.

                      It suffices to show that the two map agrees when restricted onto Uⱼ ×[Z] Y. In this case, both maps factor through V j i via pullback_fst_ι_to_V

                      The canonical isomorphism between W ×[X] Uᵢ and Uᵢ ×[X] Y. That is, the preimage of Uᵢ in W along p1 is indeed Uᵢ ×[X] Y.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For

                        The glued scheme ((gluing 𝒰 f g).glued) is indeed the pullback of f and g.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For

                          Given an open cover { Xᵢ } of X, then X ×[Z] Y is covered by Xᵢ ×[Z] Y.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For

                            Given an open cover { Yᵢ } of Y, then X ×[Z] Y is covered by X ×[Z] Yᵢ.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              @[simp]
                              theorem AlgebraicGeometry.Scheme.Pullback.openCoverOfLeftRight_map {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (𝒰X : X.OpenCover) (𝒰Y : Y.OpenCover) (f : X Z) (g : Y Z) (ij : 𝒰X.J × 𝒰Y.J) :
                              @[simp]
                              @[simp]
                              theorem AlgebraicGeometry.Scheme.Pullback.openCoverOfLeftRight_J {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (𝒰X : X.OpenCover) (𝒰Y : Y.OpenCover) (f : X Z) (g : Y Z) :
                              (AlgebraicGeometry.Scheme.Pullback.openCoverOfLeftRight 𝒰X 𝒰Y f g).J = (𝒰X.J × 𝒰Y.J)
                              def AlgebraicGeometry.Scheme.Pullback.openCoverOfLeftRight {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (𝒰X : X.OpenCover) (𝒰Y : Y.OpenCover) (f : X Z) (g : Y Z) :

                              Given an open cover { Xᵢ } of X and an open cover { Yⱼ } of Y, then X ×[Z] Y is covered by Xᵢ ×[Z] Yⱼ.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                @[simp]
                                theorem AlgebraicGeometry.Scheme.Pullback.openCoverOfBase'_map {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (𝒰 : Z.OpenCover) (f : X Z) (g : Y Z) (x : (i : (AlgebraicGeometry.Scheme.Pullback.openCoverOfLeft (𝒰.pullbackCover f) f g).J) × ((fun (i : (AlgebraicGeometry.Scheme.Pullback.openCoverOfLeft (𝒰.pullbackCover f) f g).J) => let Xᵢ := CategoryTheory.Limits.pullback f (𝒰.map i); let Yᵢ := CategoryTheory.Limits.pullback g (𝒰.map i); let W := CategoryTheory.Limits.pullback (CategoryTheory.Limits.pullback.snd g (𝒰.map i)) (CategoryTheory.Limits.pullback.snd f (𝒰.map i)); let_fun this := CategoryTheory.Limits.bigSquareIsPullback (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.snd g (𝒰.map i)) (CategoryTheory.Limits.pullback.snd f (𝒰.map i))) (CategoryTheory.Limits.pullback.fst g (𝒰.map i)) (CategoryTheory.Limits.pullback.snd f (𝒰.map i)) (𝒰.map i) (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.snd g (𝒰.map i)) (CategoryTheory.Limits.pullback.snd f (𝒰.map i))) (CategoryTheory.Limits.pullback.snd g (𝒰.map i)) g (CategoryTheory.Limits.PullbackCone.isLimitOfFlip (CategoryTheory.Limits.pullbackIsPullback g (𝒰.map i))) (CategoryTheory.Limits.PullbackCone.isLimitOfFlip (CategoryTheory.Limits.pullbackIsPullback (CategoryTheory.Limits.pullback.snd g (𝒰.map i)) (CategoryTheory.Limits.pullback.snd f (𝒰.map i)))); AlgebraicGeometry.Scheme.openCoverOfIsIso (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry (CategoryTheory.Limits.pullback.snd f (𝒰.map i)) (CategoryTheory.Limits.pullback.snd g (𝒰.map i))).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.isoLimitCone { cone := CategoryTheory.Limits.PullbackCone.mk (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.snd g (𝒰.map i)) (CategoryTheory.Limits.pullback.snd f (𝒰.map i))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.snd g (𝒰.map i)) (CategoryTheory.Limits.pullback.snd f (𝒰.map i))) (CategoryTheory.Limits.pullback.fst g (𝒰.map i))) , isLimit := this }).inv (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f (𝒰.map i)) (𝒰.map i)) g (CategoryTheory.CategoryStruct.comp ((𝒰.pullbackCover f).map i) f) g (CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback f (𝒰.map i))) (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.id Z) )))) i).J) :
                                (AlgebraicGeometry.Scheme.Pullback.openCoverOfBase' 𝒰 f g).map x = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry (CategoryTheory.Limits.pullback.snd f (𝒰.map x.fst)) (CategoryTheory.Limits.pullback.snd g (𝒰.map x.fst))).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.isoLimitCone { cone := CategoryTheory.Limits.PullbackCone.mk (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.snd g (𝒰.map x.fst)) (CategoryTheory.Limits.pullback.snd f (𝒰.map x.fst))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.snd g (𝒰.map x.fst)) (CategoryTheory.Limits.pullback.snd f (𝒰.map x.fst))) (CategoryTheory.Limits.pullback.fst g (𝒰.map x.fst))) , isLimit := CategoryTheory.Limits.bigSquareIsPullback (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.snd g (𝒰.map x.fst)) (CategoryTheory.Limits.pullback.snd f (𝒰.map x.fst))) (CategoryTheory.Limits.pullback.fst g (𝒰.map x.fst)) (CategoryTheory.Limits.pullback.snd f (𝒰.map x.fst)) (𝒰.map x.fst) (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.snd g (𝒰.map x.fst)) (CategoryTheory.Limits.pullback.snd f (𝒰.map x.fst))) (CategoryTheory.Limits.pullback.snd g (𝒰.map x.fst)) g (CategoryTheory.Limits.PullbackCone.isLimitOfFlip (CategoryTheory.Limits.pullbackIsPullback g (𝒰.map x.fst))) (CategoryTheory.Limits.PullbackCone.isLimitOfFlip (CategoryTheory.Limits.pullbackIsPullback (CategoryTheory.Limits.pullback.snd g (𝒰.map x.fst)) (CategoryTheory.Limits.pullback.snd f (𝒰.map x.fst)))) }).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f (𝒰.map x.fst)) (𝒰.map x.fst)) g (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f (𝒰.map x.fst)) f) g (CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback f (𝒰.map x.fst))) (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.id Z) ) (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f (𝒰.map x.fst)) f) g f g (CategoryTheory.Limits.pullback.fst f (𝒰.map x.fst)) (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.id Z) )))

                                (Implementation). Use openCoverOfBase instead.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For

                                  Given an open cover { Zᵢ } of Z, then X ×[Z] Y is covered by Xᵢ ×[Zᵢ] Yᵢ, where Xᵢ = X ×[Z] Zᵢ and Yᵢ = Y ×[Z] Zᵢ is the preimage of Zᵢ in X and Y.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For

                                    The isomorphism between the fiber product of two schemes Spec S and Spec T over a scheme Spec R and the Spec of the tensor product S ⊗[R] T.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      @[simp]

                                      The composition of the inverse of the isomorphism pullbackSepcIso R S T (from the pullback of Spec S ⟶ Spec R and Spec T ⟶ Spec R to Spec (S ⊗[R] T)) with the first projection is the morphism Spec (S ⊗[R] T) ⟶ Spec S obtained by applying Spec.map to the ring morphism s ↦ s ⊗ₜ[R] 1.

                                      @[simp]

                                      The composition of the inverse of the isomorphism pullbackSepcIso R S T (from the pullback of Spec S ⟶ Spec R and Spec T ⟶ Spec R to Spec (S ⊗[R] T)) with the second projection is the morphism Spec (S ⊗[R] T) ⟶ Spec T obtained by applying Spec.map to the ring morphism t ↦ 1 ⊗ₜ[R] t.

                                      @[simp]

                                      The composition of the isomorphism pullbackSepcIso R S T (from the pullback of Spec S ⟶ Spec R and Spec T ⟶ Spec R to Spec (S ⊗[R] T)) with the morphism Spec (S ⊗[R] T) ⟶ Spec S obtained by applying Spec.map to the ring morphism s ↦ s ⊗ₜ[R] 1 is the first projection.

                                      @[simp]

                                      The composition of the isomorphism pullbackSepcIso R S T (from the pullback of Spec S ⟶ Spec R and Spec T ⟶ Spec R to Spec (S ⊗[R] T)) with the morphism Spec (S ⊗[R] T) ⟶ Spec T obtained by applying Spec.map to the ring morphism t ↦ 1 ⊗ₜ[R] t is the second projection.