Exchanging the variables of an iterated power series

A power series in v whose coefficients are power series in u, an element of R⟦X⟧⟦X⟧, is a power series in the two variables u and v: the coefficient of uᵃ vᵇ in G is coeff a (coeff b G). This file defines the exchange of the two variables, PowerSeries.swap, as a ring homomorphism. It is an involution.

Main definitions

• PowerSeries.swap: the ring homomorphism R⟦X⟧⟦X⟧ → R⟦X⟧⟦X⟧ exchanging the two variables.

Main results

• PowerSeries.coeff_coeff_swap: the coefficient of uᵃ vᵇ in swap G is that of uᵇ vᵃ in G.
• PowerSeries.swap_swap: swap is an involution.
• PowerSeries.swap_C, PowerSeries.swap_map_C, PowerSeries.swap_X: swap exchanges the power series in the inner variable u, embedded as constants, with those in the outer variable v, embedded through map C.
• PowerSeries.coeff_constantCoeff_swap: setting the outer variable of swap G to zero sets the inner variable of G to zero.
• PowerSeries.coeff_swap_derivative: after exchanging the variables, the derivative in the outer variable becomes the derivative of each coefficient in the inner variable.
• Polynomial.coeff_coeff_swapPowerSeries: the coefficient of Xⁱ in the tᵏ-coefficient of swapPowerSeries Q is the tᵏ-coefficient of the coefficient of Xⁱ in Q.
• Polynomial.swapPowerSeries_C, Polynomial.swapPowerSeries_X: the values of swapPowerSeries on constants and on the polynomial variable.
• Polynomial.swapPowerSeries_injective: swapPowerSeries is injective.
• Polynomial.coeff_swapPowerSeries_mem_degreeLT: swapPowerSeries preserves degree bounds coefficientwise.
• Polynomial.exists_monic_swapPowerSeries_eq: the power series with monic constant coefficient and degree-bounded higher coefficients are exactly images of monic polynomials.

noncomputable def PowerSeries.swap {R : Type u_1} [Semiring R] : PowerSeries (PowerSeries R) →+* PowerSeries (PowerSeries R)

The exchange of the two variables of R⟦X⟧⟦X⟧, viewed as power series in u and v: the coefficient of uᵃ vᵇ in swap G is the coefficient of uᵇ vᵃ in G.

@[simp]

theorem PowerSeries.coeff_coeff_swap {R : Type u_1} [Semiring R] (G : PowerSeries (PowerSeries R)) (a b : ℕ) : (coeff a) ((coeff b) (swap G)) = (coeff b) ((coeff a) G)

The coefficient of uᵃ vᵇ in swap G is the coefficient of uᵇ vᵃ in G.

@[simp]

theorem PowerSeries.swap_swap {R : Type u_1} [Semiring R] (G : PowerSeries (PowerSeries R)) : swap (swap G) = G

Exchanging the variables twice is the identity.

@[simp]

theorem PowerSeries.swap_C {R : Type u_1} [Semiring R] (f : PowerSeries R) : swap (C f) = (map C) f

Exchanging the variables sends a power series in the inner variable u to the same power series in the outer variable v.

@[simp]

theorem PowerSeries.swap_map_C {R : Type u_1} [Semiring R] (f : PowerSeries R) : swap ((map C) f) = C f

Exchanging the variables sends a power series in the outer variable v to the same power series in the inner variable u.

@[simp]

theorem PowerSeries.swap_X {R : Type u_1} [Semiring R] : swap X = C X

Exchanging the variables sends the outer variable v to the inner variable u.

@[simp]

theorem PowerSeries.coeff_constantCoeff_swap {R : Type u_1} [Semiring R] (G : PowerSeries (PowerSeries R)) (a : ℕ) : (coeff a) (constantCoeff (swap G)) = constantCoeff ((coeff a) G)

Setting the outer variable v of swap G to zero sets the inner variable u of G to zero: the coefficient of uᵃ in the constant coefficient of swap G is the constant coefficient of the coefficient of vᵃ in G.

@[simp]

theorem PowerSeries.coeff_swap_derivative {R : Type u_2} [CommSemiring R] (G : PowerSeries (PowerSeries R)) (N : ℕ) : (coeff N) (swap (derivative G)) = derivative ((coeff N) (swap G))

Exchanging the variables turns the outer derivative into the inner one: the coefficient of vᴺ in swap (d G / dv) is the derivative in u of the coefficient of vᴺ in swap G.

noncomputable def Polynomial.swapPowerSeries {R : Type u_1} [CommSemiring R] : Polynomial (PowerSeries R) →+* PowerSeries (Polynomial R)

The ring homomorphism R⟦X⟧[X] →+* R[X]⟦X⟧ exchanging the two variables: a polynomial in X whose coefficients are power series in t is sent to the power series in t whose coefficients are polynomials in X.

@[simp]

theorem Polynomial.swapPowerSeries_C {R : Type u_1} [CommSemiring R] (a : PowerSeries R) : swapPowerSeries (C a) = (PowerSeries.map C) a

swapPowerSeries sends a constant polynomial with coefficient a : R⟦t⟧ to the same power series in t with constant polynomial coefficients.

@[simp]

theorem Polynomial.swapPowerSeries_X {R : Type u_1} [CommSemiring R] : swapPowerSeries X = PowerSeries.C X

swapPowerSeries sends the polynomial variable to the constant power series X.

@[simp]

theorem Polynomial.coeff_coeff_swapPowerSeries {R : Type u_1} [CommSemiring R] (Q : Polynomial (PowerSeries R)) (k i : ℕ) : ((PowerSeries.coeff k) (swapPowerSeries Q)).coeff i = (PowerSeries.coeff k) (Q.coeff i)

The coefficient of Xⁱ in the tᵏ-coefficient of swapPowerSeries Q is the tᵏ-coefficient of the coefficient of Xⁱ in Q.

@[simp]

theorem Polynomial.constantCoeff_swapPowerSeries {R : Type u_1} [CommSemiring R] (Q : Polynomial (PowerSeries R)) : PowerSeries.constantCoeff (swapPowerSeries Q) = map PowerSeries.constantCoeff Q

The constant coefficient of swapPowerSeries Q is the reduction of Q modulo t.

theorem Polynomial.swapPowerSeries_injective {R : Type u_1} [CommSemiring R] : Function.Injective ⇑swapPowerSeries

A polynomial over R⟦t⟧ is determined by its image under swapPowerSeries.

theorem Polynomial.coeff_swapPowerSeries_mem_degreeLT {R : Type u_1} [CommSemiring R] {Q : Polynomial (PowerSeries R)} {n : ℕ} (hQ : Q ∈ degreeLT (PowerSeries R) n) (k : ℕ) : (PowerSeries.coeff k) (swapPowerSeries Q) ∈ degreeLT R n

If Q has degree < n, then so does every coefficient of swapPowerSeries Q.

theorem Polynomial.exists_monic_swapPowerSeries_eq {S : Type u_2} [CommSemiring S] {g : Polynomial S} (hg : g.Monic) {F : PowerSeries (Polynomial S)} (hF₀ : PowerSeries.constantCoeff F = g) (hF : ∀ (k : ℕ), 1 ≤ k → (PowerSeries.coeff k) F ∈ degreeLT S g.natDegree) : ∃ (G : Polynomial (PowerSeries S)), G.Monic ∧ G.natDegree = g.natDegree ∧ map PowerSeries.constantCoeff G = g ∧ swapPowerSeries G = F

A power series F over R[X] whose constant coefficient is monic of degree d and whose other coefficients have degree < d comes from a monic polynomial over R⟦X⟧ of degree d reducing to g modulo t.