# mathlib3documentation

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), 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), g] (i j : 𝒰.J) :
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
@[simp]
theorem algebraic_geometry.Scheme.pullback.t_fst_fst_assoc {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g] (i j : 𝒰.J) (f' : 𝒰.obj j X') :
@[simp]
theorem algebraic_geometry.Scheme.pullback.t_fst_fst {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g] (i j : 𝒰.J) :
@[simp]
theorem algebraic_geometry.Scheme.pullback.t_fst_snd {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g] (i j : 𝒰.J) :
@[simp]
theorem algebraic_geometry.Scheme.pullback.t_fst_snd_assoc {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g] (i j : 𝒰.J) (f' : Y X') :
@[simp]
theorem algebraic_geometry.Scheme.pullback.t_snd {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g] (i j : 𝒰.J) :
@[simp]
theorem algebraic_geometry.Scheme.pullback.t_snd_assoc {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g] (i j : 𝒰.J) (f' : 𝒰.obj i X') :
theorem algebraic_geometry.Scheme.pullback.t_id {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g] (i : 𝒰.J) :
i = 𝟙 i)
@[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), g] (i j : 𝒰.J) :

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

noncomputable def algebraic_geometry.Scheme.pullback.t' {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g] (i j k : 𝒰.J) :

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.t'_fst_fst_fst {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g] (i j k : 𝒰.J) :
@[simp]
theorem algebraic_geometry.Scheme.pullback.t'_fst_fst_fst_assoc {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g] (i j k : 𝒰.J) (f' : 𝒰.obj j X') :
@[simp]
theorem algebraic_geometry.Scheme.pullback.t'_fst_fst_snd_assoc {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g] (i j k : 𝒰.J) (f' : Y X') :
@[simp]
theorem algebraic_geometry.Scheme.pullback.t'_fst_fst_snd {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g] (i j k : 𝒰.J) :
@[simp]
theorem algebraic_geometry.Scheme.pullback.t'_fst_snd_assoc {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g] (i j k : 𝒰.J) (f' : 𝒰.obj k X') :
@[simp]
theorem algebraic_geometry.Scheme.pullback.t'_fst_snd {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g] (i j k : 𝒰.J) :
@[simp]
theorem algebraic_geometry.Scheme.pullback.t'_snd_fst_fst {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g] (i j k : 𝒰.J) :
@[simp]
theorem algebraic_geometry.Scheme.pullback.t'_snd_fst_fst_assoc {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g] (i j k : 𝒰.J) (f' : 𝒰.obj j X') :
@[simp]
theorem algebraic_geometry.Scheme.pullback.t'_snd_fst_snd {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g] (i j k : 𝒰.J) :
@[simp]
theorem algebraic_geometry.Scheme.pullback.t'_snd_fst_snd_assoc {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g] (i j k : 𝒰.J) (f' : Y X') :
@[simp]
theorem algebraic_geometry.Scheme.pullback.t'_snd_snd {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g] (i j k : 𝒰.J) :
@[simp]
theorem algebraic_geometry.Scheme.pullback.t'_snd_snd_assoc {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g] (i j k : 𝒰.J) (f' : 𝒰.obj i X') :
theorem algebraic_geometry.Scheme.pullback.cocycle_fst_fst_fst {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g] (i j k : 𝒰.J) :
theorem algebraic_geometry.Scheme.pullback.cocycle_fst_fst_snd {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g] (i j k : 𝒰.J) :
theorem algebraic_geometry.Scheme.pullback.cocycle_fst_snd {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g] (i j k : 𝒰.J) :
theorem algebraic_geometry.Scheme.pullback.cocycle_snd_fst_fst {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g] (i j k : 𝒰.J) :
theorem algebraic_geometry.Scheme.pullback.cocycle_snd_fst_snd {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g] (i j k : 𝒰.J) :
theorem algebraic_geometry.Scheme.pullback.cocycle_snd_snd {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g] (i j k : 𝒰.J) :
theorem algebraic_geometry.Scheme.pullback.cocycle {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g] (i j k : 𝒰.J) :
k i j = 𝟙 k))
@[simp]
theorem algebraic_geometry.Scheme.pullback.gluing_to_glue_data_U {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g] (i : 𝒰.J) :
@[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), g] (_x : 𝒰.J × 𝒰.J) :
= algebraic_geometry.Scheme.pullback.gluing._match_1 𝒰 f g _x
noncomputable def algebraic_geometry.Scheme.pullback.gluing {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g] :

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

Equations
@[simp]
theorem algebraic_geometry.Scheme.pullback.gluing_to_glue_data_t' {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g] (i j k : 𝒰.J) :
k = k
@[simp]
theorem algebraic_geometry.Scheme.pullback.gluing_to_glue_data_J {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g] :
@[simp]
theorem algebraic_geometry.Scheme.pullback.gluing_to_glue_data_t {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g] (i j : 𝒰.J) :
= j
@[simp]
theorem algebraic_geometry.Scheme.pullback.gluing_to_glue_data_f {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g] (i j : 𝒰.J) :
noncomputable def algebraic_geometry.Scheme.pullback.p1 {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g] :

The first projection from the glued scheme into `X`.

Equations
noncomputable def algebraic_geometry.Scheme.pullback.p2 {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g] :

The second projection from the glued scheme into `Y`.

Equations
theorem algebraic_geometry.Scheme.pullback.p_comm {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g] :
noncomputable def algebraic_geometry.Scheme.pullback.glued_lift_pullback_map {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g] (i j : 𝒰.J) :
((𝒰.pullback_cover s.fst).map j) (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 `glued_lift`.

Equations
theorem algebraic_geometry.Scheme.pullback.glued_lift_pullback_map_fst {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g] (i j : 𝒰.J) :
= category_theory.limits.pullback.fst .hom (𝒰.map i f) g (𝟙 (𝒰.obj i)) s.snd f _ _
theorem algebraic_geometry.Scheme.pullback.glued_lift_pullback_map_fst_assoc {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g] (i j : 𝒰.J) (f' : category_theory.limits.pullback (𝒰.map i f) g X') :
= category_theory.limits.pullback.fst .hom (𝒰.map i f) g (𝟙 (𝒰.obj i)) s.snd f _ _ f'
theorem algebraic_geometry.Scheme.pullback.glued_lift_pullback_map_snd_assoc {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g] (i j : 𝒰.J) (f' : 𝒰.obj j X') :
theorem algebraic_geometry.Scheme.pullback.glued_lift_pullback_map_snd {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g] (i j : 𝒰.J) :
noncomputable def algebraic_geometry.Scheme.pullback.glued_lift {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g]  :

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
theorem algebraic_geometry.Scheme.pullback.glued_lift_p1 {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g]  :
theorem algebraic_geometry.Scheme.pullback.glued_lift_p2 {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g]  :
noncomputable def algebraic_geometry.Scheme.pullback.pullback_fst_ι_to_V {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g] (i j : 𝒰.J) :

(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
@[simp]
theorem algebraic_geometry.Scheme.pullback.pullback_fst_ι_to_V_fst_assoc {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g] (i j : 𝒰.J) (f' : category_theory.limits.pullback (𝒰.map j f) g X') :
@[simp]
theorem algebraic_geometry.Scheme.pullback.pullback_fst_ι_to_V_fst {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g] (i j : 𝒰.J) :
@[simp]
theorem algebraic_geometry.Scheme.pullback.pullback_fst_ι_to_V_snd_assoc {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g] (i j : 𝒰.J) (f' : 𝒰.obj i X') :
@[simp]
theorem algebraic_geometry.Scheme.pullback.pullback_fst_ι_to_V_snd {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g] (i j : 𝒰.J) :
theorem algebraic_geometry.Scheme.pullback.lift_comp_ι {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g] (i : 𝒰.J) :

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`

noncomputable def algebraic_geometry.Scheme.pullback.pullback_p1_iso {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g] (i : 𝒰.J) :

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
@[simp]
theorem algebraic_geometry.Scheme.pullback.pullback_p1_iso_hom_fst_assoc {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g] (i : 𝒰.J) (f' : 𝒰.obj i X') :
@[simp]
theorem algebraic_geometry.Scheme.pullback.pullback_p1_iso_hom_fst {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g] (i : 𝒰.J) :
@[simp]
theorem algebraic_geometry.Scheme.pullback.pullback_p1_iso_hom_snd_assoc {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g] (i : 𝒰.J) (f' : Y X') :
@[simp]
theorem algebraic_geometry.Scheme.pullback.pullback_p1_iso_hom_snd {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g] (i : 𝒰.J) :
@[simp]
theorem algebraic_geometry.Scheme.pullback.pullback_p1_iso_inv_fst_assoc {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g] (i : 𝒰.J) (f' : X') :
@[simp]
theorem algebraic_geometry.Scheme.pullback.pullback_p1_iso_inv_fst {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g] (i : 𝒰.J) :
@[simp]
theorem algebraic_geometry.Scheme.pullback.pullback_p1_iso_inv_snd_assoc {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g] (i : 𝒰.J) (f' : 𝒰.obj i X') :
@[simp]
theorem algebraic_geometry.Scheme.pullback.pullback_p1_iso_inv_snd {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g] (i : 𝒰.J) :
@[simp]
theorem algebraic_geometry.Scheme.pullback.pullback_p1_iso_hom_ι_assoc {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g] (i : 𝒰.J) (f' : X') :
@[simp]
theorem algebraic_geometry.Scheme.pullback.pullback_p1_iso_hom_ι {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g] (i : 𝒰.J) :
noncomputable def algebraic_geometry.Scheme.pullback.glued_is_limit {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g] :

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

Equations
theorem algebraic_geometry.Scheme.pullback.has_pullback_of_cover {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) [ (i : 𝒰.J), g] :
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[simp]
theorem algebraic_geometry.Scheme.pullback.open_cover_of_left_map {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) (i : 𝒰.J) :
= g f g (𝒰.map i) (𝟙 Y) (𝟙 Z) _ _
noncomputable def algebraic_geometry.Scheme.pullback.open_cover_of_left {X Y Z : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X Z) (g : Y Z) :

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

Equations
@[simp]
@[simp]
theorem algebraic_geometry.Scheme.pullback.open_cover_of_right_map {X Y Z : algebraic_geometry.Scheme} (𝒰 : Y.open_cover) (f : X Z) (g : Y Z) (i : 𝒰.J) :
= (𝒰.map i g) f g (𝟙 X) (𝒰.map i) (𝟙 Z) _ _
@[simp]
theorem algebraic_geometry.Scheme.pullback.open_cover_of_right_obj {X Y Z : algebraic_geometry.Scheme} (𝒰 : Y.open_cover) (f : X Z) (g : Y Z) (i : 𝒰.J) :
noncomputable def algebraic_geometry.Scheme.pullback.open_cover_of_right {X Y Z : algebraic_geometry.Scheme} (𝒰 : Y.open_cover) (f : X Z) (g : Y Z) :

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

(Implementation). Use `open_cover_of_base` instead.

Equations
@[simp]
theorem algebraic_geometry.Scheme.pullback.open_cover_of_base_map {X Y Z : algebraic_geometry.Scheme} (𝒰 : Z.open_cover) (f : X Z) (g : Y Z) (i : 𝒰.J) :
@[simp]
theorem algebraic_geometry.Scheme.pullback.open_cover_of_base_obj {X Y Z : algebraic_geometry.Scheme} (𝒰 : Z.open_cover) (f : X Z) (g : Y Z) (i : 𝒰.J) :
noncomputable def algebraic_geometry.Scheme.pullback.open_cover_of_base {X Y Z : algebraic_geometry.Scheme} (𝒰 : Z.open_cover) (f : X Z) (g : Y Z) :

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
@[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 g' i₁ i₂ i₃ e₁ e₂)