Formal (multivariate) power series - Inverses

This file defines multivariate formal power series and develops the basic properties of these objects, when it comes about multiplicative inverses.

For φ : MvPowerSeries σ R and u : Rˣ is the constant coefficient of φ, MvPowerSeries.invOfUnit φ u is a formal power series such, and MvPowerSeries.mul_invOfUnit proves that φ * invOfUnit φ u = 1. The construction of the power series invOfUnit is done by writing that relation and solving and for its coefficients by induction.

Over a field, all power series φ have an “inverse” MvPowerSeries.inv φ, which is 0 if and only if the constant coefficient of φ is zero (by MvPowerSeries.inv_eq_zero), and MvPowerSeries.mul_inv_cancel asserts the equality φ * φ⁻¹ = 1 when the constant coefficient of φ is nonzero.

Instances are defined:

• Formal power series over a local ring form a local ring.
• The morphism MvPowerSeries.map σ f : MvPowerSeries σ A →* MvPowerSeries σ B induced by a local morphism f : A →+* B (IsLocalHom f) of commutative rings is a local morphism.

@[irreducible]

noncomputable def MvPowerSeries.inv.aux {σ : Type u_1} {R : Type u_2} [Ring R] (a : R) (φ : MvPowerSeries σ R) : MvPowerSeries σ R

Auxiliary definition that unifies the totalised inverse formal power series (_)⁻¹ and the inverse formal power series that depends on an inverse of the constant coefficient invOfUnit.

theorem MvPowerSeries.coeff_inv_aux {σ : Type u_1} {R : Type u_2} [Ring R] [DecidableEq σ] (n : σ →₀ ℕ) (a : R) (φ : MvPowerSeries σ R) : (coeff R n) (inv.aux a φ) = if n = 0 then a else -a * ∑ x ∈ Finset.antidiagonal n, if x.2 < n then (coeff R x.1) φ * (coeff R x.2) (inv.aux a φ) else 0

def MvPowerSeries.invOfUnit {σ : Type u_1} {R : Type u_2} [Ring R] (φ : MvPowerSeries σ R) (u : Rˣ) : MvPowerSeries σ R

A multivariate formal power series is invertible if the constant coefficient is invertible.

theorem MvPowerSeries.coeff_invOfUnit {σ : Type u_1} {R : Type u_2} [Ring R] [DecidableEq σ] (n : σ →₀ ℕ) (φ : MvPowerSeries σ R) (u : Rˣ) : (coeff R n) (φ.invOfUnit u) = if n = 0 then ↑u⁻¹ else -↑u⁻¹ * ∑ x ∈ Finset.antidiagonal n, if x.2 < n then (coeff R x.1) φ * (coeff R x.2) (φ.invOfUnit u) else 0

@[simp]

theorem MvPowerSeries.constantCoeff_invOfUnit {σ : Type u_1} {R : Type u_2} [Ring R] (φ : MvPowerSeries σ R) (u : Rˣ) : (constantCoeff σ R) (φ.invOfUnit u) = ↑u⁻¹

@[simp]

theorem MvPowerSeries.mul_invOfUnit {σ : Type u_1} {R : Type u_2} [Ring R] (φ : MvPowerSeries σ R) (u : Rˣ) (h : (constantCoeff σ R) φ = ↑u) : φ * φ.invOfUnit u = 1

@[simp]

theorem MvPowerSeries.invOfUnit_mul {σ : Type u_1} {R : Type u_2} [Ring R] (φ : MvPowerSeries σ R) (u : Rˣ) (h : (constantCoeff σ R) φ = ↑u) : φ.invOfUnit u * φ = 1

theorem MvPowerSeries.isUnit_iff_constantCoeff {σ : Type u_1} {R : Type u_2} [Ring R] {φ : MvPowerSeries σ R} : IsUnit φ ↔ IsUnit ((constantCoeff σ R) φ)

instance MvPowerSeries.instIsLocalRing {σ : Type u_1} {R : Type u_2} [CommRing R] [IsLocalRing R] : IsLocalRing (MvPowerSeries σ R)

Multivariate formal power series over a local ring form a local ring.

instance MvPowerSeries.map.isLocalHom {σ : Type u_1} {R : Type u_2} {S : Type u_3} [CommRing R] [CommRing S] (f : R →+* S) [IsLocalHom f] : IsLocalHom (map σ f)

The map between multivariate formal power series over the same indexing set induced by a local ring hom A → B is local

def MvPowerSeries.inv {σ : Type u_1} {k : Type u_3} [Field k] (φ : MvPowerSeries σ k) : MvPowerSeries σ k

The inverse 1/f of a multivariable power series f over a field

instance MvPowerSeries.instInv {σ : Type u_1} {k : Type u_3} [Field k] : Inv (MvPowerSeries σ k)

theorem MvPowerSeries.coeff_inv {σ : Type u_1} {k : Type u_3} [Field k] [DecidableEq σ] (n : σ →₀ ℕ) (φ : MvPowerSeries σ k) : (coeff k n) φ⁻¹ = if n = 0 then ((constantCoeff σ k) φ)⁻¹ else -((constantCoeff σ k) φ)⁻¹ * ∑ x ∈ Finset.antidiagonal n, if x.2 < n then (coeff k x.1) φ * (coeff k x.2) φ⁻¹ else 0

@[simp]

theorem MvPowerSeries.constantCoeff_inv {σ : Type u_1} {k : Type u_3} [Field k] (φ : MvPowerSeries σ k) : (constantCoeff σ k) φ⁻¹ = ((constantCoeff σ k) φ)⁻¹

theorem MvPowerSeries.inv_eq_zero {σ : Type u_1} {k : Type u_3} [Field k] {φ : MvPowerSeries σ k} : φ⁻¹ = 0 ↔ (constantCoeff σ k) φ = 0

@[simp]

theorem MvPowerSeries.zero_inv {σ : Type u_1} {k : Type u_3} [Field k] : 0⁻¹ = 0

@[simp]

theorem MvPowerSeries.invOfUnit_eq {σ : Type u_1} {k : Type u_3} [Field k] (φ : MvPowerSeries σ k) (h : (constantCoeff σ k) φ ≠ 0) : φ.invOfUnit (Units.mk0 ((constantCoeff σ k) φ) h) = φ⁻¹

@[simp]

theorem MvPowerSeries.invOfUnit_eq' {σ : Type u_1} {k : Type u_3} [Field k] (φ : MvPowerSeries σ k) (u : kˣ) (h : (constantCoeff σ k) φ = ↑u) : φ.invOfUnit u = φ⁻¹

@[simp]

theorem MvPowerSeries.mul_inv_cancel {σ : Type u_1} {k : Type u_3} [Field k] (φ : MvPowerSeries σ k) (h : (constantCoeff σ k) φ ≠ 0) : φ * φ⁻¹ = 1

@[simp]

theorem MvPowerSeries.inv_mul_cancel {σ : Type u_1} {k : Type u_3} [Field k] (φ : MvPowerSeries σ k) (h : (constantCoeff σ k) φ ≠ 0) : φ⁻¹ * φ = 1

theorem MvPowerSeries.eq_mul_inv_iff_mul_eq {σ : Type u_1} {k : Type u_3} [Field k] {φ₁ φ₂ φ₃ : MvPowerSeries σ k} (h : (constantCoeff σ k) φ₃ ≠ 0) : φ₁ = φ₂ * φ₃⁻¹ ↔ φ₁ * φ₃ = φ₂

theorem MvPowerSeries.eq_inv_iff_mul_eq_one {σ : Type u_1} {k : Type u_3} [Field k] {φ ψ : MvPowerSeries σ k} (h : (constantCoeff σ k) ψ ≠ 0) : φ = ψ⁻¹ ↔ φ * ψ = 1

theorem MvPowerSeries.inv_eq_iff_mul_eq_one {σ : Type u_1} {k : Type u_3} [Field k] {φ ψ : MvPowerSeries σ k} (h : (constantCoeff σ k) ψ ≠ 0) : ψ⁻¹ = φ ↔ φ * ψ = 1

@[simp]

theorem MvPowerSeries.mul_inv_rev {σ : Type u_1} {k : Type u_3} [Field k] (φ ψ : MvPowerSeries σ k) : (φ * ψ)⁻¹ = ψ⁻¹ * φ⁻¹

instance MvPowerSeries.instInvOneClass {σ : Type u_1} {k : Type u_3} [Field k] : InvOneClass (MvPowerSeries σ k)

@[simp]

theorem MvPowerSeries.C_inv {σ : Type u_1} {k : Type u_3} [Field k] (r : k) : ((C σ k) r)⁻¹ = (C σ k) r⁻¹

@[simp]

theorem MvPowerSeries.X_inv {σ : Type u_1} {k : Type u_3} [Field k] (s : σ) : (X s)⁻¹ = 0

@[simp]

theorem MvPowerSeries.smul_inv {σ : Type u_1} {k : Type u_3} [Field k] (r : k) (φ : MvPowerSeries σ k) : (r • φ)⁻¹ = r⁻¹ • φ⁻¹