Documentation

Mathlib.RingTheory.PowerSeries.Inverse

Formal power series - Inverses #

If the constant coefficient of a formal (univariate) power series is invertible, then this formal power series is invertible. (See the discussion in Mathlib.RingTheory.MvPowerSeries.Inverse for the construction.)

Formal (univariate) power series over a local ring form a local ring.

Formal (univariate) power series over a field form a discrete valuation ring, and a normalization monoid. The definition residueFieldOfPowerSeries provides the isomorphism between the residue field of k⟦X⟧ and k, when k is a field.

def PowerSeries.inv.aux {R : Type u_1} [Ring R] :

R → PowerSeries R → PowerSeries R

Auxiliary function used for computing inverse of a power series

Equations

PowerSeries.inv.aux = MvPowerSeries.inv.aux

Instances For

theorem PowerSeries.coeff_inv_aux {R : Type u_1} [Ring R] (n : ℕ) (a : R) (φ : PowerSeries R) :

(PowerSeries.coeff R n) (PowerSeries.inv.aux a φ) = if n = 0 then a else -a * Finset.sum (Finset.antidiagonal n) fun (x : ℕ × ℕ) => if x.2 < n then (PowerSeries.coeff R x.1) φ * (PowerSeries.coeff R x.2) (PowerSeries.inv.aux a φ) else 0

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

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

Equations

PowerSeries.invOfUnit φ u = MvPowerSeries.invOfUnit φ u

Instances For

theorem PowerSeries.coeff_invOfUnit {R : Type u_1} [Ring R] (n : ℕ) (φ : PowerSeries R) (u : Rˣ) :

(PowerSeries.coeff R n) (PowerSeries.invOfUnit φ u) = if n = 0 then ↑u⁻¹ else -↑u⁻¹ * Finset.sum (Finset.antidiagonal n) fun (x : ℕ × ℕ) => if x.2 < n then (PowerSeries.coeff R x.1) φ * (PowerSeries.coeff R x.2) (PowerSeries.invOfUnit φ u) else 0

@[simp]

theorem PowerSeries.constantCoeff_invOfUnit {R : Type u_1} [Ring R] (φ : PowerSeries R) (u : Rˣ) :

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

theorem PowerSeries.mul_invOfUnit {R : Type u_1} [Ring R] (φ : PowerSeries R) (u : Rˣ) (h : (PowerSeries.constantCoeff R) φ = ↑u) :

φ * PowerSeries.invOfUnit φ u = 1

theorem PowerSeries.sub_const_eq_shift_mul_X {R : Type u_1} [Ring R] (φ : PowerSeries R) :

φ - (PowerSeries.C R) ((PowerSeries.constantCoeff R) φ) = (PowerSeries.mk fun (p : ℕ) => (PowerSeries.coeff R (p + 1)) φ) * PowerSeries.X

Two ways of removing the constant coefficient of a power series are the same.

theorem PowerSeries.sub_const_eq_X_mul_shift {R : Type u_1} [Ring R] (φ : PowerSeries R) :

φ - (PowerSeries.C R) ((PowerSeries.constantCoeff R) φ) = PowerSeries.X * PowerSeries.mk fun (p : ℕ) => (PowerSeries.coeff R (p + 1)) φ

def PowerSeries.inv {k : Type u_2} [Field k] :

PowerSeries k → PowerSeries k

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

Equations

PowerSeries.inv = MvPowerSeries.inv

Instances For

instance PowerSeries.instInvPowerSeries {k : Type u_2} [Field k] :

Inv (PowerSeries k)

Equations

PowerSeries.instInvPowerSeries = { inv := PowerSeries.inv }

theorem PowerSeries.inv_eq_inv_aux {k : Type u_2} [Field k] (φ : PowerSeries k) :

φ⁻¹ = PowerSeries.inv.aux ((PowerSeries.constantCoeff k) φ)⁻¹ φ

theorem PowerSeries.coeff_inv {k : Type u_2} [Field k] (n : ℕ) (φ : PowerSeries k) :

(PowerSeries.coeff k n) φ⁻¹ = if n = 0 then ((PowerSeries.constantCoeff k) φ)⁻¹ else -((PowerSeries.constantCoeff k) φ)⁻¹ * Finset.sum (Finset.antidiagonal n) fun (x : ℕ × ℕ) => if x.2 < n then (PowerSeries.coeff k x.1) φ * (PowerSeries.coeff k x.2) φ⁻¹ else 0

@[simp]

theorem PowerSeries.constantCoeff_inv {k : Type u_2} [Field k] (φ : PowerSeries k) :

(PowerSeries.constantCoeff k) φ⁻¹ = ((PowerSeries.constantCoeff k) φ)⁻¹

theorem PowerSeries.inv_eq_zero {k : Type u_2} [Field k] {φ : PowerSeries k} :

φ⁻¹ = 0 ↔ (PowerSeries.constantCoeff k) φ = 0

@[simp]

theorem PowerSeries.zero_inv {k : Type u_2} [Field k] :

theorem PowerSeries.invOfUnit_eq {k : Type u_2} [Field k] (φ : PowerSeries k) (h : (PowerSeries.constantCoeff k) φ ≠ 0) :

PowerSeries.invOfUnit φ (Units.mk0 ((PowerSeries.constantCoeff k) φ) h) = φ⁻¹

@[simp]

theorem PowerSeries.invOfUnit_eq' {k : Type u_2} [Field k] (φ : PowerSeries k) (u : kˣ) (h : (PowerSeries.constantCoeff k) φ = ↑u) :

PowerSeries.invOfUnit φ u = φ⁻¹

@[simp]

theorem PowerSeries.mul_inv_cancel {k : Type u_2} [Field k] (φ : PowerSeries k) (h : (PowerSeries.constantCoeff k) φ ≠ 0) :

φ * φ⁻¹ = 1

@[simp]

theorem PowerSeries.inv_mul_cancel {k : Type u_2} [Field k] (φ : PowerSeries k) (h : (PowerSeries.constantCoeff k) φ ≠ 0) :

φ⁻¹ * φ = 1

theorem PowerSeries.eq_mul_inv_iff_mul_eq {k : Type u_2} [Field k] {φ₁ : PowerSeries k} {φ₂ : PowerSeries k} {φ₃ : PowerSeries k} (h : (PowerSeries.constantCoeff k) φ₃ ≠ 0) :

φ₁ = φ₂ * φ₃⁻¹ ↔ φ₁ * φ₃ = φ₂

theorem PowerSeries.eq_inv_iff_mul_eq_one {k : Type u_2} [Field k] {φ : PowerSeries k} {ψ : PowerSeries k} (h : (PowerSeries.constantCoeff k) ψ ≠ 0) :

φ = ψ⁻¹ ↔ φ * ψ = 1

theorem PowerSeries.inv_eq_iff_mul_eq_one {k : Type u_2} [Field k] {φ : PowerSeries k} {ψ : PowerSeries k} (h : (PowerSeries.constantCoeff k) ψ ≠ 0) :

ψ⁻¹ = φ ↔ φ * ψ = 1

@[simp]

theorem PowerSeries.mul_inv_rev {k : Type u_2} [Field k] (φ : PowerSeries k) (ψ : PowerSeries k) :

(φ * ψ)⁻¹ = ψ⁻¹ * φ⁻¹

instance PowerSeries.instInvOneClassPowerSeries {k : Type u_2} [Field k] :

InvOneClass (PowerSeries k)

Equations

PowerSeries.instInvOneClassPowerSeries = let __src := inferInstanceAs (InvOneClass (MvPowerSeries Unit k)); InvOneClass.mk ⋯

@[simp]

theorem PowerSeries.C_inv {k : Type u_2} [Field k] (r : k) :

((PowerSeries.C k) r)⁻¹ = (PowerSeries.C k) r⁻¹

@[simp]

theorem PowerSeries.X_inv {k : Type u_2} [Field k] :

PowerSeries.X⁻¹ = 0

@[simp]

theorem PowerSeries.smul_inv {k : Type u_2} [Field k] (r : k) (φ : PowerSeries k) :

(r • φ)⁻¹ = r⁻¹ • φ⁻¹

def PowerSeries.firstUnitCoeff {k : Type u_2} [Field k] {f : PowerSeries k} (hf : f ≠ 0) :

firstUnitCoeff is the non-zero coefficient whose index is f.order, seen as a unit of the field. It is obtained using divided_by_X_pow_order, defined in PowerSeries.Order

Equations

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

Instances For

def PowerSeries.Inv_divided_by_X_pow_order {k : Type u_2} [Field k] {f : PowerSeries k} (hf : f ≠ 0) :

Inv_divided_by_X_pow_order is the inverse of the element obtained by diving a non-zero power series by the largest power of X dividing it. Useful to create a term of type Units, done in Unit_divided_by_X_pow_order

Equations

PowerSeries.Inv_divided_by_X_pow_order hf = PowerSeries.invOfUnit (PowerSeries.divided_by_X_pow_order hf) (PowerSeries.firstUnitCoeff hf)

Instances For

@[simp]

theorem PowerSeries.Inv_divided_by_X_pow_order_rightInv {k : Type u_2} [Field k] {f : PowerSeries k} (hf : f ≠ 0) :

PowerSeries.divided_by_X_pow_order hf * PowerSeries.Inv_divided_by_X_pow_order hf = 1

@[simp]

theorem PowerSeries.Inv_divided_by_X_pow_order_leftInv {k : Type u_2} [Field k] {f : PowerSeries k} (hf : f ≠ 0) :

PowerSeries.Inv_divided_by_X_pow_order hf * PowerSeries.divided_by_X_pow_order hf = 1

def PowerSeries.Unit_of_divided_by_X_pow_order {k : Type u_2} [Field k] (f : PowerSeries k) :

(PowerSeries k)ˣ

Unit_of_divided_by_X_pow_order is the unit power series obtained by dividing a non-zero power series by the largest power of X that divides it.

Equations

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

Instances For

theorem PowerSeries.isUnit_divided_by_X_pow_order {k : Type u_2} [Field k] {f : PowerSeries k} (hf : f ≠ 0) :

IsUnit (PowerSeries.divided_by_X_pow_order hf)

theorem PowerSeries.Unit_of_divided_by_X_pow_order_nonzero {k : Type u_2} [Field k] {f : PowerSeries k} (hf : f ≠ 0) :

↑(PowerSeries.Unit_of_divided_by_X_pow_order f) = PowerSeries.divided_by_X_pow_order hf

@[simp]

theorem PowerSeries.Unit_of_divided_by_X_pow_order_zero {k : Type u_2} [Field k] :

PowerSeries.Unit_of_divided_by_X_pow_order 0 = 1

theorem PowerSeries.eq_divided_by_X_pow_order_Iff_Unit {k : Type u_2} [Field k] {f : PowerSeries k} (hf : f ≠ 0) :

f = PowerSeries.divided_by_X_pow_order hf ↔ IsUnit f

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

IsLocalRingHom (PowerSeries.map f)

Equations

⋯ = ⋯

instance PowerSeries.instLocalRingPowerSeriesInstSemiringPowerSeriesToSemiringToCommSemiring {R : Type u_1} [CommRing R] [LocalRing R] :

LocalRing (PowerSeries R)

Equations

⋯ = ⋯

theorem PowerSeries.hasUnitMulPowIrreducibleFactorization {k : Type u_2} [Field k] :

DiscreteValuationRing.HasUnitMulPowIrreducibleFactorization (PowerSeries k)

instance PowerSeries.instUniqueFactorizationMonoidPowerSeriesToCancelCommMonoidWithZeroInstCommSemiringPowerSeriesToCommSemiringToSemifieldInstIsDomainPowerSeriesInstSemiringPowerSeriesToSemiringToRingToDivisionRingToIsDomainToCommRingToEuclideanDomainIsDedekindDomainIsDomainTo_principal_ideal_domain {k : Type u_2} [Field k] :

UniqueFactorizationMonoid (PowerSeries k)

Equations

⋯ = ⋯

instance PowerSeries.instDiscreteValuationRingPowerSeriesInstCommRingPowerSeriesToCommRingToEuclideanDomainInstIsDomainPowerSeriesInstSemiringPowerSeriesToSemiringToRingToDivisionRingToIsDomainIsDedekindDomainIsDomainTo_principal_ideal_domain {k : Type u_2} [Field k] :

DiscreteValuationRing (PowerSeries k)

Equations

⋯ = ⋯

instance PowerSeries.isNoetherianRing {k : Type u_2} [Field k] :

IsNoetherianRing (PowerSeries k)

Equations

⋯ = ⋯

theorem PowerSeries.maximalIdeal_eq_span_X {k : Type u_2} [Field k] :

LocalRing.maximalIdeal (PowerSeries k) = Ideal.span {PowerSeries.X}

The maximal ideal of k⟦X⟧ is generated by X.

instance PowerSeries.instNormalizationMonoidPowerSeriesToCancelCommMonoidWithZeroInstCommSemiringPowerSeriesToCommSemiringToSemifieldInstIsDomainPowerSeriesInstSemiringPowerSeriesToSemiringToRingToDivisionRingToIsDomainToCommRingToEuclideanDomainIsDedekindDomainIsDomainTo_principal_ideal_domain {k : Type u_2} [Field k] :

NormalizationMonoid (PowerSeries k)

Equations

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

theorem PowerSeries.ker_coeff_eq_max_ideal {k : Type u_2} [Field k] :

RingHom.ker (PowerSeries.constantCoeff k) = LocalRing.maximalIdeal (PowerSeries k)

def PowerSeries.residueFieldOfPowerSeries {k : Type u_2} [Field k] :

LocalRing.ResidueField (PowerSeries k) ≃+* k

The ring isomorphism between the residue field of the ring of power series valued in a field K and K itself.

Equations

PowerSeries.residueFieldOfPowerSeries = RingEquiv.trans (Ideal.quotEquivOfEq ⋯) (RingHom.quotientKerEquivOfSurjective ⋯)

Instances For