Power series with a left inverse for substitution

Mathlib constructs the inverse for substitution of a power series Q = uX + ⋯ whose linear coefficient u is a unit (PowerSeries.substInvOfIsUnit). This file records the converse: if a power series Q with nilpotent constant coefficient, so that it can be substituted, has a left inverse P for substitution, P(Q) = X, then the linear coefficient of Q is a unit. Indeed the chain rule gives P'(Q) * Q' = 1, so the derivative Q' is a unit of R⟦X⟧, and its constant coefficient is the linear coefficient of Q.

If moreover Q has zero constant coefficient, then Q is X times a unit of R⟦X⟧, which is the form used to change formal parameters.

Main results

• PowerSeries.isUnit_coeff_one_of_subst_eq_X: if Q can be substituted and P(Q) = X, then the linear coefficient of Q is a unit.
• PowerSeries.exists_unit_eq_X_mul_of_subst_eq_X: if constantCoeff Q = 0 and P(Q) = X, then Q = X * v for a unit v of R⟦X⟧.
• PowerSeries.subst_eq_iff_eq_subst_substInvOfIsUnit: substituting a series P = u X + ⋯ with u a unit is undone by substituting its compositional inverse: f(P) = g ↔ f = g(P⁻¹), so f is determined by f(P).
• PowerSeries.map_substInvOfIsUnit: coefficient maps commute with the explicit construction substInvOfIsUnit for any series with a unit linear coefficient; it is a compositional inverse when the constant coefficient is zero.

theorem PowerSeries.isUnit_coeff_one_of_subst_eq_X {R : Type u_1} [CommRing R] {P Q : PowerSeries R} (hQ : HasSubst Q) (h : subst Q P = X) : IsUnit ((coeff 1) Q)

A power series Q with nilpotent constant coefficient that has a left inverse P for substitution, P(Q) = X, has a unit of R as its linear coefficient.

theorem PowerSeries.exists_unit_eq_X_mul_of_subst_eq_X {R : Type u_1} [CommRing R] {P Q : PowerSeries R} (hQ : constantCoeff Q = 0) (h : subst Q P = X) : ∃ (v : (PowerSeries R)ˣ), Q = X * ↑v

A power series Q with zero constant coefficient that has a left inverse P for substitution, P(Q) = X, is X times a unit of R⟦X⟧.

theorem PowerSeries.subst_eq_iff_eq_subst_substInvOfIsUnit {R : Type u_1} [CommRing R] {P : PowerSeries R} (hP : constantCoeff P = 0) (hP' : IsUnit ((coeff 1) P)) {f g : PowerSeries R} : subst P f = g ↔ f = subst (P.substInvOfIsUnit hP') g

Substituting a series P = u X + ⋯ with u a unit is undone by substituting its compositional inverse: f(P) = g if and only if f = g(P⁻¹). In particular a power series f is determined by f(P).

@[simp]

theorem PowerSeries.map_substInvOfIsUnit {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] (f : R →+* S) {P : PowerSeries R} (hP' : IsUnit ((coeff 1) P)) : (map f) (P.substInvOfIsUnit hP') = ((map f) P).substInvOfIsUnit ⋯

Applying a ring homomorphism to the coefficients commutes with the explicit construction substInvOfIsUnit, for any series P whose linear coefficient is a unit; no condition on the constant coefficient of P is needed. When constantCoeff P = 0 this construction is the compositional inverse of P.