The analytic stalk as an instance of the regular coordinates of the Hironaka library

Kollár's local coordinates x_1, …, x_n at a point of a smooth scheme come with the derivations ∂/∂x_1, …, ∂/∂x_n, "local generators of Der_X" [Kol07, Definition 73]; the Hironaka library packages this structure on a local ring as IsLocalRing.RegularCoords R n — coordinates generating the maximal ideal, as many as the Krull dimension, with commuting derivations ∂_i and ∂_i x_j = δ_ij — together with the two conditions IsLinearOver 𝕜 (the derivations kill the constants) and SpansDerivations 𝕜 (every 𝕜-derivation is ∑_i δ(x_i) ∂_i). This module shows that the stalk 𝒪_{M,a} of an analytic manifold with the centred coordinate germs x_i − x_i(a) and the partial derivatives ∂_i of a chart (coordDerivStalk, Hironaka/Manifold/Germ/CoordDeriv.lean) is such an instance (exists_regularCoords_stalk), so that the Hironaka library's local theory of regular coordinates applies to analytic stalks:

• ∂_i (x_j − x_j(a)) = δ_ij (Hironaka/Manifold/Germ/CoordDerivChart.lean) and 𝔪_a = (x_i − x_i(a))_i (maximalIdeal_eq_span_coord');
• the ∂_i commute (coordDerivStalk_comm): through the injective Taylor homomorphism (T_a ∘ ∂_i = ∂_{X_i} ∘ T_a) this is the commutation of the formal partial derivatives ∂_{X_i}, a computation on coefficients (pderiv_comm);
• every 𝕜-derivation δ of the stalk is δ = ∑_i δ(x_i − x_i(a)) ∂_i (derivation_eq_sum_coordDerivStalk), by the uniqueness of Taylor coefficients: δ' := δ − ∑_i δ(x_i − x_i(a)) ∂_i is a 𝕜-derivation killing the coordinates, hence the polynomials in them; every germ is a polynomial plus an element of 𝔪_a^{k+1} for each k (𝔪_a^k is spanned by the monomials of degree k), a derivation lowers the order by one (Derivation.mem_pow_of_mem_pow_succ), so δ' f lies in every 𝔪_a^k, and ⋂_k 𝔪_a^k = 0 in the analytic stalk (T_a is injective and 𝕜[[X]] is (X)-adically separated, eq_zero_of_forall_mem_maximalIdeal_pow);
• 𝕜-linearity is the derivation property ∂_i (algebraMap c) = 0.

Given that 𝒪_{M,a} is a regular local ring of dimension n (Hironaka/Manifold/Germ/StalkNoetherian.lean; taken here as the hypotheses [IsRegularLocalRing 𝒪_{M,a}], n = ringKrullDim 𝒪_{M,a}), exists_regularCoords_stalk packages the instance as an existence statement. It is used for the derivative ideal sheaves (Hironaka/Manifold/IdealSheaf/Deriv.lean) and for the transport of derivations along germ maps in the maximal-contact construction (Hironaka/Manifold/MaximalContact/).

theorem Manifold.pderiv_comm {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (i j : Fin n) (F : MvPowerSeries (Fin n) 𝕜) : (MvPowerSeries.pderiv i) ((MvPowerSeries.pderiv j) F) = (MvPowerSeries.pderiv j) ((MvPowerSeries.pderiv i) F)

The formal partial derivatives ∂_{X_i} commute: on coefficients, (ν_i + 1)(ν_j + δ_ij + 1) = (ν_j + 1)(ν_i + δ_ji + 1).

@[reducible, inline]

noncomputable abbrev Manifold.centredCoord {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {a : M} (ha : a ∈ φ.source) (i : Fin n) : ↑((structureSheaf 𝕜 E M).presheaf.stalk a)

The centred coordinate germs x_i − x_i(a), abbreviated.

Equations

• Manifold.centredCoord E ψ φ hφ ha i = Manifold.coord E ψ φ hφ ha i - (Manifold.const 𝕜 E M a) ((Manifold.eval 𝕜 E M a) (Manifold.coord E ψ φ hφ ha i))

theorem Manifold.coordDerivStalk_centredCoord {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {a : M} (ha : a ∈ φ.source) (i j : Fin n) : (coordDerivStalk E ψ φ hφ ha i) (centredCoord E ψ φ hφ ha j) = if i = j then 1 else 0

theorem Manifold.coordDerivStalk_comm {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {a : M} (ha : a ∈ φ.source) (i j : Fin n) (s : ↑((structureSheaf 𝕜 E M).presheaf.stalk a)) : (coordDerivStalk E ψ φ hφ ha i) ((coordDerivStalk E ψ φ hφ ha j) s) = (coordDerivStalk E ψ φ hφ ha j) ((coordDerivStalk E ψ φ hφ ha i) s)

The partial derivatives on 𝒪_{M,a} commute (the axiom pderiv_comm of RegularCoords): through the injective Taylor homomorphism, the formal ones do.

theorem Manifold.eq_zero_of_forall_mem_maximalIdeal_pow {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {a : M} (ha : a ∈ φ.source) (s : ↑((structureSheaf 𝕜 E M).presheaf.stalk a)) (h : ∀ (k : ℕ), s ∈ IsLocalRing.maximalIdeal ↑((structureSheaf 𝕜 E M).presheaf.stalk a) ^ k) : s = 0

⋂_k 𝔪_a^k = 0 in the analytic stalk: the Taylor homomorphism is injective and sends 𝔪_a^k into (X)^k, and 𝕜[[X]] is (X)-adically separated.

theorem Manifold.exists_mem_adjoin_sub_mem_maximalIdeal_pow {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {a : M} (ha : a ∈ φ.source) (k : ℕ) (f : ↑((structureSheaf 𝕜 E M).presheaf.stalk a)) : ∃ p ∈ Algebra.adjoin 𝕜 (Set.range (centredCoord E ψ φ hφ ha)), f - p ∈ IsLocalRing.maximalIdeal ↑((structureSheaf 𝕜 E M).presheaf.stalk a) ^ k

Every germ is a polynomial in the centred coordinates plus an element of 𝔪_a^k: 𝔪_a^k is spanned by the monomials of degree k, and a coefficient g of such a monomial is its value g(a) plus an element of 𝔪_a.

theorem Manifold.derivation_eq_sum_coordDerivStalk {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {a : M} (ha : a ∈ φ.source) (δ : Derivation 𝕜 ↑((structureSheaf 𝕜 E M).presheaf.stalk a) ↑((structureSheaf 𝕜 E M).presheaf.stalk a)) (s : ↑((structureSheaf 𝕜 E M).presheaf.stalk a)) : δ s = ∑ i : Fin n, δ (centredCoord E ψ φ hφ ha i) * (coordDerivStalk E ψ φ hφ ha i) s

Every 𝕜-derivation δ of the stalk is δ = ∑_i δ(x_i − x_i(a)) ∂_i (the condition SpansDerivations 𝕜; Kollár's "∂/∂x_1, …, ∂/∂x_n are local generators of Der_X" [Kol07, Definition 73]), by the uniqueness of Taylor coefficients: δ' = δ − ∑_i δ(x_i − x_i(a)) ∂_i kills the polynomials in the coordinates and lowers the order, so δ' f ∈ ⋂_k 𝔪_a^k = 0.

theorem Manifold.exists_regularCoords_stalk {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {a : M} (ha : a ∈ φ.source) [IsRegularLocalRing ↑((structureSheaf 𝕜 E M).presheaf.stalk a)] (hdim : ↑n = ringKrullDim ↑((structureSheaf 𝕜 E M).presheaf.stalk a)) : ∃ (c : IsLocalRing.RegularCoords (↑((structureSheaf 𝕜 E M).presheaf.stalk a)) n), (∀ (i : Fin n), c.x i = centredCoord E ψ φ hφ ha i) ∧ (∀ (i : Fin n), c.pderiv i = Derivation.restrictScalars ℚ (coordDerivStalk E ψ φ hφ ha i)) ∧ c.IsLinearOver 𝕜 ∧ c.SpansDerivations 𝕜

Given that 𝒪_{M,a} is a regular local ring of dimension n, the stalk carries the regular coordinates RegularCoords of the Hironaka library, with x_i the centred coordinate germs and ∂_i the partial derivatives of the chart, 𝕜-linear (IsLinearOver 𝕜) and spanning the 𝕜-derivations (SpansDerivations 𝕜).