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 (IsLocalRingHom f) of commutative rings is a local morphism.

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.

Equations

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

theorem MvPowerSeries.coeff_inv_aux {σ : Type u_1} {R : Type u_2} [Ring R] [DecidableEq σ] (n : σ →₀ ℕ) (a : R) (φ : MvPowerSeries σ R) : (MvPowerSeries.coeff R n) (MvPowerSeries.inv.aux a φ) = if n = 0 then a else -a * Finset.sum (Finset.antidiagonal n) fun (x : (σ →₀ ℕ) × (σ →₀ ℕ)) => if x.2 < n then (MvPowerSeries.coeff R x.1) φ * (MvPowerSeries.coeff R x.2) (MvPowerSeries.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.

Equations

• MvPowerSeries.invOfUnit φ u = MvPowerSeries.inv.aux (↑u⁻¹) φ

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

@[simp]

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

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

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

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

Equations

• ⋯ = ⋯

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

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

Equations

• ⋯ = ⋯

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

Equations

• MvPowerSeries.inv φ = MvPowerSeries.inv.aux ((MvPowerSeries.constantCoeff σ k) φ)⁻¹ φ

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

Equations

• MvPowerSeries.instInvMvPowerSeries = { inv := MvPowerSeries.inv }

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

@[simp]

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

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

Equations

• MvPowerSeries.instInvOneClassMvPowerSeries = let __src := inferInstanceAs (One (MvPowerSeries σ k)); let __src_1 := inferInstanceAs (Inv (MvPowerSeries σ k)); InvOneClass.mk ⋯

@[simp]

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

@[simp]

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

@[simp]

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