Étale coordinates: the coordinate morphism U ⟶ 𝔸ⁿ_k

toAffineSpace f U v : U ⟶ 𝔸ⁿ_k = Spec k[t] is U.toSpecΓ ≫ Spec (aeval v). This module relates its properties to the ring map k[t] → Γ(X, U), t_i ↦ v_i:

• for U affine, toAffineSpace f U v is étale iff aeval v is an étale ring map (etale_toAffineSpace_iff; U.toSpecΓ is an isomorphism and Etale is a property of ring maps, Mathlib's HasRingHomProperty);
• restriction to a smaller open U' ≤ U composes with the inclusion U' ⟶ U (homOfLE_toAffineSpace), so étaleness passes to smaller opens (etale_toAffineSpace_restrict);
• the k-algebra structures Scheme.Hom.sectionsAlgebra on Γ(X, U) and Γ(X, U') form a scalar tower with the restriction map (isScalarTower_sectionsAlgebra_restrict);
• sections v of an affine open V ∋ x whose differentials at x form a basis of κ(x) ⊗ Ω[𝒪_{X,x}⁄k] are étale coordinates on a smaller affine open U ∋ x (exists_etale_toAffineSpace_of_basis), the argument of [TSPA, Tag 054L] in given coordinates: on a standard smooth affine open the d v_i generate Ω at the stalk, hence, by Nakayama spread out along a basic open (Hironaka/Algebra/Smooth/SpreadOut.lean), on an affine neighbourhood, where the étale criterion etale_aeval_of_span_eq_top (Hironaka/Algebra/Smooth/EtaleCriterion.lean) applies.

These are the tools with which étale coordinates are produced throughout Hironaka/Smooth/.

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.restrictAlgebra {X : Scheme} {U U' : X.Opens} (h : U' ≤ U) : Algebra ↑(X.presheaf.obj (Opposite.op U)) ↑(X.presheaf.obj (Opposite.op U'))

The restriction map Γ(X, U) → Γ(X, U') as an algebra structure (local use).

Equations

• AlgebraicGeometry.restrictAlgebra h = (CommRingCat.Hom.hom (X.presheaf.map (CategoryTheory.homOfLE h).op)).toAlgebra

theorem AlgebraicGeometry.isScalarTower_sectionsAlgebra_restrict {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) {U U' : X.Opens} (h : U' ≤ U) : IsScalarTower k ↑(X.presheaf.obj (Opposite.op U)) ↑(X.presheaf.obj (Opposite.op U'))

k → Γ(X, U) → Γ(X, U') is a scalar tower for the structures induced by f.

theorem AlgebraicGeometry.mem_basicOpen_iff_notMem_primeIdealOf {X : Scheme} {U : X.Opens} {x : ↥X} (hU : IsAffineOpen U) (hx : x ∈ U) (s : ↑(X.presheaf.obj (Opposite.op U))) : x ∈ X.basicOpen s ↔ s ∉ (hU.primeIdealOf ⟨x, hx⟩).asIdeal

Membership in the basic open of s at a point of an affine open, through the prime of the point.

theorem AlgebraicGeometry.etale_toAffineSpace_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))) : Etale (toAffineSpace f U v) ↔ (MvPolynomial.aeval v).Etale

For U affine, the coordinate morphism is étale iff the ring map k[t] → Γ(X, U), t_i ↦ v_i, is étale.

theorem AlgebraicGeometry.homOfLE_toAffineSpace {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) {n : ℕ} {U U' : X.Opens} (h : U' ≤ U) (v : Fin n → ↑(X.presheaf.obj (Opposite.op U))) : CategoryTheory.CategoryStruct.comp (X.homOfLE h) (toAffineSpace f U v) = toAffineSpace f U' fun (i : Fin n) => (CategoryTheory.ConcreteCategory.hom (X.presheaf.map (CategoryTheory.homOfLE h).op)) (v i)

The coordinate morphism restricted to a smaller open is the coordinate morphism of the restricted sections.

theorem AlgebraicGeometry.etale_toAffineSpace_restrict {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) {n : ℕ} {U U' : X.Opens} (h : U' ≤ U) (v : Fin n → ↑(X.presheaf.obj (Opposite.op U))) [Etale (toAffineSpace f U v)] : Etale (toAffineSpace f U' fun (i : Fin n) => (CategoryTheory.ConcreteCategory.hom (X.presheaf.map (CategoryTheory.homOfLE h).op)) (v i))

Étaleness of the coordinate morphism passes to smaller opens.

theorem AlgebraicGeometry.isStandardSmoothOfRelativeDimension_basicOpen {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) (n : ℕ) {U : X.Opens} (hU : IsAffineOpen U) (t : ↑(X.presheaf.obj (Opposite.op U))) (hstd : Algebra.IsStandardSmoothOfRelativeDimension n k ↑(X.presheaf.obj (Opposite.op U))) : Algebra.IsStandardSmoothOfRelativeDimension n k ↑(X.presheaf.obj (Opposite.op (X.basicOpen t)))

A basic open of an affine open on which X is standard smooth of relative dimension n over k is again standard smooth of relative dimension n (localization away from a section is standard smooth of relative dimension 0).

theorem AlgebraicGeometry.etale_aeval_of_isStandardSmoothOfRelativeDimension {k : Type u} [Field k] (n : ℕ) {S : Type u} [CommRing S] [Algebra k S] [Nontrivial S] [Algebra.IsStandardSmoothOfRelativeDimension n k S] (v : Fin n → S) (hspan : Submodule.span S (Set.range fun (i : Fin n) => (KaehlerDifferential.D k S) (v i)) = ⊤) : (MvPolynomial.aeval v).Etale

The instances of the étale criterion for a standard smooth algebra of relative dimension n (free Ω of rank n, formally smooth, of finite presentation).

theorem AlgebraicGeometry.exists_etale_toAffineSpace_of_basis {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) (n : ℕ) [SmoothOfRelativeDimension n f] {x : ↥X} (V : ↑X.affineOpens) (hxV : x ∈ ↑V) (v : Fin n → ↑(X.presheaf.obj (Opposite.op ↑V))) (hb : ∃ (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)) ((CategoryTheory.ConcreteCategory.hom (X.presheaf.germ (↑V) x hxV)) (v i))) : ∃ (U : ↑X.affineOpens) (_ : x ∈ ↑U) (hUV : ↑U ≤ ↑V), Etale (toAffineSpace f ↑U fun (i : Fin n) => (CategoryTheory.ConcreteCategory.hom (X.presheaf.map (CategoryTheory.homOfLE hUV).op)) (v i))

Sections v of an affine open V ∋ x whose differentials at x form a basis of κ(x) ⊗ Ω[𝒪_{X,x}⁄k] are étale coordinates on a smaller affine open U ∋ x (the argument of [TSPA, Tag 054L] in given coordinates).