Compositional inverses of multivariate formal substitutions

A family a : σ → MvPowerSeries σ R is a formal self-map X ↦ (a_i(X)); composition of two such maps is (a ∘ b)_i = subst b (a_i), with the identity X. Associativity is MvPowerSeries.subst_comp_subst_apply and the identity laws are subst_X and subst_self, so these maps form a monoid (subject to the HasSubst side conditions). This file records the resulting uniqueness of compositional inverses; the construction of the inverse for a map with identity linear part is developed separately.

theorem MvPowerSeries.leftInv_eq_rightInv {σ : Type u_1} {R : Type u_2} [CommRing R] {a E F : σ → MvPowerSeries σ R} (hE : HasSubst E) (hF : HasSubst a) (hFa : ∀ (i : σ), subst a (F i) = X i) (haE : ∀ (i : σ), subst E (a i) = X i) : E = F

A left compositional inverse equals a right compositional inverse. If F is a left inverse of a (F ∘ a = X, i.e. subst a (F i) = X i) and E is a right inverse (a ∘ E = X, i.e. subst E (a i) = X i), then E = F. In particular the compositional inverse of a formal substitution, when it exists, is unique.

def MvPowerSeries.AgreeBelow {σ : Type u_1} {R : Type u_2} [CommRing R] (k : ℕ) (f g : MvPowerSeries σ R) : Prop

Two power series agree below degree k if their coefficients coincide in all degrees < k.

Equations

• MvPowerSeries.AgreeBelow k f g = ∀ (e : σ →₀ ℕ), Finsupp.degree e < k → (MvPowerSeries.coeff e) f = (MvPowerSeries.coeff e) g

theorem MvPowerSeries.AgreeBelow.mul {σ : Type u_1} {R : Type u_2} [CommRing R] {k : ℕ} {f f' g g' : MvPowerSeries σ R} (hf : AgreeBelow k f f') (hg : AgreeBelow k g g') : AgreeBelow k (f * g) (f' * g')

theorem MvPowerSeries.AgreeBelow.pow {σ : Type u_1} {R : Type u_2} [CommRing R] {k : ℕ} {f g : MvPowerSeries σ R} (h : AgreeBelow k f g) (n : ℕ) : AgreeBelow k (f ^ n) (g ^ n)

theorem MvPowerSeries.prod_pow_single_add {σ : Type u_1} {R : Type u_2} [CommRing R] (c : σ → MvPowerSeries σ R) (s : σ) (n : ℕ) (m' : σ →₀ ℕ) : ((Finsupp.single s n + m').prod fun (s : σ) (e : ℕ) => c s ^ e) = c s ^ n * m'.prod fun (s : σ) (e : ℕ) => c s ^ e

Factor one variable out of a product of powers ∏ (c s)^{m s}.

theorem MvPowerSeries.AgreeBelow.prod {σ : Type u_1} {R : Type u_2} [CommRing R] {k : ℕ} {b b' : σ → MvPowerSeries σ R} (hbb : ∀ (s : σ), AgreeBelow k (b s) (b' s)) (m : σ →₀ ℕ) : AgreeBelow k (m.prod fun (s : σ) (e : ℕ) => b s ^ e) (m.prod fun (s : σ) (e : ℕ) => b' s ^ e)

theorem MvPowerSeries.constantCoeff_prod_pow_eq_zero {σ : Type u_1} {R : Type u_2} [CommRing R] {b : σ → MvPowerSeries σ R} (hb0 : ∀ (s : σ), constantCoeff (b s) = 0) {m : σ →₀ ℕ} (hm : m ≠ 0) : constantCoeff (m.prod fun (s : σ) (e : ℕ) => b s ^ e) = 0

theorem MvPowerSeries.coeff_prod_pow_agree_boost {σ : Type u_1} {R : Type u_2} [CommRing R] {k : ℕ} {b b' : σ → MvPowerSeries σ R} (hb0 : ∀ (s : σ), constantCoeff (b s) = 0) (hb'0 : ∀ (s : σ), constantCoeff (b' s) = 0) (hbb : ∀ (s : σ), AgreeBelow k (b s) (b' s)) {m : σ →₀ ℕ} (hm2 : 2 ≤ Finsupp.degree m) {d : σ →₀ ℕ} (hd : Finsupp.degree d ≤ k) : (coeff d) (m.prod fun (s : σ) (e : ℕ) => b s ^ e) = (coeff d) (m.prod fun (s : σ) (e : ℕ) => b' s ^ e)

theorem MvPowerSeries.coeff_subst_agree_boost {σ : Type u_1} {R : Type u_2} [CommRing R] {k : ℕ} {b b' : σ → MvPowerSeries σ R} (hb : HasSubst b) (hb' : HasSubst b') (hb0 : ∀ (s : σ), constantCoeff (b s) = 0) (hb'0 : ∀ (s : σ), constantCoeff (b' s) = 0) (hbb : ∀ (s : σ), AgreeBelow k (b s) (b' s)) {g : MvPowerSeries σ R} (hg : ∀ (e : σ →₀ ℕ), Finsupp.degree e ≤ 1 → (coeff e) g = 0) {d : σ →₀ ℕ} (hd : Finsupp.degree d ≤ k) : (coeff d) (subst b g) = (coeff d) (subst b' g)

The boost lemma: substituting a series g of order ≥ 2 into two families that agree below degree k (and have zero constant coefficients) yields results agreeing below degree k + 1. This one-degree gain is what makes the fixed-point iteration for the compositional inverse converge.

noncomputable def MvPowerSeries.iterInv {σ : Type u_1} {R : Type u_2} [CommRing R] (a : σ → MvPowerSeries σ R) : ℕ → σ → MvPowerSeries σ R

The fixed-point iteration for the compositional inverse of a: iterInv 0 = X and iterInv (k+1) i = X i - (a i - X i)(iterInv k).

Equations

• MvPowerSeries.iterInv a 0 = MvPowerSeries.X
• MvPowerSeries.iterInv a k.succ = fun (i : σ) => MvPowerSeries.X i - MvPowerSeries.subst (MvPowerSeries.iterInv a k) (a i - MvPowerSeries.X i)

@[simp]

theorem MvPowerSeries.iterInv_zero {σ : Type u_1} {R : Type u_2} [CommRing R] {a : σ → MvPowerSeries σ R} : iterInv a 0 = X

theorem MvPowerSeries.iterInv_succ {σ : Type u_1} {R : Type u_2} [CommRing R] {a : σ → MvPowerSeries σ R} (n : ℕ) (i : σ) : iterInv a (n + 1) i = X i - subst (iterInv a n) (a i - X i)

@[irreducible]

noncomputable def MvPowerSeries.invSubst {σ : Type u_1} {R : Type u_2} [CommRing R] (a : σ → MvPowerSeries σ R) (i : σ) : MvPowerSeries σ R

The compositional inverse of a, assembled from the stabilized coefficients of the iteration.

Equations

• MvPowerSeries.invSubst a i d = (MvPowerSeries.coeff d) (MvPowerSeries.iterInv a (Finsupp.degree d + 1) i)

theorem MvPowerSeries.coeff_invSubst {σ : Type u_1} {R : Type u_2} [CommRing R] (a : σ → MvPowerSeries σ R) (i : σ) (d : σ →₀ ℕ) : (coeff d) (invSubst a i) = (coeff d) (iterInv a (Finsupp.degree d + 1) i)

theorem MvPowerSeries.coeff_subst_low {σ : Type u_1} {R : Type u_2} [CommRing R] {b : σ → MvPowerSeries σ R} (hb : HasSubst b) (hb0 : ∀ (s : σ), constantCoeff (b s) = 0) {g : MvPowerSeries σ R} (hg : ∀ (e' : σ →₀ ℕ), Finsupp.degree e' ≤ 1 → (coeff e') g = 0) {e : σ →₀ ℕ} (he : Finsupp.degree e ≤ 1) : (coeff e) (subst b g) = 0

theorem MvPowerSeries.constantCoeff_iterInv {σ : Type u_1} {R : Type u_2} [CommRing R] [Finite σ] {a : σ → MvPowerSeries σ R} (ha : ∀ (i : σ) (e : σ →₀ ℕ), Finsupp.degree e ≤ 1 → (coeff e) (a i - X i) = 0) (k : ℕ) (i : σ) : constantCoeff (iterInv a k i) = 0

theorem MvPowerSeries.hasSubst_iterInv {σ : Type u_1} {R : Type u_2} [CommRing R] [Finite σ] {a : σ → MvPowerSeries σ R} (ha : ∀ (i : σ) (e : σ →₀ ℕ), Finsupp.degree e ≤ 1 → (coeff e) (a i - X i) = 0) (k : ℕ) : HasSubst (iterInv a k)

theorem MvPowerSeries.agreeBelow_iterInv_succ {σ : Type u_1} {R : Type u_2} [CommRing R] [Finite σ] {a : σ → MvPowerSeries σ R} (ha : ∀ (i : σ) (e : σ →₀ ℕ), Finsupp.degree e ≤ 1 → (coeff e) (a i - X i) = 0) (k : ℕ) (i : σ) : AgreeBelow (k + 1) (iterInv a (k + 1) i) (iterInv a k i)

Consecutive iterates agree below one more degree each step: this is the boost lemma applied to the perturbation a i - X i (of order ≥ 2).

theorem MvPowerSeries.coeff_iterInv_stable {σ : Type u_1} {R : Type u_2} [CommRing R] [Finite σ] {a : σ → MvPowerSeries σ R} (ha : ∀ (i : σ) (e : σ →₀ ℕ), Finsupp.degree e ≤ 1 → (coeff e) (a i - X i) = 0) (i : σ) (d : σ →₀ ℕ) {j : ℕ} (hj : Finsupp.degree d + 1 ≤ j) : (coeff d) (iterInv a j i) = (coeff d) (iterInv a (Finsupp.degree d + 1) i)

Coefficient stabilization: from degree d.degree + 1 onward the degree-d coefficient of the iterates is constant.

theorem MvPowerSeries.constantCoeff_invSubst {σ : Type u_1} {R : Type u_2} [CommRing R] [Finite σ] {a : σ → MvPowerSeries σ R} (ha : ∀ (i : σ) (e : σ →₀ ℕ), Finsupp.degree e ≤ 1 → (coeff e) (a i - X i) = 0) (i : σ) : constantCoeff (invSubst a i) = 0

theorem MvPowerSeries.hasSubst_invSubst {σ : Type u_1} {R : Type u_2} [CommRing R] [Finite σ] {a : σ → MvPowerSeries σ R} (ha : ∀ (i : σ) (e : σ →₀ ℕ), Finsupp.degree e ≤ 1 → (coeff e) (a i - X i) = 0) : HasSubst (invSubst a)

theorem MvPowerSeries.coeff_iterInv_eq_invSubst {σ : Type u_1} {R : Type u_2} [CommRing R] [Finite σ] {a : σ → MvPowerSeries σ R} (ha : ∀ (i : σ) (e : σ →₀ ℕ), Finsupp.degree e ≤ 1 → (coeff e) (a i - X i) = 0) (i : σ) (d : σ →₀ ℕ) {j : ℕ} (hj : Finsupp.degree d + 1 ≤ j) : (coeff d) (iterInv a j i) = (coeff d) (invSubst a i)

theorem MvPowerSeries.agreeBelow_invSubst_iterInv {σ : Type u_1} {R : Type u_2} [CommRing R] [Finite σ] {a : σ → MvPowerSeries σ R} (ha : ∀ (i : σ) (e : σ →₀ ℕ), Finsupp.degree e ≤ 1 → (coeff e) (a i - X i) = 0) (k : ℕ) (i : σ) : AgreeBelow k (invSubst a i) (iterInv a k i)

theorem MvPowerSeries.subst_iterInv_eq {σ : Type u_1} {R : Type u_2} [CommRing R] [Finite σ] {a : σ → MvPowerSeries σ R} (ha : ∀ (i : σ) (e : σ →₀ ℕ), Finsupp.degree e ≤ 1 → (coeff e) (a i - X i) = 0) (k : ℕ) (i : σ) : subst (iterInv a k) (a i) = iterInv a k i + X i - iterInv a (k + 1) i

theorem MvPowerSeries.subst_invSubst {σ : Type u_1} {R : Type u_2} [CommRing R] [Finite σ] {a : σ → MvPowerSeries σ R} (ha : ∀ (i : σ) (e : σ →₀ ℕ), Finsupp.degree e ≤ 1 → (coeff e) (a i - X i) = 0) (i : σ) : subst (invSubst a) (a i) = X i

Existence of the compositional inverse: invSubst a is a right inverse of a (a ∘ invSubst a = X), for any a with zero constant term and identity linear part.

theorem MvPowerSeries.agreeBelow_iterInv_X {σ : Type u_1} {R : Type u_2} [CommRing R] [Finite σ] {a : σ → MvPowerSeries σ R} (ha : ∀ (i : σ) (e : σ →₀ ℕ), Finsupp.degree e ≤ 1 → (coeff e) (a i - X i) = 0) (k : ℕ) (i : σ) : AgreeBelow 2 (iterInv a k i) (X i)

Each iterate agrees with the identity X below degree 2: the corrections have order ≥ 2. So invSubst a again has zero constant term and identity linear part.

theorem MvPowerSeries.coeff_invSubst_sub_X {σ : Type u_1} {R : Type u_2} [CommRing R] [Finite σ] {a : σ → MvPowerSeries σ R} (ha : ∀ (i : σ) (e : σ →₀ ℕ), Finsupp.degree e ≤ 1 → (coeff e) (a i - X i) = 0) (i : σ) (e : σ →₀ ℕ) (he : Finsupp.degree e ≤ 1) : (coeff e) (invSubst a i - X i) = 0

theorem MvPowerSeries.subst_a_invSubst {σ : Type u_1} {R : Type u_2} [CommRing R] [Finite σ] {a : σ → MvPowerSeries σ R} (ha : ∀ (i : σ) (e : σ →₀ ℕ), Finsupp.degree e ≤ 1 → (coeff e) (a i - X i) = 0) (i : σ) : subst a (invSubst a i) = X i

Two-sided: invSubst a is also a left inverse of a (invSubst a ∘ a = X).