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:

@[irreducible]
noncomputable def MvPowerSeries.inv.aux {σ : Type u_1} {R : Type u_2} [Ring R] (a : 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 * xFinset.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ˣ) :

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

    Equations
    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⁻¹ * xFinset.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
      instance MvPowerSeries.instLocalRing {σ : Type u_1} {R : Type u_2} [CommRing R] [LocalRing 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] :

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

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

      Equations
      Instances For
        instance MvPowerSeries.instInv {σ : Type u_1} {k : Type u_3} [Field 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) φ)⁻¹ * xFinset.antidiagonal n, if x.2 < n then (MvPowerSeries.coeff k x.1) φ * (MvPowerSeries.coeff k x.2) φ⁻¹ else 0
        theorem MvPowerSeries.inv_eq_zero {σ : Type u_1} {k : Type u_3} [Field k] {φ : MvPowerSeries σ k} :
        @[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) :
        φ.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] :
        Equations
        @[simp]
        theorem MvPowerSeries.C_inv {σ : Type u_1} {k : Type u_3} [Field k] (r : k) :
        @[simp]
        theorem MvPowerSeries.X_inv {σ : Type u_1} {k : Type u_3} [Field k] (s : σ) :
        @[simp]
        theorem MvPowerSeries.smul_inv {σ : Type u_1} {k : Type u_3} [Field k] (r : k) (φ : MvPowerSeries σ k) :