Coordinate systems as étale maps to affine space: the definitions

Kollár works with "local coordinate systems" x_1, …, x_n at a point p of a smooth k-variety ([Kol07, 95], the proof of Theorem 92), and Włodarczyk makes the notion global on an open U: "étale morphisms φ_1, φ_2 : U → 𝔸ⁿ with φ_1^*(x_i) = u_i" ([Wlo05, Lemma 2.9.5], step (0) of the proof). The étale-neighbourhood construction that compares two hypersurfaces of maximal contact (Hironaka/Scheme/Smooth/Graph.lean, Hironaka/Resolution/Algebraic/MaximalContact/Theorem92.lean) needs exactly this reading:

• EtaleCoordinates f n U: a coordinate system on the affine open U ⊆ X over k (f : X ⟶ Spec k) is an n-tuple u = (u_0, …, u_{n-1}) of sections of 𝒪_U whose coordinate morphism φ_u = toAffineSpace f U u : U ⟶ 𝔸ⁿ_k = Spec k[t_0, …, t_{n-1}] (the morphism with φ_u^*(t_i) = u_i, toAffineSpace_appTop_X) is étale. The structure EtaleCoordinatesAdapted f n r Z x is a coordinate system together with a chart around x and the adaptedness Z ∩ U = φ_u⁻¹(L); here the chart U is given and nothing is adapted.
• ratPoint a: the k-rational point a = (a_0, …, a_{n-1}) of 𝔸ⁿ_k, the prime ideal of the polynomials vanishing at a, the kernel of evaluation k[t] → k at a (maximal, as the kernel of a surjection onto the field k); origin k n is the point 0, t_0 = ⋯ = t_{n-1} = 0.

structure AlgebraicGeometry.EtaleCoordinates {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) (n : ℕ) (U : ↑X.affineOpens) : Type u

A coordinate system on the affine open U: n sections u_0, …, u_{n-1} of 𝒪_U whose coordinate morphism φ_u = (u_0, …, u_{n-1}) : U ⟶ 𝔸ⁿ_k is étale (Kollár's "local coordinate systems", [Kol07, 95]; Włodarczyk's "étale morphisms φ : U → 𝔸ⁿ with φ^*(x_i) = u_i" in the proof of [Wlo05, Lemma 2.9.5]).

• v : Fin n → ↑(X.presheaf.obj (Opposite.op ↑U))

  The coordinate functions u_0, …, u_{n-1} ∈ Γ(U, 𝒪_U).

• etale : Etale (toAffineSpace f (↑U) self.v)

  The coordinate morphism φ_u = toAffineSpace f U v : U ⟶ 𝔸ⁿ_k is étale.

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.EtaleCoordinates.hom {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) {n : ℕ} {U : ↑X.affineOpens} (c : EtaleCoordinates f n U) : ↑↑U ⟶ Spec ↧(MvPolynomial (Fin n) k)

The coordinate morphism φ_u : U ⟶ 𝔸ⁿ_k of a coordinate system u.

Equations

• AlgebraicGeometry.EtaleCoordinates.hom f c = AlgebraicGeometry.toAffineSpace f (↑U) c.v

theorem AlgebraicGeometry.surjective_aeval {k : Type u} [Field k] {n : ℕ} (a : Fin n → k) : Function.Surjective ⇑(MvPolynomial.aeval a)

Evaluation at a point of kⁿ is onto k (constants).

noncomputable def AlgebraicGeometry.ratPoint {k : Type u} [Field k] {n : ℕ} (a : Fin n → k) : ↥(Spec ↧(MvPolynomial (Fin n) k))

The k-rational point a = (a_0, …, a_{n-1}) of 𝔸ⁿ_k = Spec k[t_0, …, t_{n-1}] — the prime (maximal) ideal of the polynomials vanishing at a, the kernel of evaluation at a.

Equations

• AlgebraicGeometry.ratPoint a = { asIdeal := RingHom.ker (MvPolynomial.aeval a), isPrime := ⋯ }

theorem AlgebraicGeometry.mem_ratPoint_asIdeal_iff {k : Type u} [Field k] {n : ℕ} (a : Fin n → k) (p : MvPolynomial (Fin n) k) : p ∈ (ratPoint a).asIdeal ↔ (MvPolynomial.aeval a) p = 0

theorem AlgebraicGeometry.isMaximal_ratPoint_asIdeal {k : Type u} [Field k] {n : ℕ} (a : Fin n → k) : (ratPoint a).asIdeal.IsMaximal

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.origin (k : Type u) [Field k] (n : ℕ) : ↥(Spec ↧(MvPolynomial (Fin n) k))

The origin 0 ∈ 𝔸ⁿ_k, the k-point t_0 = ⋯ = t_{n-1} = 0. It is the common image of a point p under the coordinate morphisms of two coordinate systems whose members lie in 𝔪_p ([Kol07, 95]: "Pick local sections x_1, x_1' ∈ MC(I)", which lie in 𝔪_p since the hypersurfaces of maximal contact pass through p).

Equations

• AlgebraicGeometry.origin k n = AlgebraicGeometry.ratPoint fun (x : Fin n) => 0