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.lean 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.

noncomputable 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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

theorem PowerSeries.sub_const_eq_shift_mul_X {R : Type u_1} [Ring R] (φ : PowerSeries R) : φ - C (constantCoeff φ) = (mk fun (p : ℕ) => (coeff (p + 1)) φ) * 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) : φ - C (constantCoeff φ) = X * mk fun (p : ℕ) => (coeff (p + 1)) φ

@[reducible, inline]

noncomputable abbrev 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

theorem PowerSeries.inv_eq_inv_aux {k : Type u_2} [Field k] (φ : PowerSeries k) : φ⁻¹ = inv.aux (constantCoeff φ)⁻¹ φ

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

@[simp]

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

theorem PowerSeries.inv_eq_zero {k : Type u_2} [Field k] {φ : PowerSeries k} : φ⁻¹ = 0 ↔ constantCoeff φ = 0

theorem PowerSeries.zero_inv {k : Type u_2} [Field k] : 0⁻¹ = 0

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

@[simp]

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

@[simp]

theorem PowerSeries.X_inv {k : Type u_2} [Field k] : X⁻¹ = 0

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

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

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.

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

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

@[simp]

theorem PowerSeries.Inv_divided_by_X_pow_order_rightInv {k : Type u_2} [Field k] {f : PowerSeries k} (hf : f ≠ 0) : f.divXPowOrder * 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) : Inv_divided_by_X_pow_order hf * f.divXPowOrder = 1

noncomputable 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.

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

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

@[simp]

theorem PowerSeries.Unit_of_divided_by_X_pow_order_zero {k : Type u_2} [Field k] : 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 = f.divXPowOrder ↔ IsUnit f

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

theorem PowerSeries.hasUnitMulPowIrreducibleFactorization {k : Type u_2} [Field k] : IsDiscreteValuationRing.HasUnitMulPowIrreducibleFactorization (PowerSeries k)

instance PowerSeries.instUniqueFactorizationMonoid {k : Type u_2} [Field k] : UniqueFactorizationMonoid (PowerSeries k)

instance PowerSeries.instIsDiscreteValuationRing {k : Type u_2} [Field k] : IsDiscreteValuationRing (PowerSeries k)

theorem PowerSeries.maximalIdeal_eq_span_X {k : Type u_2} [Field k] : IsLocalRing.maximalIdeal (PowerSeries k) = Ideal.span {X}

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

@[implicit_reducible]

noncomputable instance PowerSeries.instNormalizationMonoid {k : Type u_2} [Field k] : NormalizationMonoid (PowerSeries k)

theorem PowerSeries.normUnit_X {k : Type u_2} [Field k] : normUnit X = 1

theorem PowerSeries.X_eq_normalizeX {k : Type u_2} [Field k] : X = normalize X

theorem PowerSeries.normalized_count_X_eq_of_coe {k : Type u_2} [Field k] {P : Polynomial k} (hP : P ≠ 0) : Multiset.count X (UniqueFactorizationMonoid.normalizedFactors ↑P) = Multiset.count Polynomial.X (UniqueFactorizationMonoid.normalizedFactors P)

theorem PowerSeries.ker_coeff_eq_max_ideal {k : Type u_2} [Field k] : RingHom.ker constantCoeff = IsLocalRing.maximalIdeal (PowerSeries k)

noncomputable def PowerSeries.residueFieldOfPowerSeries {k : Type u_2} [Field k] : IsLocalRing.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.