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 : 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

  The point of X.

• y : ↥Y

  The point of Y.

• s : ↥S

  The point of S below x and y.

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

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

theorem AlgebraicGeometry.Scheme.Pullback.Triplet.ext_iff {X Y S : Scheme} {f : X ⟶ S} {g : Y ⟶ S} {t₁ t₂ : Triplet f g} : t₁ = t₂ ↔ t₁.x = t₂.x ∧ t₁.y = t₂.y

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

def AlgebraicGeometry.Scheme.Pullback.Triplet.tensorInl {X Y S : Scheme} {f : X ⟶ S} {g : Y ⟶ S} (T : 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).

def AlgebraicGeometry.Scheme.Pullback.Triplet.tensorInr {X Y S : Scheme} {f : X ⟶ S} {g : Y ⟶ S} (T : 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).

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

@[deprecated AlgebraicGeometry.Scheme.Pullback.Triplet.isPullback_SpecMap_tensor (since := "2025-10-07")]

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

Alias of AlgebraicGeometry.Scheme.Pullback.Triplet.isPullback_SpecMap_tensor.

def AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr {X Y S : Scheme} {f : X ⟶ S} {g : Y ⟶ S} {T₁ T₂ : 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.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[deprecated AlgebraicGeometry.Scheme.Pullback.Triplet.SpecMap_tensorInl_fromSpecResidueField (since := "2025-10-07")]

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

Alias of AlgebraicGeometry.Scheme.Pullback.Triplet.SpecMap_tensorInl_fromSpecResidueField.

def AlgebraicGeometry.Scheme.Pullback.Triplet.SpecTensorTo {X Y S : Scheme} {f : X ⟶ S} {g : Y ⟶ S} (T : Triplet f g) : 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.

@[simp]

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

@[deprecated AlgebraicGeometry.Scheme.Pullback.Triplet.fst_SpecTensorTo_apply (since := "2025-10-11")]

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

Alias of AlgebraicGeometry.Scheme.Pullback.Triplet.fst_SpecTensorTo_apply.

@[simp]

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

@[deprecated AlgebraicGeometry.Scheme.Pullback.Triplet.snd_SpecTensorTo_apply (since := "2025-10-11")]

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

Alias of AlgebraicGeometry.Scheme.Pullback.Triplet.snd_SpecTensorTo_apply.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

def AlgebraicGeometry.Scheme.Pullback.ofPointTensor {X Y S : Scheme} {f : X ⟶ S} {g : Y ⟶ S} (t : ↥(CategoryTheory.Limits.pullback f g)) : (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).

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.tensorCongr_SpecTensorTo_assoc {X Y S : Scheme} {f : X ⟶ S} {g : Y ⟶ S} {T T' : Triplet f g} (h : T = T') {Z : Scheme} (h✝ : CategoryTheory.Limits.pullback f g ⟶ Z) : CategoryTheory.CategoryStruct.comp (Spec.map (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 : Scheme} {f : X ⟶ S} {g : Y ⟶ S} (T : Triplet f g) (p : ↥(Spec T.tensor)) : CategoryTheory.CategoryStruct.comp (Spec.map (Hom.residueFieldMap T.SpecTensorTo p)) (CategoryTheory.CategoryStruct.comp (Spec.map (ofPointTensor (T.SpecTensorTo p))) (Spec.map (tensorCongr ⋯).hom)) = (Spec T.tensor).fromSpecResidueField p

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

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

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

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

@[simp]

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

@[simp]

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

theorem AlgebraicGeometry.Scheme.Pullback.Triplet.exists_preimage {X Y S : Scheme} {f : X ⟶ S} {g : Y ⟶ S} (T : Triplet f g) : ∃ (t : ↥(CategoryTheory.Limits.pullback f g)), (CategoryTheory.Limits.pullback.fst f g) t = T.x ∧ (CategoryTheory.Limits.pullback.snd f g) 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 : Scheme} {f : X ⟶ S} {g : Y ⟶ S} (x : ↥X) (y : ↥Y) (h : f x = g y) : ∃ (z : ↥(CategoryTheory.Limits.pullback f g)), (CategoryTheory.Limits.pullback.fst f g) z = x ∧ (CategoryTheory.Limits.pullback.snd f g) 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.isEmpty_pullback_iff {X Y S : Scheme} {f : X ⟶ S} {g : Y ⟶ S} : IsEmpty ↥(CategoryTheory.Limits.pullback f g) ↔ Disjoint (Set.range ⇑f) (Set.range ⇑g)

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

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

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

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

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

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

theorem AlgebraicGeometry.Scheme.pullbackComparison_forget_surjective {X Y S : Scheme} (f : X ⟶ S) (g : Y ⟶ S) : Function.Surjective (CategoryTheory.Limits.pullbackComparison forget f g)

The comparison map for pullbacks under the forgetful functor Scheme ⥤ Type u is surjective.

@[deprecated AlgebraicGeometry.Scheme.pullbackComparison_forget_surjective (since := "2025-10-06")]

theorem AlgebraicGeometry.Scheme.Pullback.forget_comparison_surjective {X Y S : Scheme} (f : X ⟶ S) (g : Y ⟶ S) : Function.Surjective (CategoryTheory.Limits.pullbackComparison forget f g)

Alias of AlgebraicGeometry.Scheme.pullbackComparison_forget_surjective.

---

The comparison map for pullbacks under the forgetful functor Scheme ⥤ Type u is surjective.

theorem AlgebraicGeometry.Scheme.exists_preimage_of_isPullback {P X Y Z : Scheme} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} (h : CategoryTheory.IsPullback fst snd f g) (x : ↥X) (y : ↥Y) (hxy : f x = g y) : ∃ (p : ↥P), fst p = x ∧ snd p = y

theorem AlgebraicGeometry.Scheme.image_preimage_eq_of_isPullback {P X Y Z : Scheme} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} (h : CategoryTheory.IsPullback fst snd f g) (s : Set ↥X) : ⇑snd '' (⇑fst ⁻¹' s) = ⇑g ⁻¹' (⇑f '' s)

instance AlgebraicGeometry.Surjective.instIsStableUnderBaseChangeScheme : CategoryTheory.MorphismProperty.IsStableUnderBaseChange @Surjective

instance AlgebraicGeometry.Surjective.instFstScheme {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [Surjective g] : Surjective (CategoryTheory.Limits.pullback.fst f g)

instance AlgebraicGeometry.Surjective.instSndScheme {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [Surjective f] : Surjective (CategoryTheory.Limits.pullback.snd f g)