Smooth schemes are étale-locally affine spaces

Every point x of X smooth of relative dimension n over k has an affine open neighbourhood U with an étale morphism U ⟶ 𝔸ⁿ_k ([TSPA, Tag 054L]; exists_etale_toAffineSpace). The argument of that lemma, run in coordinates chosen at the point rather than from a standard smooth presentation: κ(x) ⊗ Ω[𝒪_{X,x}⁄k] has dimension n (Ω[𝒪_{X,x}⁄k] is free of rank n, the localization of the free module of a standard smooth chart) and is spanned by the classes 1 ⊗ d a, a ∈ 𝒪_{X,x}; a basis 1 ⊗ d a_0, …, 1 ⊗ d a_{n-1} is extracted from this spanning set, the a_i are lifted to sections v_i of an affine open around x (exists_affineOpen_germ_eq), and exists_etale_toAffineSpace_of_basis (Hironaka/Scheme/Smooth/EtaleCoordinates.lean) makes (v_0, …, v_{n-1}) étale coordinates on a smaller affine open. The lifting lemma exists_affineOpen_germ_eq is used wherever elements of a stalk are spread out to sections (EtaleCoordinatesAdapted.lean, CoordinateSystemPair.lean).

theorem AlgebraicGeometry.exists_affineOpen_germ_eq {X : Scheme} {x : ↥X} (V : ↑X.affineOpens) (hxV : x ∈ ↑V) {m : ℕ} (a : Fin m → ↑(X.presheaf.stalk x)) : ∃ (U : ↑X.affineOpens) (hxU : x ∈ ↑U) (_ : ↑U ≤ ↑V) (w : Fin m → ↑(X.presheaf.obj (Opposite.op ↑U))), ∀ (i : Fin m), (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ (↑U) x hxU)) (w i) = a i

Finitely many elements of the stalk at x are germs of sections over one affine open neighbourhood of x inside a given affine open V.

theorem AlgebraicGeometry.free_kaehlerDifferential_stalk {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) (n : ℕ) [SmoothOfRelativeDimension n f] (x : ↥X) : Module.Free ↑(X.presheaf.stalk x) Ω[↑(X.presheaf.stalk x)⁄k] ∧ Module.finrank ↑(X.presheaf.stalk x) Ω[↑(X.presheaf.stalk x)⁄k] = n

Ω[𝒪_{X,x}⁄k] is free of rank n: the base change of Ω[Γ(U)⁄k], free of rank n on a standard smooth affine chart U ∋ x.

theorem AlgebraicGeometry.finrank_residueField_tensor_kaehler_stalk {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) (n : ℕ) [SmoothOfRelativeDimension n f] (x : ↥X) : Module.finrank (IsLocalRing.ResidueField ↑(X.presheaf.stalk x)) (TensorProduct (↑(X.presheaf.stalk x)) (IsLocalRing.ResidueField ↑(X.presheaf.stalk x)) Ω[↑(X.presheaf.stalk x)⁄k]) = n

dim_κ κ(x) ⊗ Ω[𝒪_{X,x}⁄k] = n at every point (base change of a free module of rank n).

theorem AlgebraicGeometry.exists_basis_tensor_kaehler_stalk {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) (n : ℕ) [SmoothOfRelativeDimension n f] (x : ↥X) : ∃ (a : Fin n → ↑(X.presheaf.stalk x)) (b : Module.Basis (Fin n) (IsLocalRing.ResidueField ↑(X.presheaf.stalk x)) (TensorProduct (↑(X.presheaf.stalk x)) (IsLocalRing.ResidueField ↑(X.presheaf.stalk x)) Ω[↑(X.presheaf.stalk x)⁄k])), ∀ (i : Fin n), b i = 1 ⊗ₜ[↑(X.presheaf.stalk x)] (KaehlerDifferential.D k ↑(X.presheaf.stalk x)) (a i)

A basis of κ(x) ⊗ Ω[𝒪_{X,x}⁄k] consisting of classes 1 ⊗ d a_i of n elements of the stalk.

theorem AlgebraicGeometry.exists_etale_toAffineSpace {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) (n : ℕ) [SmoothOfRelativeDimension n f] (x : ↥X) : ∃ (U : ↑X.affineOpens) (_ : x ∈ ↑U) (v : Fin n → ↑(X.presheaf.obj (Opposite.op ↑U))), Etale (toAffineSpace f (↑U) v)

Every point of a scheme smooth of relative dimension n over k has an affine open neighbourhood with an étale coordinate morphism to 𝔸ⁿ_k [TSPA, Tag 054L].