mathlib documentation

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

noncomputable def algebraic_geometry.Scheme.pullback.V {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [∀ (i : 𝒰.J), category_theory.limits.has_pullback (𝒰.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
noncomputable def algebraic_geometry.Scheme.pullback.t {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [∀ (i : 𝒰.J), category_theory.limits.has_pullback (𝒰.map i f) g] (i j : 𝒰.J) :

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
theorem algebraic_geometry.Scheme.pullback.t_id {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [∀ (i : 𝒰.J), category_theory.limits.has_pullback (𝒰.map i f) g] (i : 𝒰.J) :
@[reducible]
noncomputable def algebraic_geometry.Scheme.pullback.fV {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [∀ (i : 𝒰.J), category_theory.limits.has_pullback (𝒰.map i f) g] (i j : 𝒰.J) :

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

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
@[simp]
theorem algebraic_geometry.Scheme.pullback.gluing_to_glue_data_V {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [∀ (i : 𝒰.J), category_theory.limits.has_pullback (𝒰.map i f) g] (_x : 𝒰.J × 𝒰.J) :
(algebraic_geometry.Scheme.pullback.gluing 𝒰 f g).to_glue_data.V _x = algebraic_geometry.Scheme.pullback.gluing._match_1 𝒰 f g _x

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

Equations

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

This is used in glued_lift.

Equations

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

Equations

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

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

Equations

(Implementation). Use open_cover_of_base instead.

Equations