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 Y Z : Scheme} (𝒰 : X.OpenCover) (f : X Z) (g : Y Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i 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.
def AlgebraicGeometry.Scheme.Pullback.t {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X Z) (g : Y Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i j : 𝒰.J) :
v 𝒰 f g i j v 𝒰 f g j i

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.
theorem AlgebraicGeometry.Scheme.Pullback.t_id {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X Z) (g : Y Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i : 𝒰.J) :
t 𝒰 f g i i = CategoryTheory.CategoryStruct.id (v 𝒰 f g i i)
@[reducible, inline]
abbrev AlgebraicGeometry.Scheme.Pullback.fV {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X Z) (g : Y Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i j : 𝒰.J) :

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.
def AlgebraicGeometry.Scheme.Pullback.t' {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X Z) (g : Y Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i j k : 𝒰.J) :
CategoryTheory.Limits.pullback (fV 𝒰 f g i j) (fV 𝒰 f g i k) CategoryTheory.Limits.pullback (fV 𝒰 f g j k) (fV 𝒰 f g j i)

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.
theorem AlgebraicGeometry.Scheme.Pullback.cocycle {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X Z) (g : Y Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i j k : 𝒰.J) :
CategoryTheory.CategoryStruct.comp (t' 𝒰 f g i j k) (CategoryTheory.CategoryStruct.comp (t' 𝒰 f g j k i) (t' 𝒰 f g k i j)) = CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback (fV 𝒰 f g i j) (fV 𝒰 f g i k))

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

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem AlgebraicGeometry.Scheme.Pullback.gluing_f {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X Z) (g : Y Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (x✝ x✝¹ : 𝒰.J) :
@[simp]
theorem AlgebraicGeometry.Scheme.Pullback.gluing_V {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X Z) (g : Y Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (x✝ : 𝒰.J × 𝒰.J) :
(gluing 𝒰 f g).V x✝ = match x✝ with | (i, j) => v 𝒰 f g i j
@[simp]
theorem AlgebraicGeometry.Scheme.Pullback.gluing_t {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X Z) (g : Y Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i j : 𝒰.J) :
(gluing 𝒰 f g).t i j = t 𝒰 f g i j
@[simp]
theorem AlgebraicGeometry.Scheme.Pullback.gluing_t' {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X Z) (g : Y Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i j k : 𝒰.J) :
(gluing 𝒰 f g).t' i j k = t' 𝒰 f g i j k
@[simp]
theorem AlgebraicGeometry.Scheme.Pullback.gluing_J {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X Z) (g : Y Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] :
(gluing 𝒰 f g).J = 𝒰.J
@[simp]
theorem AlgebraicGeometry.Scheme.Pullback.gluing_ι {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X Z) (g : Y Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (j : 𝒰.J) :
def AlgebraicGeometry.Scheme.Pullback.p1 {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X Z) (g : Y Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] :
(gluing 𝒰 f g).glued X

The first projection from the glued scheme into X.

Equations
  • One or more equations did not get rendered due to their size.
def AlgebraicGeometry.Scheme.Pullback.p2 {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X Z) (g : Y Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] :
(gluing 𝒰 f g).glued Y

The second projection from the glued scheme into Y.

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

(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.

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.
def AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X Z) (g : Y Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i j : 𝒰.J) :
CategoryTheory.Limits.pullback (CategoryTheory.Limits.pullback.fst (p1 𝒰 f g) (𝒰.map i)) ((gluing 𝒰 f g).ι j) v 𝒰 f g j i

(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.

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.
@[simp]

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.

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.
@[simp]
theorem AlgebraicGeometry.Scheme.Pullback.openCoverOfLeft_J {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X Z) (g : Y Z) :
(openCoverOfLeft 𝒰 f g).J = 𝒰.J

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.
@[simp]
theorem AlgebraicGeometry.Scheme.Pullback.openCoverOfRight_J {X Y Z : Scheme} (𝒰 : Y.OpenCover) (f : X Z) (g : Y Z) :
(openCoverOfRight 𝒰 f g).J = 𝒰.J

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.
@[simp]
theorem AlgebraicGeometry.Scheme.Pullback.openCoverOfLeftRight_obj {X Y Z : Scheme} (𝒰X : X.OpenCover) (𝒰Y : Y.OpenCover) (f : X Z) (g : Y Z) (ij : 𝒰X.J × 𝒰Y.J) :
@[simp]
theorem AlgebraicGeometry.Scheme.Pullback.openCoverOfLeftRight_map {X Y Z : Scheme} (𝒰X : X.OpenCover) (𝒰Y : Y.OpenCover) (f : X Z) (g : Y Z) (ij : 𝒰X.J × 𝒰Y.J) :
@[simp]
theorem AlgebraicGeometry.Scheme.Pullback.openCoverOfLeftRight_J {X Y Z : Scheme} (𝒰X : X.OpenCover) (𝒰Y : Y.OpenCover) (f : X Z) (g : Y Z) :
(openCoverOfLeftRight 𝒰X 𝒰Y f g).J = (𝒰X.J × 𝒰Y.J)

(Implementation). Use openCoverOfBase instead.

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem AlgebraicGeometry.Scheme.Pullback.openCoverOfBase'_map {X Y Z : Scheme} (𝒰 : Z.OpenCover) (f : X Z) (g : Y Z) (x : (i : (openCoverOfLeft (Cover.pullbackCover 𝒰 f) f g).J) × ((fun (i : (openCoverOfLeft (Cover.pullbackCover 𝒰 f) f g).J) => coverOfIsIso (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 := .cone, isLimit := .isLimit }).inv (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f (𝒰.map i)) (𝒰.map i)) g (CategoryTheory.CategoryStruct.comp ((Cover.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) :

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.
@[simp]
theorem AlgebraicGeometry.Scheme.Pullback.openCoverOfBase_J {X Y Z : Scheme} (𝒰 : Z.OpenCover) (f : X Z) (g : Y Z) :
(openCoverOfBase 𝒰 f g).J = 𝒰.J

Given 𝒰 i covering Y and 𝒱 i j covering 𝒰 i, this is the open cover 𝒱 i j₁ ×[𝒰 i] 𝒱 i j₂ ranging over all i, j₁, j₂.

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

The image of 𝒱 i j₁ ×[𝒰 i] 𝒱 i j₂ in diagonalCover with j₁ = j₂

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

The restriction of the diagonal X ⟶ X ×ₛ X to 𝒱 i j ×[𝒰 i] 𝒱 i j is the diagonal 𝒱 i j ⟶ 𝒱 i j ×[𝒰 i] 𝒱 i j.

Equations
  • One or more equations did not get rendered due to their size.
instance AlgebraicGeometry.Scheme.pullback_map_isOpenImmersion {X Y S X' Y' S' : Scheme} (f : X S) (g : Y S) (f' : X' S') (g' : Y' S') (i₁ : X X') (i₂ : Y Y') (i₃ : S S') (e₁ : CategoryTheory.CategoryStruct.comp f i₃ = CategoryTheory.CategoryStruct.comp i₁ f') (e₂ : CategoryTheory.CategoryStruct.comp g i₃ = CategoryTheory.CategoryStruct.comp i₂ g') [IsOpenImmersion i₁] [IsOpenImmersion i₂] [CategoryTheory.Mono i₃] :
IsOpenImmersion (CategoryTheory.Limits.pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂)

The isomorphism between the fibred 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.
@[simp]

The composition of the inverse of the isomorphism pullbackSpecIso 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 pullbackSpecIso 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 pullbackSpecIso 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 pullbackSpecIso 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.

theorem AlgebraicGeometry.isPullback_Spec_map_isPushout {A B C P : CommRingCat} (f : A B) (g : A C) (inl : B P) (inr : C P) (h : CategoryTheory.IsPushout f g inl inr) :