The image point of a coordinate system, and its stalks

• Kollár chooses the two coordinate systems x_1, x_2, … and x_1', x_2, … with x_1, x_1' ∈ MC(I) ⊆ 𝔪_p, so that both send p to 0 ([Kol07, 95], the proof of Theorem 92). The point φ_v(x) ∈ 𝔸ⁿ_k of the coordinate morphism φ_v = toAffineSpace f U v is the prime (aeval v)⁻¹(𝔭_x) of k[t] (toAffineSpace_base_apply), which contains the coordinate t_i iff v_i ∈ 𝔭_x, i.e. iff the germ (v_i)_x is not a unit, i.e. lies in 𝔪_x (X_mem_toAffineSpace_base_iff). A prime of k[t] containing every t_i is the maximal ideal of the origin (eq_origin_iff_forall_X_mem: the kernel of evaluation at 0 consists of the polynomials without constant term, all in (t_0, …, t_{n-1}), and it is maximal). Hence φ_v(x) = 0 iff all (v_i)_x ∈ 𝔪_x (toAffineSpace_base_eq_origin_iff), and two coordinate systems with all coordinates vanishing at x have the same image point (toAffineSpace_base_eq).
• For an étale g : Y ⟶ Z and y ∈ Y, the stalk map 𝒪_{Z,g(y)} → 𝒪_{Y,y} is an unramified local homomorphism, so 𝔪_{g(y)} 𝒪_{Y,y} = 𝔪_y (map_maximalIdeal_stalkMap_of_etale; [TSPA, Tag 00UW]; Mathlib's FormallyUnramified.stalkMap, Algebra.FormallyUnramified.map_maximalIdeal). For a coordinate system this says that the coordinates together with parameters of φ_u(x) generate 𝔪_x; at a k-rational point, 𝔪_x = (u_i − u_i(x)).

Used for the point (p, p) of the graph of two coordinate systems (GraphCompletion.lean, TwoPointEtalePair.lean) and in HironakaExamples/OrderReduction/Example106.lean and HironakaExamples/Sequence/Remark33Warning63.lean.

The origin of 𝔸ⁿ_k

theorem AlgebraicGeometry.X_mem_origin_asIdeal (k : Type u) [Field k] (n : ℕ) (i : Fin n) : MvPolynomial.X i ∈ (origin k n).asIdeal

theorem AlgebraicGeometry.origin_asIdeal_le_of_forall_X_mem (k : Type u) [Field k] (n : ℕ) (I : Ideal (MvPolynomial (Fin n) k)) (hI : ∀ (i : Fin n), MvPolynomial.X i ∈ I) : (origin k n).asIdeal ≤ I

A polynomial vanishing at the origin lies in the ideal (t_0, …, t_{n-1}).

theorem AlgebraicGeometry.eq_origin_iff_forall_X_mem (k : Type u) [Field k] (n : ℕ) (y : ↥(Spec ↧(MvPolynomial (Fin n) k))) : y = origin k n ↔ ∀ (i : Fin n), MvPolynomial.X i ∈ y.asIdeal

A point of 𝔸ⁿ_k is the origin iff its prime contains every coordinate t_i.

The image point of a coordinate morphism

theorem AlgebraicGeometry.toAffineSpace_base_apply {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) {n : ℕ} {U : X.Opens} (hU : IsAffineOpen U) (v : Fin n → ↑(X.presheaf.obj (Opposite.op U))) (x : ↥U) : (toAffineSpace f U v) x = PrimeSpectrum.comap (MvPolynomial.aeval v).toRingHom (hU.primeIdealOf x)

The point φ_v(x) ∈ 𝔸ⁿ_k: the prime (aeval v)⁻¹(𝔭_x) of k[t], 𝔭_x the prime of x in Γ(X, U).

theorem AlgebraicGeometry.X_mem_toAffineSpace_base_iff {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) {n : ℕ} {U : X.Opens} (hU : IsAffineOpen U) (v : Fin n → ↑(X.presheaf.obj (Opposite.op U))) (x : ↥U) (i : Fin n) : MvPolynomial.X i ∈ ((toAffineSpace f U v) x).asIdeal ↔ (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) (v i) ∈ IsLocalRing.maximalIdeal ↑(X.presheaf.stalk ↑x)

The coordinate t_i vanishes at φ_v(x) iff the germ (v_i)_x lies in 𝔪_x.

theorem AlgebraicGeometry.toAffineSpace_base_eq_origin_iff {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) {n : ℕ} {U : X.Opens} (hU : IsAffineOpen U) (v : Fin n → ↑(X.presheaf.obj (Opposite.op U))) (x : ↥U) : (toAffineSpace f U v) x = origin k n ↔ ∀ (i : Fin n), (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) (v i) ∈ IsLocalRing.maximalIdeal ↑(X.presheaf.stalk ↑x)

φ_v(x) = 0 iff every coordinate v_i vanishes at x (the coordinate systems of [Kol07, 95] send p to 0).

theorem AlgebraicGeometry.toAffineSpace_base_eq {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) {n : ℕ} {U : X.Opens} (hU : IsAffineOpen U) (v v' : Fin n → ↑(X.presheaf.obj (Opposite.op U))) (x : ↥U) (hv : ∀ (i : Fin n), (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) (v i) ∈ IsLocalRing.maximalIdeal ↑(X.presheaf.stalk ↑x)) (hv' : ∀ (i : Fin n), (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) (v' i) ∈ IsLocalRing.maximalIdeal ↑(X.presheaf.stalk ↑x)) : (toAffineSpace f U v) x = (toAffineSpace f U v') x

Two coordinate morphisms whose coordinates all vanish at x send x to the same point (the origin).

The stalks of an étale morphism

theorem AlgebraicGeometry.map_maximalIdeal_stalkMap_of_etale {Y Z : Scheme} (g : Y ⟶ Z) [Etale g] (y : ↥Y) : Ideal.map (CommRingCat.Hom.hom (Scheme.Hom.stalkMap g y)) (IsLocalRing.maximalIdeal ↑(Z.presheaf.stalk (g y))) = IsLocalRing.maximalIdeal ↑(Y.presheaf.stalk y)

The stalk map of an étale morphism is an unramified local homomorphism essentially of finite type, so 𝔪_{g(y)} 𝒪_{Y,y} = 𝔪_y [TSPA, Tag 00UW].