Equimultiplicity of μ-constant families

DefinitionMilnor number#✓fully proved

Let \(R\) be a commutative ring and let \(f\) be a formal power series over \(R\) in variables \(z_i\) indexed by a set \(\sigma\). The Milnor number \(\mu(f) \in \mathbb{N} \cup \{\infty\}\) is the rank, as an \(R\)-module, of the quotient of this power series ring by the ideal generated by the partial derivatives \(\partial f / \partial z_i\) for \(i \in \sigma\), and \(\infty\) when that rank is infinite. For \(R = \mathbb{C}\) and \(\sigma = \{1, \dots, n\}\) it is \(\dim_{\mathbb{C}} \mathbb{C}[[z_1, \dots, z_n]] / (\partial f / \partial z_1, \dots, \partial f / \partial z_n)\).

noncomputable def milnorNumber {σ R : Type*} [CommRing R] (f : MvPowerSeries σ R) : ℕ∞ :=
  (Module.rank R (MvPowerSeries σ R ⧸ Ideal.span (Set.range (pderiv · f)))).toENat

Used by 1

Used byEquimultiplicity of μ-constant families

TheoremEquimultiplicity of μ-constant families#●ready to prove

Let \(n \in \mathbb{N}\) and let \((f_t)_{t \in [0,1]}\) be a family of formal power series in \(\mathbb{C}[[z_1, \dots, z_n]]\) such that each coefficient of \(f_t\) depends continuously on \(t\) and each \(f_t\) has zero constant term. If there is a natural number \(\mu\) such that the Milnor number of \(f_t\) equals \(\mu\) for every \(t\), then the order of \(f_t\) (the least total degree of a monomial with nonzero coefficient, \(\infty\) if \(f_t = 0\)) is the same for all \(t \in [0,1]\).

The paper calls this order the multiplicity of \(f_t\). Its Theorem 1.1 does not state that the constant terms vanish, but the hypothesis is needed: it says that each \(f_t\) is a germ \((\mathbb{C}^n, 0) \to (\mathbb{C}, 0)\), as in the paper's abstract and Corollary 1.3. For \(n = 1\) and \(f_t = z_1 + t\) the Milnor number is \(0\) for every \(t\), since the ideal of partial derivatives contains \(1\), while \(f_0\) has order \(1\) and \(f_1\) has order \(0\).

public theorem_wanted theorem_1_1 (n : ℕ) (f : unitInterval → MvPowerSeries (Fin n) ℂ)
    (cont : ∀ d, Continuous fun t ↦ coeff d (f t)) (h_const : ∀ t, constantCoeff (f t) = 0)
    (h : ∃ μ : ℕ, ∀ t, milnorNumber (f t) = μ) : ∀ t₁ t₂, (f t₁).order = (f t₂).order

Sources

• J. Fernández de Bobadilla and T. Pełka, Symplectic monodromy at radius zero and equimultiplicity of μ-constant families, Annals of Math, 200 (1) 2024. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge. Problem annals_symplectic_monodromy of the lean-eval benchmark.

Uses 1

Statement usesMilnor number

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.