Documentation

Mathlib.RingTheory.MvPowerSeries.Inverse

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.

Equations

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

Instances For

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 * ∑ x ∈ Finset.antidiagonal n, 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

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

Instances For

theorem MvPowerSeries.coeff_invOfUnit {σ : Type u_1} {R : Type u_2} [Ring R] [DecidableEq σ] (n : σ →₀ ℕ) (φ : MvPowerSeries σ R) (u : Rˣ) :

(MvPowerSeries.coeff R n) (φ.invOfUnit u) = if n = 0 then ↑u⁻¹ else -↑u⁻¹ * ∑ x ∈ Finset.antidiagonal n, if x.2 < n then (MvPowerSeries.coeff R x.1) φ * (MvPowerSeries.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ˣ) :

(MvPowerSeries.constantCoeff σ R) (φ.invOfUnit u) = ↑u⁻¹

@[simp]

theorem MvPowerSeries.mul_invOfUnit {σ : Type u_1} {R : Type u_2} [Ring R] (φ : MvPowerSeries σ R) (u : Rˣ) (h : (MvPowerSeries.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 : (MvPowerSeries.constantCoeff σ R) φ = ↑u) :

φ.invOfUnit u * φ = 1

theorem MvPowerSeries.isUnit_iff_constantCoeff {σ : Type u_1} {R : Type u_2} [Ring R] {φ : MvPowerSeries σ R} :

IsUnit φ ↔ IsUnit ((MvPowerSeries.constantCoeff σ R) φ)

instance MvPowerSeries.instLocalRing {σ : 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

⋯ = ⋯

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

IsLocalHom (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

@[deprecated MvPowerSeries.map.isLocalHom]

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

IsLocalHom (MvPowerSeries.map σ f)

Alias of MvPowerSeries.map.isLocalHom.

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

Equations

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

Instances For

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

Inv (MvPowerSeries σ k)

Equations

MvPowerSeries.instInv = { 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) φ)⁻¹ * ∑ x ∈ Finset.antidiagonal n, 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] :

@[simp]

theorem MvPowerSeries.invOfUnit_eq {σ : Type u_1} {k : Type u_3} [Field k] (φ : MvPowerSeries σ k) (h : (MvPowerSeries.constantCoeff σ k) φ ≠ 0) :

φ.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) :

φ.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.instInvOneClass {σ : Type u_1} {k : Type u_3} [Field k] :

InvOneClass (MvPowerSeries σ k)

Equations

MvPowerSeries.instInvOneClass = 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⁻¹ • φ⁻¹