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
- algebraic_geometry.Scheme.pullback.V 𝒰 f g i j = category_theory.limits.pullback (category_theory.limits.pullback.fst ≫ 𝒰.map i) (𝒰.map j)
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) :
algebraic_geometry.Scheme.pullback.V 𝒰 f g i j ⟶ algebraic_geometry.Scheme.pullback.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
- algebraic_geometry.Scheme.pullback.t 𝒰 f g i j = (category_theory.limits.pullback_symmetry (category_theory.limits.pullback.fst ≫ 𝒰.map i) (𝒰.map j)).hom ≫ (category_theory.limits.pullback_assoc (𝒰.map j) (𝒰.map i) (𝒰.map i ≫ f) g).inv ≫ id ((category_theory.limits.pullback.map (category_theory.limits.pullback.snd ≫ 𝒰.map i ≫ f) g (category_theory.limits.pullback.snd ≫ 𝒰.map j ≫ f) g (category_theory.limits.pullback_symmetry (𝒰.map j) (𝒰.map i)).hom (𝟙 Y) (𝟙 Z) _ _ ≫ (category_theory.limits.pullback_assoc (𝒰.map i) (𝒰.map j) (𝒰.map j ≫ f) g).hom) ≫ (category_theory.limits.pullback_symmetry (𝒰.map i) (category_theory.limits.pullback.fst ≫ 𝒰.map j)).hom)
@[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), category_theory.limits.has_pullback (𝒰.map i ≫ f) g]
(i j : 𝒰.J)
{X' : algebraic_geometry.Scheme}
(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), category_theory.limits.has_pullback (𝒰.map i ≫ f) 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), category_theory.limits.has_pullback (𝒰.map i ≫ f) 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), category_theory.limits.has_pullback (𝒰.map i ≫ f) g]
(i j : 𝒰.J)
{X' : algebraic_geometry.Scheme}
(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), category_theory.limits.has_pullback (𝒰.map i ≫ f) 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), category_theory.limits.has_pullback (𝒰.map i ≫ f) g]
(i j : 𝒰.J)
{X' : algebraic_geometry.Scheme}
(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), category_theory.limits.has_pullback (𝒰.map i ≫ f) g]
(i : 𝒰.J) :
algebraic_geometry.Scheme.pullback.t 𝒰 f g i i = 𝟙 (algebraic_geometry.Scheme.pullback.V 𝒰 f g 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), category_theory.limits.has_pullback (𝒰.map i ≫ f) g]
(i j : 𝒰.J) :
algebraic_geometry.Scheme.pullback.V 𝒰 f g i j ⟶ category_theory.limits.pullback (𝒰.map i ≫ f) g
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), category_theory.limits.has_pullback (𝒰.map i ≫ f) g]
(i j k : 𝒰.J) :
category_theory.limits.pullback (algebraic_geometry.Scheme.pullback.fV 𝒰 f g i j) (algebraic_geometry.Scheme.pullback.fV 𝒰 f g i k) ⟶ category_theory.limits.pullback (algebraic_geometry.Scheme.pullback.fV 𝒰 f g j k) (algebraic_geometry.Scheme.pullback.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
- algebraic_geometry.Scheme.pullback.t' 𝒰 f g i j k = (category_theory.limits.pullback_right_pullback_fst_iso (category_theory.limits.pullback.fst ≫ 𝒰.map i) (𝒰.map k) (algebraic_geometry.Scheme.pullback.fV 𝒰 f g i j)).hom ≫ (category_theory.limits.pullback.map (algebraic_geometry.Scheme.pullback.fV 𝒰 f g i j ≫ category_theory.limits.pullback.fst ≫ 𝒰.map i) (𝒰.map k) (algebraic_geometry.Scheme.pullback.fV 𝒰 f g j i ≫ category_theory.limits.pullback.fst ≫ 𝒰.map j) (𝒰.map k) (algebraic_geometry.Scheme.pullback.t 𝒰 f g i j) (𝟙 (𝒰.obj k)) (𝟙 X) _ _ ≫ (category_theory.limits.pullback_right_pullback_fst_iso (category_theory.limits.pullback.fst ≫ 𝒰.map j) (𝒰.map k) (algebraic_geometry.Scheme.pullback.fV 𝒰 f g j i)).inv) ≫ (category_theory.limits.pullback_symmetry (algebraic_geometry.Scheme.pullback.fV 𝒰 f g j i) (algebraic_geometry.Scheme.pullback.fV 𝒰 f g j k)).hom
@[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), category_theory.limits.has_pullback (𝒰.map i ≫ f) 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), category_theory.limits.has_pullback (𝒰.map i ≫ f) g]
(i j k : 𝒰.J)
{X' : algebraic_geometry.Scheme}
(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), category_theory.limits.has_pullback (𝒰.map i ≫ f) g]
(i j k : 𝒰.J)
{X' : algebraic_geometry.Scheme}
(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), category_theory.limits.has_pullback (𝒰.map i ≫ f) 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), category_theory.limits.has_pullback (𝒰.map i ≫ f) g]
(i j k : 𝒰.J)
{X' : algebraic_geometry.Scheme}
(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), category_theory.limits.has_pullback (𝒰.map i ≫ f) 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), category_theory.limits.has_pullback (𝒰.map i ≫ f) 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), category_theory.limits.has_pullback (𝒰.map i ≫ f) g]
(i j k : 𝒰.J)
{X' : algebraic_geometry.Scheme}
(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), category_theory.limits.has_pullback (𝒰.map i ≫ f) 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), category_theory.limits.has_pullback (𝒰.map i ≫ f) g]
(i j k : 𝒰.J)
{X' : algebraic_geometry.Scheme}
(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), category_theory.limits.has_pullback (𝒰.map i ≫ f) 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), category_theory.limits.has_pullback (𝒰.map i ≫ f) g]
(i j k : 𝒰.J)
{X' : algebraic_geometry.Scheme}
(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), category_theory.limits.has_pullback (𝒰.map i ≫ f) g]
(i j k : 𝒰.J) :
algebraic_geometry.Scheme.pullback.t' 𝒰 f g i j k ≫ algebraic_geometry.Scheme.pullback.t' 𝒰 f g j k i ≫ algebraic_geometry.Scheme.pullback.t' 𝒰 f g k i j ≫ category_theory.limits.pullback.fst ≫ category_theory.limits.pullback.fst ≫ category_theory.limits.pullback.fst = category_theory.limits.pullback.fst ≫ category_theory.limits.pullback.fst ≫ category_theory.limits.pullback.fst
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), category_theory.limits.has_pullback (𝒰.map i ≫ f) g]
(i j k : 𝒰.J) :
algebraic_geometry.Scheme.pullback.t' 𝒰 f g i j k ≫ algebraic_geometry.Scheme.pullback.t' 𝒰 f g j k i ≫ algebraic_geometry.Scheme.pullback.t' 𝒰 f g k i j ≫ category_theory.limits.pullback.fst ≫ category_theory.limits.pullback.fst ≫ category_theory.limits.pullback.snd = category_theory.limits.pullback.fst ≫ category_theory.limits.pullback.fst ≫ category_theory.limits.pullback.snd
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), category_theory.limits.has_pullback (𝒰.map i ≫ f) g]
(i j k : 𝒰.J) :
algebraic_geometry.Scheme.pullback.t' 𝒰 f g i j k ≫ algebraic_geometry.Scheme.pullback.t' 𝒰 f g j k i ≫ algebraic_geometry.Scheme.pullback.t' 𝒰 f g k i j ≫ category_theory.limits.pullback.fst ≫ category_theory.limits.pullback.snd = category_theory.limits.pullback.fst ≫ category_theory.limits.pullback.snd
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), category_theory.limits.has_pullback (𝒰.map i ≫ f) g]
(i j k : 𝒰.J) :
algebraic_geometry.Scheme.pullback.t' 𝒰 f g i j k ≫ algebraic_geometry.Scheme.pullback.t' 𝒰 f g j k i ≫ algebraic_geometry.Scheme.pullback.t' 𝒰 f g k i j ≫ category_theory.limits.pullback.snd ≫ category_theory.limits.pullback.fst ≫ category_theory.limits.pullback.fst = category_theory.limits.pullback.snd ≫ category_theory.limits.pullback.fst ≫ category_theory.limits.pullback.fst
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), category_theory.limits.has_pullback (𝒰.map i ≫ f) g]
(i j k : 𝒰.J) :
algebraic_geometry.Scheme.pullback.t' 𝒰 f g i j k ≫ algebraic_geometry.Scheme.pullback.t' 𝒰 f g j k i ≫ algebraic_geometry.Scheme.pullback.t' 𝒰 f g k i j ≫ category_theory.limits.pullback.snd ≫ category_theory.limits.pullback.fst ≫ category_theory.limits.pullback.snd = category_theory.limits.pullback.snd ≫ category_theory.limits.pullback.fst ≫ category_theory.limits.pullback.snd
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), category_theory.limits.has_pullback (𝒰.map i ≫ f) g]
(i j k : 𝒰.J) :
algebraic_geometry.Scheme.pullback.t' 𝒰 f g i j k ≫ algebraic_geometry.Scheme.pullback.t' 𝒰 f g j k i ≫ algebraic_geometry.Scheme.pullback.t' 𝒰 f g k i j ≫ category_theory.limits.pullback.snd ≫ category_theory.limits.pullback.snd = category_theory.limits.pullback.snd ≫ category_theory.limits.pullback.snd
theorem
algebraic_geometry.Scheme.pullback.cocycle
{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 k : 𝒰.J) :
algebraic_geometry.Scheme.pullback.t' 𝒰 f g i j k ≫ algebraic_geometry.Scheme.pullback.t' 𝒰 f g j k i ≫ algebraic_geometry.Scheme.pullback.t' 𝒰 f g k i j = 𝟙 (category_theory.limits.pullback (algebraic_geometry.Scheme.pullback.fV 𝒰 f g i j) (algebraic_geometry.Scheme.pullback.fV 𝒰 f g i 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), category_theory.limits.has_pullback (𝒰.map i ≫ f) g]
(i : 𝒰.J) :
(algebraic_geometry.Scheme.pullback.gluing 𝒰 f g).to_glue_data.U i = category_theory.limits.pullback (𝒰.map i ≫ f) g
@[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
noncomputable
def
algebraic_geometry.Scheme.pullback.gluing
{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] :
Given Uᵢ ×[Z] Y, this is the glued fibered product X ×[Z] Y.
Equations
- algebraic_geometry.Scheme.pullback.gluing 𝒰 f g = {to_glue_data := {J := 𝒰.J, U := λ (i : 𝒰.J), category_theory.limits.pullback (𝒰.map i ≫ f) g, V := λ (_x : 𝒰.J × 𝒰.J), algebraic_geometry.Scheme.pullback.gluing._match_1 𝒰 f g _x, f := λ (i j : 𝒰.J), category_theory.limits.pullback.fst, f_mono := _, f_has_pullback := _, f_id := _, t := λ (i j : 𝒰.J), algebraic_geometry.Scheme.pullback.t 𝒰 f g i j, t_id := _, t' := λ (i j k : 𝒰.J), algebraic_geometry.Scheme.pullback.t' 𝒰 f g i j k, t_fac := _, cocycle := _}, f_open := _}
- algebraic_geometry.Scheme.pullback.gluing._match_1 𝒰 f g (i, j) = algebraic_geometry.Scheme.pullback.V 𝒰 f g i j
@[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), category_theory.limits.has_pullback (𝒰.map i ≫ f) g]
(i j k : 𝒰.J) :
(algebraic_geometry.Scheme.pullback.gluing 𝒰 f g).to_glue_data.t' i j k = algebraic_geometry.Scheme.pullback.t' 𝒰 f g i j 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), category_theory.limits.has_pullback (𝒰.map i ≫ f) g] :
(algebraic_geometry.Scheme.pullback.gluing 𝒰 f g).to_glue_data.J = 𝒰.J
@[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), category_theory.limits.has_pullback (𝒰.map i ≫ f) g]
(i j : 𝒰.J) :
(algebraic_geometry.Scheme.pullback.gluing 𝒰 f g).to_glue_data.t i j = algebraic_geometry.Scheme.pullback.t 𝒰 f g i 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), category_theory.limits.has_pullback (𝒰.map i ≫ f) 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), category_theory.limits.has_pullback (𝒰.map i ≫ f) g] :
(algebraic_geometry.Scheme.pullback.gluing 𝒰 f g).glued ⟶ X
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), category_theory.limits.has_pullback (𝒰.map i ≫ f) g] :
(algebraic_geometry.Scheme.pullback.gluing 𝒰 f g).glued ⟶ Y
The second projection from the glued scheme into Y.
theorem
algebraic_geometry.Scheme.pullback.p_comm
{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] :
algebraic_geometry.Scheme.pullback.p1 𝒰 f g ≫ f = algebraic_geometry.Scheme.pullback.p2 𝒰 f g ≫ 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), category_theory.limits.has_pullback (𝒰.map i ≫ f) g]
(s : category_theory.limits.pullback_cone f g)
(i j : 𝒰.J) :
category_theory.limits.pullback ((𝒰.pullback_cover s.fst).map i) ((𝒰.pullback_cover s.fst).map j) ⟶ (algebraic_geometry.Scheme.pullback.gluing 𝒰 f g).to_glue_data.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 glued_lift.
Equations
- algebraic_geometry.Scheme.pullback.glued_lift_pullback_map 𝒰 f g s i j = id ((category_theory.limits.pullback_right_pullback_fst_iso s.fst (𝒰.map j) category_theory.limits.pullback.fst).hom ≫ category_theory.limits.pullback.map (category_theory.limits.pullback.fst ≫ s.fst) (𝒰.map j) (category_theory.limits.pullback.fst ≫ 𝒰.map i) (𝒰.map j) ((category_theory.limits.pullback_symmetry s.fst (𝒰.map i)).hom ≫ category_theory.limits.pullback.map (𝒰.map i) s.fst (𝒰.map i ≫ f) g (𝟙 (𝒰.obj i)) s.snd f _ _) (𝟙 (𝒰.obj j)) (𝟙 X) _ _)
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), category_theory.limits.has_pullback (𝒰.map i ≫ f) g]
(s : category_theory.limits.pullback_cone f g)
(i j : 𝒰.J) :
algebraic_geometry.Scheme.pullback.glued_lift_pullback_map 𝒰 f g s i j ≫ category_theory.limits.pullback.fst = category_theory.limits.pullback.fst ≫ (category_theory.limits.pullback_symmetry s.fst (𝒰.map i)).hom ≫ category_theory.limits.pullback.map (𝒰.map i) s.fst (𝒰.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), category_theory.limits.has_pullback (𝒰.map i ≫ f) g]
(s : category_theory.limits.pullback_cone f g)
(i j : 𝒰.J)
{X' : algebraic_geometry.Scheme}
(f' : category_theory.limits.pullback (𝒰.map i ≫ f) g ⟶ X') :
algebraic_geometry.Scheme.pullback.glued_lift_pullback_map 𝒰 f g s i j ≫ category_theory.limits.pullback.fst ≫ f' = category_theory.limits.pullback.fst ≫ (category_theory.limits.pullback_symmetry s.fst (𝒰.map i)).hom ≫ category_theory.limits.pullback.map (𝒰.map i) s.fst (𝒰.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), category_theory.limits.has_pullback (𝒰.map i ≫ f) g]
(s : category_theory.limits.pullback_cone f g)
(i j : 𝒰.J)
{X' : algebraic_geometry.Scheme}
(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), category_theory.limits.has_pullback (𝒰.map i ≫ f) g]
(s : category_theory.limits.pullback_cone f 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), category_theory.limits.has_pullback (𝒰.map i ≫ f) g]
(s : category_theory.limits.pullback_cone f g) :
s.X ⟶ (algebraic_geometry.Scheme.pullback.gluing 𝒰 f g).glued
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
- algebraic_geometry.Scheme.pullback.glued_lift 𝒰 f g s = (𝒰.pullback_cover s.fst).glue_morphisms (λ (i : (𝒰.pullback_cover s.fst).J), (category_theory.limits.pullback_symmetry s.fst (𝒰.map i)).hom ≫ category_theory.limits.pullback.map (𝒰.map i) s.fst (𝒰.map i ≫ f) g (𝟙 (𝒰.obj i)) s.snd f _ _ ≫ (algebraic_geometry.Scheme.pullback.gluing 𝒰 f g).ι i) _
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), category_theory.limits.has_pullback (𝒰.map i ≫ f) g]
(s : category_theory.limits.pullback_cone f 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), category_theory.limits.has_pullback (𝒰.map i ≫ f) g]
(s : category_theory.limits.pullback_cone f 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), category_theory.limits.has_pullback (𝒰.map i ≫ f) 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
- algebraic_geometry.Scheme.pullback.pullback_fst_ι_to_V 𝒰 f g i j = (category_theory.limits.pullback_symmetry category_theory.limits.pullback.fst ((algebraic_geometry.Scheme.pullback.gluing 𝒰 f g).ι j) ≪≫ category_theory.limits.pullback_right_pullback_fst_iso (algebraic_geometry.Scheme.pullback.p1 𝒰 f g) (𝒰.map i) ((algebraic_geometry.Scheme.pullback.gluing 𝒰 f g).ι j)).hom ≫ (category_theory.limits.pullback.congr_hom _ _).hom
@[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), category_theory.limits.has_pullback (𝒰.map i ≫ f) g]
(i j : 𝒰.J)
{X' : algebraic_geometry.Scheme}
(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), category_theory.limits.has_pullback (𝒰.map i ≫ f) 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), category_theory.limits.has_pullback (𝒰.map i ≫ f) g]
(i j : 𝒰.J)
{X' : algebraic_geometry.Scheme}
(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), category_theory.limits.has_pullback (𝒰.map i ≫ f) 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), category_theory.limits.has_pullback (𝒰.map i ≫ f) 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), category_theory.limits.has_pullback (𝒰.map i ≫ f) g]
(i : 𝒰.J) :
category_theory.limits.pullback (algebraic_geometry.Scheme.pullback.p1 𝒰 f g) (𝒰.map i) ≅ category_theory.limits.pullback (𝒰.map i ≫ f) g
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
- algebraic_geometry.Scheme.pullback.pullback_p1_iso 𝒰 f g i = {hom := category_theory.limits.pullback.lift category_theory.limits.pullback.snd (category_theory.limits.pullback.fst ≫ algebraic_geometry.Scheme.pullback.p2 𝒰 f g) _, inv := category_theory.limits.pullback.lift ((algebraic_geometry.Scheme.pullback.gluing 𝒰 f g).ι i) category_theory.limits.pullback.fst _, hom_inv_id' := _, inv_hom_id' := _}
@[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), category_theory.limits.has_pullback (𝒰.map i ≫ f) g]
(i : 𝒰.J)
{X' : algebraic_geometry.Scheme}
(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), category_theory.limits.has_pullback (𝒰.map i ≫ f) 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), category_theory.limits.has_pullback (𝒰.map i ≫ f) g]
(i : 𝒰.J)
{X' : algebraic_geometry.Scheme}
(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), category_theory.limits.has_pullback (𝒰.map i ≫ f) 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), category_theory.limits.has_pullback (𝒰.map i ≫ f) g]
(i : 𝒰.J)
{X' : algebraic_geometry.Scheme}
(f' : (algebraic_geometry.Scheme.pullback.gluing 𝒰 f g).glued ⟶ X') :
(algebraic_geometry.Scheme.pullback.pullback_p1_iso 𝒰 f g i).inv ≫ category_theory.limits.pullback.fst ≫ f' = (algebraic_geometry.Scheme.pullback.gluing 𝒰 f g).ι i ≫ f'
@[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), category_theory.limits.has_pullback (𝒰.map i ≫ f) 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), category_theory.limits.has_pullback (𝒰.map i ≫ f) g]
(i : 𝒰.J)
{X' : algebraic_geometry.Scheme}
(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), category_theory.limits.has_pullback (𝒰.map i ≫ f) 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), category_theory.limits.has_pullback (𝒰.map i ≫ f) g]
(i : 𝒰.J)
{X' : algebraic_geometry.Scheme}
(f' : (algebraic_geometry.Scheme.pullback.gluing 𝒰 f g).glued ⟶ X') :
(algebraic_geometry.Scheme.pullback.pullback_p1_iso 𝒰 f g i).hom ≫ (algebraic_geometry.Scheme.pullback.gluing 𝒰 f g).ι i ≫ f' = category_theory.limits.pullback.fst ≫ f'
@[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), category_theory.limits.has_pullback (𝒰.map i ≫ f) 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), category_theory.limits.has_pullback (𝒰.map i ≫ f) g] :
The glued scheme ((gluing 𝒰 f g).glued) is indeed the pullback of f and g.
Equations
- algebraic_geometry.Scheme.pullback.glued_is_limit 𝒰 f g = (category_theory.limits.pullback_cone.mk (algebraic_geometry.Scheme.pullback.p1 𝒰 f g) (algebraic_geometry.Scheme.pullback.p2 𝒰 f g) _).is_limit_aux' (λ (s : category_theory.limits.pullback_cone f g), ⟨algebraic_geometry.Scheme.pullback.glued_lift 𝒰 f g s, _⟩)
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), category_theory.limits.has_pullback (𝒰.map i ≫ f) g] :
@[protected, instance]
theorem
algebraic_geometry.Scheme.pullback.affine_affine_has_pullback
{B C : CommRing}
{X : algebraic_geometry.Scheme}
(f : X ⟶ algebraic_geometry.Scheme.Spec.obj (opposite.op C))
(g : algebraic_geometry.Scheme.Spec.obj (opposite.op B) ⟶ algebraic_geometry.Scheme.Spec.obj (opposite.op C)) :
@[protected, instance]
def
algebraic_geometry.Scheme.pullback.base_affine_has_pullback
{C : CommRing}
{X Y : algebraic_geometry.Scheme}
(f : X ⟶ algebraic_geometry.Scheme.Spec.obj (opposite.op C))
(g : Y ⟶ algebraic_geometry.Scheme.Spec.obj (opposite.op C)) :
@[protected, instance]
def
algebraic_geometry.Scheme.pullback.left_affine_comp_pullback_has_pullback
{X Y Z : algebraic_geometry.Scheme}
(f : X ⟶ Z)
(g : Y ⟶ Z)
(i : Z.affine_cover.J) :
category_theory.limits.has_pullback ((Z.affine_cover.pullback_cover f).map i ≫ f) g
@[protected, instance]
def
algebraic_geometry.Scheme.pullback.category_theory.limits.has_pullback
{X Y Z : algebraic_geometry.Scheme}
(f : X ⟶ Z)
(g : Y ⟶ Z) :
@[protected, instance]
def
algebraic_geometry.Scheme.pullback.category_theory.limits.pullback.algebraic_geometry.is_affine
{X Y Z : algebraic_geometry.Scheme}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[algebraic_geometry.is_affine X]
[algebraic_geometry.is_affine Y]
[algebraic_geometry.is_affine Z] :
@[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) :
(algebraic_geometry.Scheme.pullback.open_cover_of_left 𝒰 f g).map i = category_theory.limits.pullback.map (𝒰.map i ≫ f) g f g (𝒰.map i) (𝟙 Y) (𝟙 Z) _ _
@[simp]
theorem
algebraic_geometry.Scheme.pullback.open_cover_of_left_J
{X Y Z : algebraic_geometry.Scheme}
(𝒰 : X.open_cover)
(f : X ⟶ Z)
(g : 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
- algebraic_geometry.Scheme.pullback.open_cover_of_left 𝒰 f g = ((algebraic_geometry.Scheme.pullback.gluing 𝒰 f g).open_cover.pushforward_iso (category_theory.limits.limit.iso_limit_cone {cone := category_theory.limits.pullback_cone.mk (algebraic_geometry.Scheme.pullback.p1 𝒰 f g) (algebraic_geometry.Scheme.pullback.p2 𝒰 f g) _, is_limit := algebraic_geometry.Scheme.pullback.glued_is_limit 𝒰 f g _}).inv).copy 𝒰.J (λ (i : 𝒰.J), category_theory.limits.pullback (𝒰.map i ≫ f) g) (λ (i : 𝒰.J), category_theory.limits.pullback.map (𝒰.map i ≫ f) g f g (𝒰.map i) (𝟙 Y) (𝟙 Z) _ _) (equiv.refl 𝒰.J) (λ (_x : 𝒰.J), category_theory.iso.refl ((λ (i : 𝒰.J), category_theory.limits.pullback (𝒰.map i ≫ f) g) _x)) _
@[simp]
theorem
algebraic_geometry.Scheme.pullback.open_cover_of_left_obj
{X Y Z : algebraic_geometry.Scheme}
(𝒰 : X.open_cover)
(f : X ⟶ Z)
(g : Y ⟶ Z)
(i : 𝒰.J) :
(algebraic_geometry.Scheme.pullback.open_cover_of_left 𝒰 f g).obj i = category_theory.limits.pullback (𝒰.map i ≫ f) g
@[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) :
(algebraic_geometry.Scheme.pullback.open_cover_of_right 𝒰 f g).map i = category_theory.limits.pullback.map f (𝒰.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) :
(algebraic_geometry.Scheme.pullback.open_cover_of_right 𝒰 f g).obj i = category_theory.limits.pullback f (𝒰.map i ≫ g)
@[simp]
theorem
algebraic_geometry.Scheme.pullback.open_cover_of_right_J
{X Y Z : algebraic_geometry.Scheme}
(𝒰 : Y.open_cover)
(f : X ⟶ Z)
(g : Y ⟶ Z) :
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
- algebraic_geometry.Scheme.pullback.open_cover_of_right 𝒰 f g = ((algebraic_geometry.Scheme.pullback.open_cover_of_left 𝒰 g f).pushforward_iso (category_theory.limits.pullback_symmetry g f).hom).copy 𝒰.J (λ (i : 𝒰.J), category_theory.limits.pullback f (𝒰.map i ≫ g)) (λ (i : 𝒰.J), category_theory.limits.pullback.map f (𝒰.map i ≫ g) f g (𝟙 X) (𝒰.map i) (𝟙 Z) _ _) (equiv.refl 𝒰.J) (λ (i : 𝒰.J), category_theory.limits.pullback_symmetry f (𝒰.map i ≫ g)) _
@[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) :
@[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) :
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
- algebraic_geometry.Scheme.pullback.open_cover_of_left_right 𝒰X 𝒰Y f g = ((algebraic_geometry.Scheme.pullback.open_cover_of_left 𝒰X f g).bind (λ (x : (algebraic_geometry.Scheme.pullback.open_cover_of_left 𝒰X f g).J), algebraic_geometry.Scheme.pullback.open_cover_of_right 𝒰Y (𝒰X.map x ≫ f) g)).copy (𝒰X.J × 𝒰Y.J) (λ (ij : 𝒰X.J × 𝒰Y.J), category_theory.limits.pullback (𝒰X.map ij.fst ≫ f) (𝒰Y.map ij.snd ≫ g)) (λ (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) _ _) (equiv.sigma_equiv_prod 𝒰X.J 𝒰Y.J).symm (λ (_x : 𝒰X.J × 𝒰Y.J), category_theory.iso.refl ((λ (ij : 𝒰X.J × 𝒰Y.J), category_theory.limits.pullback (𝒰X.map ij.fst ≫ f) (𝒰Y.map ij.snd ≫ g)) _x)) _
@[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) :
(algebraic_geometry.Scheme.pullback.open_cover_of_left_right 𝒰X 𝒰Y f g).obj ij = 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
- algebraic_geometry.Scheme.pullback.open_cover_of_base' 𝒰 f g = (algebraic_geometry.Scheme.pullback.open_cover_of_left (𝒰.pullback_cover f) f g).bind (λ (i : (algebraic_geometry.Scheme.pullback.open_cover_of_left (𝒰.pullback_cover f) f g).J), let Xᵢ : algebraic_geometry.Scheme := category_theory.limits.pullback f (𝒰.map i), Yᵢ : algebraic_geometry.Scheme := category_theory.limits.pullback g (𝒰.map i), W : algebraic_geometry.Scheme := category_theory.limits.pullback category_theory.limits.pullback.snd category_theory.limits.pullback.snd in algebraic_geometry.Scheme.open_cover_of_is_iso ((category_theory.limits.pullback_symmetry category_theory.limits.pullback.snd category_theory.limits.pullback.snd).hom ≫ (category_theory.limits.limit.iso_limit_cone {cone := category_theory.limits.pullback_cone.mk category_theory.limits.pullback.snd (category_theory.limits.pullback.fst ≫ category_theory.limits.pullback.fst) _, is_limit := category_theory.limits.big_square_is_pullback category_theory.limits.pullback.fst category_theory.limits.pullback.fst category_theory.limits.pullback.snd (𝒰.map i) category_theory.limits.pullback.snd category_theory.limits.pullback.snd g _ _ (category_theory.limits.pullback_cone.flip_is_limit (category_theory.limits.pullback_is_pullback g (𝒰.map i))) (category_theory.limits.pullback_cone.flip_is_limit (category_theory.limits.pullback_is_pullback category_theory.limits.pullback.snd category_theory.limits.pullback.snd))}).inv ≫ category_theory.limits.pullback.map (category_theory.limits.pullback.snd ≫ 𝒰.map i) g ((𝒰.pullback_cover f).map i ≫ f) g (𝟙 (category_theory.limits.pullback f (𝒰.map i))) (𝟙 Y) (𝟙 Z) _ _))
@[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
- algebraic_geometry.Scheme.pullback.open_cover_of_base 𝒰 f g = (algebraic_geometry.Scheme.pullback.open_cover_of_base' 𝒰 f g).copy 𝒰.J (λ (i : 𝒰.J), category_theory.limits.pullback category_theory.limits.pullback.snd category_theory.limits.pullback.snd) (λ (i : 𝒰.J), category_theory.limits.pullback.map category_theory.limits.pullback.snd category_theory.limits.pullback.snd f g category_theory.limits.pullback.fst category_theory.limits.pullback.fst (𝒰.map i) _ _) ((equiv.prod_punit 𝒰.J).symm.trans (equiv.sigma_equiv_prod 𝒰.J punit).symm) (λ (_x : 𝒰.J), category_theory.iso.refl ((λ (i : 𝒰.J), category_theory.limits.pullback category_theory.limits.pullback.snd category_theory.limits.pullback.snd) _x)) _
@[simp]
theorem
algebraic_geometry.Scheme.pullback.open_cover_of_base_J
{X Y Z : algebraic_geometry.Scheme}
(𝒰 : Z.open_cover)
(f : X ⟶ Z)
(g : Y ⟶ Z) :
@[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₃] :
algebraic_geometry.is_open_immersion (category_theory.limits.pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂)