English
The tensor of Spec through a pullback Triplet maps back to Spec via the associated base changes; this equality holds after composing the natural maps.
Русский
Тензорная карта Spec через вытяжку Triplet возвращает Spec через соответствующие базовые изменения; равенство сохраняется после композиции естественных отображений.
LaTeX
$$$\text{Spec.map}(\text{tensorCongr}) \circ \text{SpecTensorTo} = \text{SpecOfPoint}$$$
Lean4
/-- 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)`.
-/
def carrierEquiv : ↑(pullback f g) ≃ Σ T : Triplet f g, Spec T.tensor
where
toFun t := ⟨.ofPoint t, SpecOfPoint t⟩
invFun T := T.1.SpecTensorTo.base T.2
left_inv := SpecTensorTo_SpecOfPoint
right_inv := by
intro ⟨T, p⟩
apply carrierEquiv_eq_iff.mpr
use T.ofPoint_SpecTensorTo p
have : (Spec.map (Hom.residueFieldMap T.SpecTensorTo p)).base (⊥ : PrimeSpectrum _) = (⊥ : PrimeSpectrum _) :=
(PrimeSpectrum.instUnique).uniq _
simp only [SpecOfPoint, Triplet.tensorCongr_inv, ← this, ← Scheme.comp_base_apply, ← Scheme.comp_base_apply]
simp [Triplet.Spec_ofPointTensor_SpecTensorTo]
