Hazewinkel's functional equation lemma

Let A be a subring of a commutative ring K, let p be a prime, let σ be a ring endomorphism of K that maps A into itself and lifts the Frobenius of A / p A, so that σ(a) ≡ a ^ p modulo p A for a ∈ A, and let s₁, s₂, … be elements of K with p sᵢ ∈ A. A power series h over K satisfies the functional equation if

h(X) - ∑_{i ≥ 1} sᵢ (σⁱ h)(X ^ (pⁱ)) ∈ A⟦X⟧,

where σⁱ h applies σⁱ to the coefficients of h. Formally the sum is truncated in each degree (TauCeti.functionalEquationSum); as p ≥ 2, this agrees with the infinite sum whenever h has zero constant coefficient. Hazewinkel's functional equation lemma says that if a power series f = b₁ X + ⋯ in one variable, with b₁ a unit of A, satisfies the functional equation, then the formal group law f⁻¹(f(X) + f(Y)) with logarithm f has all its coefficients in A, although the coefficients of f itself have denominators.

The proof characterises the integral series of zero constant coefficient as those ψ for which f(ψ) satisfies the functional equation (TauCeti.satisfiesFunctionalEquation_subst_iff). For integral ψ, the defect of f(ψ) is computed from that of f: it differs by the terms sᵢ σⁱ(bₘ) (ψ ^ (pⁱ m) - (σⁱ ψ)(X ^ (pⁱ)) ^ m), and these are integral because ψ ^ (pⁱ) ≡ (σⁱ ψ)(X ^ (pⁱ)) modulo p while p ^ (vₚ(m)) bₘ ∈ A. Conversely the lowest nonintegral coefficient of ψ would reappear, multiplied by b₁, in the defect of f(ψ). The formal group law F = f⁻¹(f(X) + f(Y)) has f(F) = f(X) + f(Y), whose defect is the sum of the integral defects of f(X) and f(Y).

With A = ℤ_(p)[v₁, v₂, …] inside K = ℚ[v₁, v₂, …], σ(vᵢ) = vᵢ ^ p and sᵢ = vᵢ / p, the lemma shows that the logarithm defined by Hazewinkel's recursion p mₙ = ∑ vᵢ σⁱ(m_(n - i)) is the logarithm of a formal group law over ℤ_(p)[v₁, v₂, …]. With σ = id and a single nonzero sₕ = 1 / p it gives the formal group law over ℤ_(p) with logarithm ∑ₖ X ^ (p ^ (h k)) / pᵏ.

Main definitions

• TauCeti.functionalEquationSum p σ s: the twisted sum h ↦ ∑_{i ≥ 1} sᵢ (σⁱ h)(X ^ (pⁱ)), truncated in degree d to the terms 1 ≤ i ≤ |d|. For p ≥ 2 and h of zero constant coefficient this is the infinite sum.
• TauCeti.SatisfiesFunctionalEquation p σ s A h: h satisfies the functional equation, that is h - functionalEquationSum p σ s h has coefficients in A.

Main results

• TauCeti.SatisfiesFunctionalEquation.natCast_pow_factorization_mul_coeff_mem: a solution f of the functional equation has p ^ (vₚ(n)) fₙ ∈ A.
• TauCeti.satisfiesFunctionalEquation_subst_iff: for a solution f = b₁ X + ⋯ with b₁ a unit of A and ψ of zero constant coefficient, f(ψ) satisfies the functional equation if and only if ψ has coefficients in A.
• TauCeti.coeff_inv_smul_𝔾ₐ_toPowerSeries_mem: Hazewinkel's functional equation lemma, the formal group law f⁻¹(f(X) + f(Y)) has coefficients in A.

References

• M. Hazewinkel, Formal Groups and Applications, Chapter I, §2 (the functional equation lemma).

noncomputable def TauCeti.functionalEquationSum {K : Type u_1} [CommRing K] {τ : Type u_2} (p : ℕ) [NeZero p] (σ : K →+* K) (s : ℕ → K) : MvPowerSeries τ K →+ MvPowerSeries τ K

The degree-truncated twisted sum of the functional equation: the coefficient of X^d is ∑_{1 ≤ i ≤ |d|} sᵢ times the coefficient of X^d in (σⁱ h)(X ^ (pⁱ)), where σⁱ h applies σⁱ to the coefficients of h; in degree zero it is 0.

For p ≥ 2 it is the infinite sum ∑_{i ≥ 1} sᵢ (σⁱ h)(X ^ (pⁱ)) in every nonzero degree d: the terms with i > |d| vanish, because pⁱ > |d| cannot divide a nonzero exponent of X^d. In degree zero the infinite sum is 0 only when h has zero constant coefficient. So for p ≥ 2 and h of zero constant coefficient this is ∑_{i ≥ 1} sᵢ (σⁱ h)(X ^ (pⁱ)); for p = 1 or a nonzero constant coefficient it is only the truncation.

@[simp]

theorem TauCeti.coeff_functionalEquationSum {K : Type u_1} [CommRing K] {τ : Type u_2} (p : ℕ) [NeZero p] (σ : K →+* K) (s : ℕ → K) (h : MvPowerSeries τ K) (d : τ →₀ ℕ) : (MvPowerSeries.coeff d) ((functionalEquationSum p σ s) h) = ∑ i ∈ Finset.Icc 1 (Finsupp.degree d), s i * (MvPowerSeries.coeff d) ((MvPowerSeries.expand (p ^ i) ⋯) ((MvPowerSeries.map (σ ^ i)) h))

The coefficient of X^d in functionalEquationSum p σ s h is the sum over 1 ≤ i ≤ |d| of sᵢ times the coefficient of X^d in (σⁱ h)(X ^ (pⁱ)).

@[simp]

theorem TauCeti.powerSeries_coeff_functionalEquationSum {K : Type u_1} [CommRing K] (p : ℕ) [NeZero p] (σ : K →+* K) (s : ℕ → K) (f : PowerSeries K) (n : ℕ) : (PowerSeries.coeff n) ((functionalEquationSum p σ s) f) = ∑ i ∈ Finset.Icc 1 n, s i * if p ^ i ∣ n then (σ ^ i) ((PowerSeries.coeff (n / p ^ i)) f) else 0

In one variable, the coefficient of Xⁿ in functionalEquationSum p σ s f is the sum of sᵢ σⁱ(f_(n / pⁱ)) over the 1 ≤ i ≤ n with pⁱ ∣ n.

def TauCeti.SatisfiesFunctionalEquation {K : Type u_1} [CommRing K] {τ : Type u_2} (p : ℕ) [NeZero p] (σ : K →+* K) (s : ℕ → K) (A : Subring K) (h : MvPowerSeries τ K) : Prop

h satisfies the functional equation for (p, σ, s) relative to the subring A: h - functionalEquationSum p σ s h has all its coefficients in A. For p ≥ 2 and h of zero constant coefficient, this says that h - ∑_{i ≥ 1} sᵢ (σⁱ h)(X ^ (pⁱ)) is integral.

theorem TauCeti.satisfiesFunctionalEquation_iff {K : Type u_1} [CommRing K] {τ : Type u_2} {p : ℕ} [NeZero p] {σ : K →+* K} {s : ℕ → K} {A : Subring K} {h : MvPowerSeries τ K} : SatisfiesFunctionalEquation p σ s A h ↔ ∀ (d : τ →₀ ℕ), (MvPowerSeries.coeff d) (h - (functionalEquationSum p σ s) h) ∈ A

h satisfies the functional equation exactly when every coefficient of h - functionalEquationSum p σ s h is in A.

theorem TauCeti.powerSeries_satisfiesFunctionalEquation_iff {K : Type u_1} [CommRing K] {p : ℕ} [NeZero p] {σ : K →+* K} {s : ℕ → K} {A : Subring K} {f : PowerSeries K} : SatisfiesFunctionalEquation p σ s A f ↔ ∀ (n : ℕ), (PowerSeries.coeff n) (f - (functionalEquationSum p σ s) f) ∈ A

In one variable, f satisfies the functional equation exactly when the coefficient of Xⁿ in f - functionalEquationSum p σ s f is in A for every n.

theorem TauCeti.SatisfiesFunctionalEquation.add {K : Type u_1} [CommRing K] {τ : Type u_2} {p : ℕ} [NeZero p] {σ : K →+* K} {s : ℕ → K} {A : Subring K} {h₁ h₂ : MvPowerSeries τ K} (h₁' : SatisfiesFunctionalEquation p σ s A h₁) (h₂' : SatisfiesFunctionalEquation p σ s A h₂) : SatisfiesFunctionalEquation p σ s A (h₁ + h₂)

Solutions of the functional equation are closed under addition.

theorem TauCeti.satisfiesFunctionalEquation_zero {K : Type u_1} [CommRing K] {τ : Type u_2} {p : ℕ} [NeZero p] {σ : K →+* K} {s : ℕ → K} {A : Subring K} : SatisfiesFunctionalEquation p σ s A 0

0 satisfies the functional equation.

theorem TauCeti.SatisfiesFunctionalEquation.neg {K : Type u_1} [CommRing K] {τ : Type u_2} {p : ℕ} [NeZero p] {σ : K →+* K} {s : ℕ → K} {A : Subring K} {h : MvPowerSeries τ K} (h' : SatisfiesFunctionalEquation p σ s A h) : SatisfiesFunctionalEquation p σ s A (-h)

Solutions of the functional equation are closed under negation.

theorem TauCeti.SatisfiesFunctionalEquation.sub {K : Type u_1} [CommRing K] {τ : Type u_2} {p : ℕ} [NeZero p] {σ : K →+* K} {s : ℕ → K} {A : Subring K} {h₁ h₂ : MvPowerSeries τ K} (h₁' : SatisfiesFunctionalEquation p σ s A h₁) (h₂' : SatisfiesFunctionalEquation p σ s A h₂) : SatisfiesFunctionalEquation p σ s A (h₁ - h₂)

Solutions of the functional equation are closed under subtraction.

theorem TauCeti.SatisfiesFunctionalEquation.natCast_pow_factorization_mul_coeff_mem {K : Type u_1} [CommRing K] {p : ℕ} [hp : Fact (Nat.Prime p)] {σ : K →+* K} {s : ℕ → K} {A : Subring K} (hσ : Set.MapsTo ⇑σ ↑A ↑A) (hs : ∀ (i : ℕ), ↑p * s i ∈ A) {f : PowerSeries K} (hf : SatisfiesFunctionalEquation p σ s A f) (n : ℕ) : ↑p ^ n.factorization p * (PowerSeries.coeff n) f ∈ A

Denominators of a solution of the functional equation. If f satisfies the functional equation, then p ^ (vₚ(n)) fₙ ∈ A for the coefficient fₙ of Xⁿ.

theorem TauCeti.SatisfiesFunctionalEquation.subst {K : Type u_1} [CommRing K] {τ : Type u_2} {p : ℕ} [hp : Fact (Nat.Prime p)] {σ : K →+* K} {s : ℕ → K} {A : Subring K} (hσ : Set.MapsTo ⇑σ ↑A ↑A) (hσp : ∀ a ∈ A, ∃ b ∈ A, σ a - a ^ p = ↑p * b) (hs : ∀ (i : ℕ), ↑p * s i ∈ A) {f : PowerSeries K} (hf₀ : PowerSeries.constantCoeff f = 0) (hf : SatisfiesFunctionalEquation p σ s A f) {ψ : MvPowerSeries τ K} (hψ₀ : MvPowerSeries.constantCoeff ψ = 0) (hψ : ∀ (d : τ →₀ ℕ), (MvPowerSeries.coeff d) ψ ∈ A) : SatisfiesFunctionalEquation p σ s A (PowerSeries.subst ψ f)

If f satisfies the functional equation and ψ is an integral power series of zero constant coefficient, in any number of variables, then f(ψ) satisfies the functional equation.

theorem TauCeti.coeff_mem_of_satisfiesFunctionalEquation_subst {K : Type u_1} [CommRing K] {τ : Type u_2} {p : ℕ} [hp : Fact (Nat.Prime p)] {σ : K →+* K} {s : ℕ → K} {A : Subring K} (hσ : Set.MapsTo ⇑σ ↑A ↑A) (hσp : ∀ a ∈ A, ∃ b ∈ A, σ a - a ^ p = ↑p * b) (hs : ∀ (i : ℕ), ↑p * s i ∈ A) {f : PowerSeries K} (hf₀ : PowerSeries.constantCoeff f = 0) (hf₁ : ∃ u ∈ A, u * (PowerSeries.coeff 1) f = 1) (hf : SatisfiesFunctionalEquation p σ s A f) {ψ : MvPowerSeries τ K} (hψ₀ : MvPowerSeries.constantCoeff ψ = 0) (h : SatisfiesFunctionalEquation p σ s A (PowerSeries.subst ψ f)) (d : τ →₀ ℕ) : (MvPowerSeries.coeff d) ψ ∈ A

Let f = b₁ X + ⋯ satisfy the functional equation, with b₁ a unit of A. If ψ has zero constant coefficient and f(ψ) satisfies the functional equation, then ψ has coefficients in A.

theorem TauCeti.satisfiesFunctionalEquation_subst_iff {K : Type u_1} [CommRing K] {τ : Type u_2} {p : ℕ} [hp : Fact (Nat.Prime p)] {σ : K →+* K} {s : ℕ → K} {A : Subring K} (hσ : Set.MapsTo ⇑σ ↑A ↑A) (hσp : ∀ a ∈ A, ∃ b ∈ A, σ a - a ^ p = ↑p * b) (hs : ∀ (i : ℕ), ↑p * s i ∈ A) {f : PowerSeries K} (hf₀ : PowerSeries.constantCoeff f = 0) (hf₁ : ∃ u ∈ A, u * (PowerSeries.coeff 1) f = 1) (hf : SatisfiesFunctionalEquation p σ s A f) {ψ : MvPowerSeries τ K} (hψ₀ : MvPowerSeries.constantCoeff ψ = 0) : SatisfiesFunctionalEquation p σ s A (PowerSeries.subst ψ f) ↔ ∀ (d : τ →₀ ℕ), (MvPowerSeries.coeff d) ψ ∈ A

Integral substitutions. Let f = b₁ X + ⋯ satisfy the functional equation, with b₁ a unit of A. A power series ψ of zero constant coefficient has coefficients in A if and only if f(ψ) satisfies the functional equation.

theorem TauCeti.coeff_inv_smul_𝔾ₐ_toPowerSeries_mem {K : Type u_1} [CommRing K] {p : ℕ} [hp : Fact (Nat.Prime p)] {σ : K →+* K} {s : ℕ → K} {A : Subring K} (hσ : Set.MapsTo ⇑σ ↑A ↑A) (hσp : ∀ a ∈ A, ∃ b ∈ A, σ a - a ^ p = ↑p * b) (hs : ∀ (i : ℕ), ↑p * s i ∈ A) (f : FormalCoordinate K) (hf₁ : ∃ u ∈ A, u * (PowerSeries.coeff 1) f.toPowerSeries = 1) (hf : SatisfiesFunctionalEquation p σ s A f.toPowerSeries) (d : Fin 2 →₀ ℕ) : (MvPowerSeries.coeff d) (f⁻¹ • FormalGroup.𝔾ₐ).toPowerSeries ∈ A

Hazewinkel's functional equation lemma. Let f = b₁ X + ⋯ be a formal coordinate over K whose linear coefficient b₁ is a unit of A, and suppose that f satisfies the functional equation. Then the formal group law f⁻¹(f(X) + f(Y)) with logarithm f, the transport f⁻¹ • 𝔾ₐ of the additive formal group law, has all its coefficients in A.