The graph of two coordinate systems: the point (p, p)

Kollár's point (p, p) ∈ U_2(p) of the graph ([Kol07, 95], the proof of Theorem 92); Włodarczyk's component "whose images φ_u(U) and φ_v(U) contain x" (the proof of [Wlo05, Lemma 2.9.5]). For two coordinate systems u, v on U whose coordinates all vanish at p (so that φ_u(p) = φ_v(p) = 0, Origin.lean), the canonical morphism s : Spec κ(p) ⟶ U (through the stalk, Opens.fromSpecStalkOfMem) has s ≫ φ_u = s ≫ φ_v: both are Spec of the ring map k[t] → κ(p) sending every t_i to 0 and the constants to the k-structure of κ(p) (MvPolynomial.ringHom_ext). The induced Spec κ(p) ⟶ W = U ×_{𝔸ⁿ} U sends the point of Spec κ(p) to a point q over p for both projections; s is a preimmersion, so its stalk map is surjective, its residue field map κ(p) → κ(p) is surjective, and both κ(p) → κ(q) are isomorphisms (isIso_residueFieldMap_of_comp). The morphism Spec κ(p) ⟶ W itself is named graphPoint in GraphFormal.lean; GraphComponent.lean and GraphDiagonalPair.lean build the neighbourhood pair at this point.

Residue field maps

theorem AlgebraicGeometry.residueFieldMap_surjective_of_surjectiveOnStalks {Y Z : Scheme} (g : Y ⟶ Z) [SurjectiveOnStalks g] (y : ↥Y) : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (Scheme.Hom.residueFieldMap g y))

The residue field map of a morphism surjective on stalks is surjective.

theorem AlgebraicGeometry.isIso_residueFieldMap_of_surjective {Y Z : Scheme} (g : Y ⟶ Z) (y : ↥Y) (h : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (Scheme.Hom.residueFieldMap g y))) : CategoryTheory.IsIso (Scheme.Hom.residueFieldMap g y)

A surjective residue field map is an isomorphism (a homomorphism of fields is injective).

theorem AlgebraicGeometry.isIso_residueFieldMap_of_comp {T W V : Scheme} (g : T ⟶ W) (h : W ⟶ V) [SurjectiveOnStalks (CategoryTheory.CategoryStruct.comp g h)] (t : ↥T) : CategoryTheory.IsIso (Scheme.Hom.residueFieldMap h (g t))

If g ≫ h is surjective on stalks, h has trivial residue field extension at the image points of g: κ(h (g t)) → κ(g t) is an isomorphism.

The canonical morphism Spec κ(p) ⟶ U and its image in 𝔸ⁿ_k

noncomputable def AlgebraicGeometry.specResidueFieldToOpens {X : Scheme} {U : ↑X.affineOpens} {p : ↥X} (hpU : p ∈ ↑U) : Spec (X.residueField p) ⟶ ↑↑U

The canonical morphism Spec κ(p) ⟶ U for p ∈ U: Spec of the residue map followed by Spec 𝒪_{X,p} ⟶ U.

Equations

• AlgebraicGeometry.specResidueFieldToOpens hpU = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (X.residue p)) ((↑U).fromSpecStalkOfMem p hpU)

theorem AlgebraicGeometry.specResidueFieldToOpens_ι {X : Scheme} {U : ↑X.affineOpens} {p : ↥X} (hpU : p ∈ ↑U) : CategoryTheory.CategoryStruct.comp (specResidueFieldToOpens hpU) (↑U).ι = X.fromSpecResidueField p

instance AlgebraicGeometry.isPreimmersion_specResidueFieldToOpens {X : Scheme} {U : ↑X.affineOpens} {p : ↥X} (hpU : p ∈ ↑U) : IsPreimmersion (specResidueFieldToOpens hpU)

theorem AlgebraicGeometry.specResidueFieldToOpens_apply {X : Scheme} {U : ↑X.affineOpens} {p : ↥X} (hpU : p ∈ ↑U) (s : ↥(Spec (X.residueField p))) : (specResidueFieldToOpens hpU) s = ⟨p, hpU⟩

theorem AlgebraicGeometry.specResidueFieldToOpens_toAffineSpace {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) {n : ℕ} {U : ↑X.affineOpens} {p : ↥X} (hpU : p ∈ ↑U) (v : Fin n → ↑(X.presheaf.obj (Opposite.op ↑U))) : CategoryTheory.CategoryStruct.comp (specResidueFieldToOpens hpU) (toAffineSpace f (↑U) v) = Spec.map (CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (MvPolynomial.aeval v).toRingHom) (CategoryTheory.CategoryStruct.comp (X.presheaf.germ (↑U) p hpU) (X.residue p)))

The composite Spec κ(p) ⟶ U ⟶ 𝔸ⁿ_k is Spec of k[t] → κ(p), t_i ↦ v_i(p).

theorem AlgebraicGeometry.specResidueFieldToOpens_toAffineSpace_eq {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) {n : ℕ} {U : ↑X.affineOpens} {p : ↥X} (hpU : p ∈ ↑U) (v v' : Fin n → ↑(X.presheaf.obj (Opposite.op ↑U))) (hv : ∀ (i : Fin n), (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ (↑U) p hpU)) (v i) ∈ IsLocalRing.maximalIdeal ↑(X.presheaf.stalk p)) (hv' : ∀ (i : Fin n), (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ (↑U) p hpU)) (v' i) ∈ IsLocalRing.maximalIdeal ↑(X.presheaf.stalk p)) : CategoryTheory.CategoryStruct.comp (specResidueFieldToOpens hpU) (toAffineSpace f (↑U) v) = CategoryTheory.CategoryStruct.comp (specResidueFieldToOpens hpU) (toAffineSpace f (↑U) v')

If all coordinates of v and v' vanish at p, the two composites Spec κ(p) ⟶ 𝔸ⁿ_k agree: both send every t_i to 0.

The point (p, p) of the graph

theorem AlgebraicGeometry.EtaleCoordinates.exists_graph_point {k : Type u} [Field k] {X : Scheme} {f : X ⟶ Spec ↧k} {n : ℕ} {U : ↑X.affineOpens} (c c' : EtaleCoordinates f n U) {p : ↥X} (hpU : p ∈ ↑U) (hc : ∀ (i : Fin n), (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ (↑U) p hpU)) (c.v i) ∈ IsLocalRing.maximalIdeal ↑(X.presheaf.stalk p)) (hc' : ∀ (i : Fin n), (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ (↑U) p hpU)) (c'.v i) ∈ IsLocalRing.maximalIdeal ↑(X.presheaf.stalk p)) : ∃ (q : ↥(c.graph c')), (c.graphFst c') q = ⟨p, hpU⟩ ∧ (c.graphSnd c') q = ⟨p, hpU⟩ ∧ CategoryTheory.IsIso (Scheme.Hom.residueFieldMap (c.graphFst c') q) ∧ CategoryTheory.IsIso (Scheme.Hom.residueFieldMap (c.graphSnd c') q)

If all coordinates of both systems vanish at p, there is a point q of W over p for both projections, with κ(q) = κ(p) (Kollár's "(p, p) ∈ U_2(p)", [Kol07, 95]).