mathlib3 documentation

algebraic_geometry.pullbacks

Fibred products of schemes #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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
@[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
@[simp]
theorem algebraic_geometry.Scheme.pullback.open_cover_of_left_right_map {X Y Z : algebraic_geometry.Scheme} (𝒰X : X.open_cover) (𝒰Y : Y.open_cover) (f : X Z) (g : Y Z) (ij : 𝒰X.J × 𝒰Y.J) :
(algebraic_geometry.Scheme.pullback.open_cover_of_left_right 𝒰X 𝒰Y f g).map ij = category_theory.limits.pullback.map (𝒰X.map ij.fst f) (𝒰Y.map ij.snd g) f g (𝒰X.map ij.fst) (𝒰Y.map ij.snd) (𝟙 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
@[simp]

(Implementation). Use open_cover_of_base instead.

Equations
@[protected, instance]
def algebraic_geometry.category_theory.limits.pullback.map.is_open_immersion {X Y S X' Y' S' : algebraic_geometry.Scheme} (f : X S) (g : Y S) (f' : X' S') (g' : Y' S') (i₁ : X X') (i₂ : Y Y') (i₃ : S S') (e₁ : f i₃ = i₁ f') (e₂ : g i₃ = i₂ g') [algebraic_geometry.is_open_immersion i₁] [algebraic_geometry.is_open_immersion i₂] [category_theory.mono i₃] :