English
Let f: X → Y be a morphism of schemes and suppose H is a witness for the existence part of the valuative criterion for f. Then the underlying continuous map base(f) carries a SpecializingMap structure, i.e. specialization relations on Y are compatible with the map to X along f.
Русский
Пусть f: X → Y — морфизм схем и даны данные(H), служащие доказательством существования по критерию Валюативности для f. Тогда базовая непрерывная карта f.base имеет структуру SpecializingMap, то есть отношение специализации на Y совместимо с отображением в X через f.
LaTeX
$$$SpecializingMap\ f_{\mathrm{base}}$$$
Lean4
@[stacks 01KE]
theorem specializingMap (H : ValuativeCriterion.Existence f) : SpecializingMap f.base :=
by
intro x' y h
let stalk_y_to_residue_x' : Y.presheaf.stalk y ⟶ X.residueField x' :=
Y.presheaf.stalkSpecializes h ≫ f.stalkMap x' ≫ X.residue x'
obtain ⟨A, hA, hA_local⟩ := exists_factor_valuationRing stalk_y_to_residue_x'.hom
let stalk_y_to_A : Y.presheaf.stalk y ⟶ .of A := CommRingCat.ofHom (stalk_y_to_residue_x'.hom.codRestrict _ hA)
have w :
X.fromSpecResidueField x' ≫ f =
Spec.map (CommRingCat.ofHom (algebraMap A (X.residueField x'))) ≫ Spec.map stalk_y_to_A ≫ Y.fromSpecStalk y :=
by
rw [Scheme.fromSpecResidueField, Category.assoc, ← Scheme.Spec_map_stalkMap_fromSpecStalk, ←
Scheme.Spec_map_stalkSpecializes_fromSpecStalk h]
simp_rw [← Spec.map_comp_assoc]
rfl
obtain ⟨l, hl₁, hl₂⟩ := (H { R := A, K := X.residueField x', commSq := ⟨w⟩, .. }).exists_lift
dsimp only at hl₁ hl₂
refine ⟨l.base (closedPoint A), ?_, ?_⟩
· simp_rw [← Scheme.fromSpecResidueField_apply x' (closedPoint (X.residueField x')), ← hl₁]
exact (specializes_closedPoint _).map l.base.hom.2
· rw [← Scheme.comp_base_apply, hl₂]
simp only [Scheme.comp_coeBase, TopCat.coe_comp, Function.comp_apply]
have : (Spec.map stalk_y_to_A).base (closedPoint A) = closedPoint (Y.presheaf.stalk y) :=
comap_closedPoint (S := A) (stalk_y_to_residue_x'.hom.codRestrict A.toSubring hA)
rw [this, Y.fromSpecStalk_closedPoint]
