The power series ring as a coordinate structure

Kollár works in R = K⟦x₁, …, xₙ⟧, a field K of characteristic zero, with its maximal ideal 𝔪 [Kol07, Notation 93]; the formal automorphisms of the form 1 + B live there, and the Cohen structure theorem identifies the completion of every regular local ℚ-algebra with coordinates with such a ring. This file makes MvPowerSeries (Fin n) K an instance of the coordinate structure IsLocalRing.RegularCoords:

• MvPowerSeries.pderiv_pderiv_comm: the formal partial derivatives commute. Mathlib has no such lemma; it follows coefficientwise from MvPowerSeries.coeff_pderiv, because both iterated derivatives have n-th coefficient (nᵢ + 1)(nⱼ + 1) (or (nᵢ + 1)(nᵢ + 2) when i = j) times the coefficient at n + eᵢ + eⱼ.
• MvPowerSeries.exists_eq_sum_X_mul, mem_span_range_X_of_constantCoeff_eq_zero, mem_span_range_X_pow_iff_le_order, maximalIdeal_eq_span_range_X: for finitely many variables the maximal ideal of K⟦X⟧ is generated by the variables, and f ∈ (X)^k iff every monomial of f has degree at least k, i.e. k ≤ order f. The decomposition f = ∑ᵢ Xᵢ gᵢ is built one variable at a time: the monomials of f containing Xₐ form Xₐ · gₐ, and the rest is handled by induction on the set of variables.
• MvPowerSeries.ordElem_eq_order: hence the order of an element in the sense of Hironaka/Algebra/Local/Order.lean is Mathlib's MvPowerSeries.order.
• IsLocalRing.RegularCoords.mvPowerSeries: the structure with x = X and ∂ᵢ = pderiv K i (restricted to a ℚ-derivation). Two of its fields are taken as explicit hypotheses: that the maximal ideal is generated by the Xᵢ (maximalIdeal_eq_span_range_X below) and that the Krull dimension is n (proved together with the regularity of K⟦X⟧, an instance argument, in Hironaka/Algebra/Local/PowerSeriesRegular.lean).

theorem MvPowerSeries.pderiv_pderiv_comm {σ : Type u_1} {R : Type u_2} [CommSemiring R] (i j : σ) (f : MvPowerSeries σ R) : (pderiv i) ((pderiv j) f) = (pderiv j) ((pderiv i) f)

The formal partial derivatives of a multivariate power series commute.

theorem MvPowerSeries.exists_eq_sum_X_mul {σ : Type u_1} {R : Type u_2} [CommSemiring R] (s : Finset σ) (f : MvPowerSeries σ R) (hf : ∀ (m : σ →₀ ℕ), (∀ i ∈ s, m i = 0) → (coeff m) f = 0) : ∃ (g : σ → MvPowerSeries σ R), f = ∑ i ∈ s, X i * g i ∧ ∀ i ∈ s, ∀ (d : σ →₀ ℕ), (coeff d) (g i) ≠ 0 → (coeff (d + Finsupp.single i 1)) f ≠ 0

Every power series whose monomials all involve a variable from the finite set s is a combination ∑ᵢ Xᵢ gᵢ over s, and the monomials of gᵢ are those of f shifted by Xᵢ (the finite-σ decomposition behind 𝔪 = (X)).

theorem MvPowerSeries.mem_span_range_X_of_constantCoeff_eq_zero {σ : Type u_1} {R : Type u_2} [CommSemiring R] [Finite σ] {f : MvPowerSeries σ R} (hf : constantCoeff f = 0) : f ∈ Ideal.span (Set.range X)

A power series with zero constant coefficient in finitely many variables lies in the ideal generated by the variables.

theorem MvPowerSeries.mem_span_range_X_pow_iff_le_order {σ : Type u_1} {R : Type u_2} [CommSemiring R] [Finite σ] (k : ℕ) (f : MvPowerSeries σ R) : f ∈ Ideal.span (Set.range X) ^ k ↔ ↑k ≤ f.order

The powers of the ideal of variables, in finitely many variables: f ∈ (X)^k iff every monomial of f has degree at least k, i.e. k ≤ order f.

theorem MvPowerSeries.maximalIdeal_eq_span_range_X (σ : Type u_1) [Finite σ] (K : Type u_2) [Field K] : IsLocalRing.maximalIdeal (MvPowerSeries σ K) = Ideal.span (Set.range X)

The maximal ideal of K⟦Xₛ : s ∈ σ⟧, σ finite, is generated by the variables (the 𝔪 of [Kol07, Notation 93]).

theorem MvPowerSeries.ordElem_eq_order {σ : Type u_1} [Finite σ] {K : Type u_2} [Field K] (f : MvPowerSeries σ K) : IsLocalRing.ordElem f = f.order

In K⟦Xₛ : s ∈ σ⟧, σ finite, the order of an element as defined here is Mathlib's MvPowerSeries.order (via 𝔪 = (X) and mem_span_range_X_pow_iff_le_order).

noncomputable def IsLocalRing.RegularCoords.mvPowerSeries (K : Type u_1) [Field K] [CharZero K] (n : ℕ) [IsRegularLocalRing (MvPowerSeries (Fin n) K)] (hspan : maximalIdeal (MvPowerSeries (Fin n) K) = Ideal.span (Set.range MvPowerSeries.X)) (hcard : ↑n = ringKrullDim (MvPowerSeries (Fin n) K)) : RegularCoords (MvPowerSeries (Fin n) K) n

The coordinate structure on K⟦X₁, …, Xₙ⟧ of [Kol07, Notation 93], with x = X and ∂ᵢ = pderiv K i. The hypotheses hspan and hcard (the maximal ideal is generated by the variables; the Krull dimension is n) and the regularity instance are supplied by MvPowerSeries.maximalIdeal_eq_span_range_X and Hironaka/Algebra/Local/PowerSeriesRegular.lean.

Equations

• One or more equations did not get rendered due to their size.