Underlying topological space of fibre product of schemes

Let f : X ⟶ S and g : Y ⟶ S be morphisms of schemes. In this file we describe the underlying topological space of pullback f g, i.e. the fiber product X ×[S] Y.

Main results

• AlgebraicGeometry.Scheme.Pullback.carrierEquiv: The bijective correspondence between the points of X ×[S] Y and pairs (z, p) of triples z = (x, y, s) with f x = s = g y and prime ideals q of κ(x) ⊗[κ(s)] κ(y).
• AlgebraicGeometry.Scheme.Pullback.exists_preimage: For every triple (x, y, s) with f x = s = g y, there exists z : X ×[S] Y lying above x and y.

We also give the ranges of pullback.fst, pullback.snd and pullback.map.

structure AlgebraicGeometry.Scheme.Pullback.Triplet {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) : Type u

A Triplet over f : X ⟶ S and g : Y ⟶ S is a triple of points x : X, y : Y, s : S such that f x = s = f y.

• x : ↑↑X.toPresheafedSpace

  The point of X.

• y : ↑↑Y.toPresheafedSpace

  The point of Y.

• s : ↑↑S.toPresheafedSpace

  The point of S below x and y.

• hx : f.base self.x = self.s
• hy : g.base self.y = self.s

theorem AlgebraicGeometry.Scheme.Pullback.Triplet.ext {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} {t₁ t₂ : AlgebraicGeometry.Scheme.Pullback.Triplet f g} (ex : t₁.x = t₂.x) (ey : t₁.y = t₂.y) : t₁ = t₂

def AlgebraicGeometry.Scheme.Pullback.Triplet.mk' {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (x : ↑↑X.toPresheafedSpace) (y : ↑↑Y.toPresheafedSpace) (h : f.base x = g.base y) : AlgebraicGeometry.Scheme.Pullback.Triplet f g

Make a triplet from x : X and y : Y such that f x = g y.

Equations

• AlgebraicGeometry.Scheme.Pullback.Triplet.mk' x y h = { x := x, y := y, s := g.base y, hx := h, hy := ⋯ }

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.Triplet.mk'_s {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (x : ↑↑X.toPresheafedSpace) (y : ↑↑Y.toPresheafedSpace) (h : f.base x = g.base y) : (AlgebraicGeometry.Scheme.Pullback.Triplet.mk' x y h).s = g.base y

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.Triplet.mk'_x {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (x : ↑↑X.toPresheafedSpace) (y : ↑↑Y.toPresheafedSpace) (h : f.base x = g.base y) : (AlgebraicGeometry.Scheme.Pullback.Triplet.mk' x y h).x = x

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.Triplet.mk'_y {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (x : ↑↑X.toPresheafedSpace) (y : ↑↑Y.toPresheafedSpace) (h : f.base x = g.base y) : (AlgebraicGeometry.Scheme.Pullback.Triplet.mk' x y h).y = y

def AlgebraicGeometry.Scheme.Pullback.Triplet.tensor {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (T : AlgebraicGeometry.Scheme.Pullback.Triplet f g) : CommRingCat

Given x : X and y : Y such that f x = s = g y, this is κ(x) ⊗[κ(s)] κ(y).

Equations

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

instance AlgebraicGeometry.Scheme.Pullback.Triplet.instNontrivialαCommRingTensor {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (T : AlgebraicGeometry.Scheme.Pullback.Triplet f g) : Nontrivial ↑T.tensor

Equations

• ⋯ = ⋯

def AlgebraicGeometry.Scheme.Pullback.Triplet.tensorInl {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (T : AlgebraicGeometry.Scheme.Pullback.Triplet f g) : X.residueField T.x ⟶ T.tensor

Given x : X and y : Y such that f x = s = g y, this is the canonical map κ(x) ⟶ κ(x) ⊗[κ(s)] κ(y).

Equations

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

def AlgebraicGeometry.Scheme.Pullback.Triplet.tensorInr {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (T : AlgebraicGeometry.Scheme.Pullback.Triplet f g) : Y.residueField T.y ⟶ T.tensor

Given x : X and y : Y such that f x = s = g y, this is the canonical map κ(y) ⟶ κ(x) ⊗[κ(s)] κ(y).

Equations

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

theorem AlgebraicGeometry.Scheme.Pullback.Triplet.Spec_map_tensor_isPullback {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (T : AlgebraicGeometry.Scheme.Pullback.Triplet f g) : CategoryTheory.IsPullback (AlgebraicGeometry.Spec.map T.tensorInl) (AlgebraicGeometry.Spec.map T.tensorInr) (AlgebraicGeometry.Spec.map (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.residueFieldCongr ⋯).inv (AlgebraicGeometry.Scheme.Hom.residueFieldMap f T.x))) (AlgebraicGeometry.Spec.map (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.residueFieldCongr ⋯).inv (AlgebraicGeometry.Scheme.Hom.residueFieldMap g T.y)))

def AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} {T₁ T₂ : AlgebraicGeometry.Scheme.Pullback.Triplet f g} (e : T₁ = T₂) : T₁.tensor ≅ T₂.tensor

Given propositionally equal triplets T₁ and T₂ over f and g, the corresponding T₁.tensor and T₂.tensor are isomorphic.

Equations

• AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr e = CategoryTheory.eqToIso ⋯

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr_refl {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} {x : AlgebraicGeometry.Scheme.Pullback.Triplet f g} : AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr ⋯ = CategoryTheory.Iso.refl x.tensor

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr_symm {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} {x y : AlgebraicGeometry.Scheme.Pullback.Triplet f g} (e : x = y) : (AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr e).symm = AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr ⋯

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr_inv {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} {x y : AlgebraicGeometry.Scheme.Pullback.Triplet f g} (e : x = y) : (AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr e).inv = (AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr ⋯).hom

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr_trans {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} {x y z : AlgebraicGeometry.Scheme.Pullback.Triplet f g} (e : x = y) (e' : y = z) : AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr e ≪≫ AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr e' = AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr ⋯

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr_trans_hom {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} {x y z : AlgebraicGeometry.Scheme.Pullback.Triplet f g} (e : x = y) (e' : y = z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr e).hom (AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr e').hom = (AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr ⋯).hom

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr_trans_hom_assoc {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} {x y z : AlgebraicGeometry.Scheme.Pullback.Triplet f g} (e : x = y) (e' : y = z) {Z : CommRingCat} (h : z.tensor ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr e).hom (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr e').hom h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr ⋯).hom h

theorem AlgebraicGeometry.Scheme.Pullback.Triplet.Spec_map_tensorInl_fromSpecResidueField {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (T : AlgebraicGeometry.Scheme.Pullback.Triplet f g) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map T.tensorInl) (X.fromSpecResidueField T.x)) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map T.tensorInr) (Y.fromSpecResidueField T.y)) g

def AlgebraicGeometry.Scheme.Pullback.Triplet.SpecTensorTo {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (T : AlgebraicGeometry.Scheme.Pullback.Triplet f g) : AlgebraicGeometry.Spec T.tensor ⟶ CategoryTheory.Limits.pullback f g

Given x : X, y : Y and s : S such that f x = s = g y, this is Spec (κ(x) ⊗[κ(s)] κ(y)) ⟶ X ×ₛ Y.

Equations

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

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.Triplet.specTensorTo_base_fst {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (T : AlgebraicGeometry.Scheme.Pullback.Triplet f g) (p : ↑↑(AlgebraicGeometry.Spec T.tensor).toPresheafedSpace) : (CategoryTheory.Limits.pullback.fst f g).base (T.SpecTensorTo.base p) = T.x

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.Triplet.specTensorTo_base_snd {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (T : AlgebraicGeometry.Scheme.Pullback.Triplet f g) (p : ↑↑(AlgebraicGeometry.Spec T.tensor).toPresheafedSpace) : (CategoryTheory.Limits.pullback.snd f g).base (T.SpecTensorTo.base p) = T.y

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.Triplet.specTensorTo_fst {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (T : AlgebraicGeometry.Scheme.Pullback.Triplet f g) : CategoryTheory.CategoryStruct.comp T.SpecTensorTo (CategoryTheory.Limits.pullback.fst f g) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map T.tensorInl) (X.fromSpecResidueField T.x)

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.Triplet.specTensorTo_fst_assoc {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (T : AlgebraicGeometry.Scheme.Pullback.Triplet f g) {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp T.SpecTensorTo (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f g) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map T.tensorInl) (CategoryTheory.CategoryStruct.comp (X.fromSpecResidueField T.x) h)

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.Triplet.specTensorTo_snd {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (T : AlgebraicGeometry.Scheme.Pullback.Triplet f g) : CategoryTheory.CategoryStruct.comp T.SpecTensorTo (CategoryTheory.Limits.pullback.snd f g) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map T.tensorInr) (Y.fromSpecResidueField T.y)

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.Triplet.specTensorTo_snd_assoc {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (T : AlgebraicGeometry.Scheme.Pullback.Triplet f g) {Z : AlgebraicGeometry.Scheme} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp T.SpecTensorTo (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f g) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map T.tensorInr) (CategoryTheory.CategoryStruct.comp (Y.fromSpecResidueField T.y) h)

def AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (t : ↑↑(CategoryTheory.Limits.pullback f g).toPresheafedSpace) : AlgebraicGeometry.Scheme.Pullback.Triplet f g

Given t : X ×[S] Y, it maps to X and Y with same image in S, yielding a Triplet f g.

Equations

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

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint_y {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (t : ↑↑(CategoryTheory.Limits.pullback f g).toPresheafedSpace) : (AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint t).y = (CategoryTheory.Limits.pullback.snd f g).base t

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint_x {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (t : ↑↑(CategoryTheory.Limits.pullback f g).toPresheafedSpace) : (AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint t).x = (CategoryTheory.Limits.pullback.fst f g).base t

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint_s {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (t : ↑↑(CategoryTheory.Limits.pullback f g).toPresheafedSpace) : (AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint t).s = f.base ((CategoryTheory.Limits.pullback.fst f g).base t)

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint_SpecTensorTo {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (T : AlgebraicGeometry.Scheme.Pullback.Triplet f g) (p : ↑↑(AlgebraicGeometry.Spec T.tensor).toPresheafedSpace) : AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint (T.SpecTensorTo.base p) = T

theorem AlgebraicGeometry.Scheme.Pullback.residueFieldCongr_inv_residueFieldMap_ofPoint {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (t : ↑↑(CategoryTheory.Limits.pullback f g).toPresheafedSpace) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.residueFieldCongr ⋯).inv (AlgebraicGeometry.Scheme.Hom.residueFieldMap f (AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint t).x)) (AlgebraicGeometry.Scheme.Hom.residueFieldMap (CategoryTheory.Limits.pullback.fst f g) t) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.residueFieldCongr ⋯).inv (AlgebraicGeometry.Scheme.Hom.residueFieldMap g (AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint t).y)) (AlgebraicGeometry.Scheme.Hom.residueFieldMap (CategoryTheory.Limits.pullback.snd f g) t)

def AlgebraicGeometry.Scheme.Pullback.ofPointTensor {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (t : ↑↑(CategoryTheory.Limits.pullback f g).toPresheafedSpace) : (AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint t).tensor ⟶ (CategoryTheory.Limits.pullback f g).residueField t

Given t : X ×[S] Y with projections to X, Y and S denoted by x, y and s respectively, this is the canonical map κ(x) ⊗[κ(s)] κ(y) ⟶ κ(t).

Equations

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

theorem AlgebraicGeometry.Scheme.Pullback.ofPointTensor_SpecTensorTo {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (t : ↑↑(CategoryTheory.Limits.pullback f g).toPresheafedSpace) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Pullback.ofPointTensor t)) (AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint t).SpecTensorTo = (CategoryTheory.Limits.pullback f g).fromSpecResidueField t

theorem AlgebraicGeometry.Scheme.Pullback.ofPointTensor_SpecTensorTo_assoc {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (t : ↑↑(CategoryTheory.Limits.pullback f g).toPresheafedSpace) {Z : AlgebraicGeometry.Scheme} (h : CategoryTheory.Limits.pullback f g ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Pullback.ofPointTensor t)) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint t).SpecTensorTo h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.pullback f g).fromSpecResidueField t) h

def AlgebraicGeometry.Scheme.Pullback.SpecOfPoint {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (t : ↑↑(CategoryTheory.Limits.pullback f g).toPresheafedSpace) : ↑↑(AlgebraicGeometry.Spec (AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint t).tensor).toPresheafedSpace

If t is a point in X ×[S] Y above (x, y, s), then this is the image of the unique point of Spec κ(s) in Spec κ(x) ⊗[κ(s)] κ(y).

Equations

• AlgebraicGeometry.Scheme.Pullback.SpecOfPoint t = (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Pullback.ofPointTensor t)).base ⊥

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.SpecTensorTo_SpecOfPoint {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (t : ↑↑(CategoryTheory.Limits.pullback f g).toPresheafedSpace) : (AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint t).SpecTensorTo.base (AlgebraicGeometry.Scheme.Pullback.SpecOfPoint t) = t

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.tensorCongr_SpecTensorTo {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} {T T' : AlgebraicGeometry.Scheme.Pullback.Triplet f g} (h : T = T') : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr h).hom) T.SpecTensorTo = T'.SpecTensorTo

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.tensorCongr_SpecTensorTo_assoc {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} {T T' : AlgebraicGeometry.Scheme.Pullback.Triplet f g} (h : T = T') {Z : AlgebraicGeometry.Scheme} (h✝ : CategoryTheory.Limits.pullback f g ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr h).hom) (CategoryTheory.CategoryStruct.comp T.SpecTensorTo h✝) = CategoryTheory.CategoryStruct.comp T'.SpecTensorTo h✝

theorem AlgebraicGeometry.Scheme.Pullback.Triplet.Spec_ofPointTensor_SpecTensorTo {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (T : AlgebraicGeometry.Scheme.Pullback.Triplet f g) (p : ↑↑(AlgebraicGeometry.Spec T.tensor).toPresheafedSpace) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Hom.residueFieldMap T.SpecTensorTo p)) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Pullback.ofPointTensor (T.SpecTensorTo.base p))) (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr ⋯).hom)) = (AlgebraicGeometry.Spec T.tensor).fromSpecResidueField p

theorem AlgebraicGeometry.Scheme.Pullback.carrierEquiv_eq_iff {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} {T₁ T₂ : (T : AlgebraicGeometry.Scheme.Pullback.Triplet f g) × ↑↑(AlgebraicGeometry.Spec T.tensor).toPresheafedSpace} : T₁ = T₂ ↔ ∃ (e : T₁.fst = T₂.fst), (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr e).inv).base T₁.snd = T₂.snd

A helper lemma to work with AlgebraicGeometry.Scheme.Pullback.carrierEquiv.

def AlgebraicGeometry.Scheme.Pullback.carrierEquiv {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} : ↑↑(CategoryTheory.Limits.pullback f g).toPresheafedSpace ≃ (T : AlgebraicGeometry.Scheme.Pullback.Triplet f g) × ↑↑(AlgebraicGeometry.Spec T.tensor).toPresheafedSpace

The points of the underlying topological space of X ×[S] Y bijectively correspond to pairs of triples x : X, y : Y, s : S with f x = s = f y and prime ideals of κ(x) ⊗[κ(s)] κ(y).

Equations

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

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.carrierEquiv_symm_fst {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (T : AlgebraicGeometry.Scheme.Pullback.Triplet f g) (p : ↑↑(AlgebraicGeometry.Spec T.tensor).toPresheafedSpace) : (CategoryTheory.Limits.pullback.fst f g).base (AlgebraicGeometry.Scheme.Pullback.carrierEquiv.symm ⟨T, p⟩) = T.x

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.carrierEquiv_symm_snd {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (T : AlgebraicGeometry.Scheme.Pullback.Triplet f g) (p : ↑↑(AlgebraicGeometry.Spec T.tensor).toPresheafedSpace) : (CategoryTheory.Limits.pullback.snd f g).base (AlgebraicGeometry.Scheme.Pullback.carrierEquiv.symm ⟨T, p⟩) = T.y

theorem AlgebraicGeometry.Scheme.Pullback.Triplet.exists_preimage {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (T : AlgebraicGeometry.Scheme.Pullback.Triplet f g) : ∃ (t : ↑↑(CategoryTheory.Limits.pullback f g).toPresheafedSpace), (CategoryTheory.Limits.pullback.fst f g).base t = T.x ∧ (CategoryTheory.Limits.pullback.snd f g).base t = T.y

Given a triple (x, y, s) with f x = s = f y there exists t : X ×[S] Y above x and ỳ. For the unpacked version without Triplet, see AlgebraicGeometry.Scheme.Pullback.exists_preimage.

theorem AlgebraicGeometry.Scheme.Pullback.exists_preimage_pullback {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (x : ↑↑X.toPresheafedSpace) (y : ↑↑Y.toPresheafedSpace) (h : f.base x = g.base y) : ∃ (z : ↑↑(CategoryTheory.Limits.pullback f g).toPresheafedSpace), (CategoryTheory.Limits.pullback.fst f g).base z = x ∧ (CategoryTheory.Limits.pullback.snd f g).base z = y

If f : X ⟶ S and g : Y ⟶ S are morphisms of schemes and x : X and y : Y are points such that f x = g y, then there exists z : X ×[S] Y lying above x and y.

In other words, the map from the underlying topological space of X ×[S] Y to the fiber product of the underlying topological spaces of X and Y over S is surjective.

theorem AlgebraicGeometry.Scheme.Pullback.range_fst {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) : Set.range ⇑(CategoryTheory.Limits.pullback.fst f g).base = ⇑f.base ⁻¹' Set.range ⇑g.base

theorem AlgebraicGeometry.Scheme.Pullback.range_snd {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) : Set.range ⇑(CategoryTheory.Limits.pullback.snd f g).base = ⇑g.base ⁻¹' Set.range ⇑f.base

theorem AlgebraicGeometry.Scheme.Pullback.range_fst_comp {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) : Set.range ⇑(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f g) f).base = Set.range ⇑f.base ∩ Set.range ⇑g.base

theorem AlgebraicGeometry.Scheme.Pullback.range_snd_comp {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) : Set.range ⇑(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f g) g).base = Set.range ⇑f.base ∩ Set.range ⇑g.base

theorem AlgebraicGeometry.Scheme.Pullback.range_map {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) {X' Y' S' : AlgebraicGeometry.Scheme} (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') [CategoryTheory.Mono i₃] : Set.range ⇑(CategoryTheory.Limits.pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂).base = ⇑(CategoryTheory.Limits.pullback.fst f' g').base ⁻¹' Set.range ⇑i₁.base ∩ ⇑(CategoryTheory.Limits.pullback.snd f' g').base ⁻¹' Set.range ⇑i₂.base

instance AlgebraicGeometry.Scheme.isJointlySurjectivePreserving (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) : AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P

Equations

• ⋯ = ⋯

instance AlgebraicGeometry.Scheme.instIsStableUnderBaseChangeSurjective : CategoryTheory.MorphismProperty.IsStableUnderBaseChange @AlgebraicGeometry.Surjective

Equations

• AlgebraicGeometry.Scheme.instIsStableUnderBaseChangeSurjective = ⋯