English
For X,Y and a morphism f: X ⟶ Y, the natural transformation between residue-field maps and the fromSpecResidueField maps commutes: Spec.map (f.residueFieldMap x) ≫ Y.fromSpecResidueField _ = X.fromSpecResidueField x ≫ f.
Русский
Для X ⟶ Y и фиксации x, естественный трансформационный композит между остаточными полями и отображениями fromSpecResidueField коммутирует: Spec.map (f.residueFieldMap x) ≫ Y.fromSpecResidueField _ = X.fromSpecResidueField x ≫ f.
LaTeX
$$Spec.map (f.residueFieldMap x) ≫ Y.fromSpecResidueField _ = X.fromSpecResidueField x ≫ f$$
Lean4
/-- For a field `K` and a scheme `X`, the morphisms `Spec K ⟶ X` bijectively correspond
to pairs of points `x` of `X` and embeddings `κ(x) ⟶ K`. -/
def SpecToEquivOfField (K : Type u) [Field K] (X : Scheme.{u}) : (Spec (.of K) ⟶ X) ≃ Σ x, X.residueField x ⟶ .of K
where
toFun f := ⟨_, X.descResidueField (Scheme.stalkClosedPointTo f)⟩
invFun xf := Spec.map xf.2 ≫ X.fromSpecResidueField xf.1
left_inv := Scheme.descResidueField_stalkClosedPointTo_fromSpecResidueField K X
right_inv
f := by
rw [SpecToEquivOfField_eq_iff]
simp only [CommRingCat.coe_of, Scheme.comp_coeBase, TopCat.coe_comp, Function.comp_apply,
Scheme.fromSpecResidueField_apply, exists_true_left]
rw [← Spec.map_inj, Spec.map_comp, ← cancel_mono (X.fromSpecResidueField _)]
erw [Scheme.descResidueField_stalkClosedPointTo_fromSpecResidueField]
simp
