The formal logarithm of a formal group law

Over a field K, the formal logarithm ChabautyColeman.FormalGroupLaw.log is the radial (Euler) antiderivative ChabautyColeman.eulerAntideriv of the row ∑_j (M⁻¹)_{ij} X_j of the invariant differential; ChabautyColeman.FormalGroupLaw.exp is its compositional inverse. That log's differential is the invariant differential (pderiv_log) uses the closedness proved in Chabauty.Series.FormalGroupLaw.Invariance together with CharZero. Over a p-adic base, coeff_log_map_padic/coeff_log_map_scale bound the p-power denominators and exists_integral_scaled_log produces the p-scaled integral form.

Main definitions

• ChabautyColeman.eulerAntideriv: the radial antiderivative (divide the degree-k part by k).
• ChabautyColeman.FormalGroupLaw.log, ChabautyColeman.FormalGroupLaw.exp.

Main statements

• ChabautyColeman.FormalGroupLaw.log_comp_exp, .exp_comp_log: log and exp are inverse.
• ChabautyColeman.FormalGroupLaw.pderiv_log, .log_subst_F: the differential of log.
• ChabautyColeman.FormalGroupLaw.exists_integral_scaled_log: the p-scaled integral logarithm.

Blueprint nodes: def:fgl-log, lem:fgl-log.

The radial (Euler) antiderivative

noncomputable def ChabautyColeman.eulerAntideriv {ι : Type u_1} {K : Type u_2} [Field K] (g : MvPowerSeries ι K) : MvPowerSeries ι K

The radial (Euler) antiderivative of a multivariate power series: divide the degree-k homogeneous part by k. (At k = 0 the junk value (0 : K)⁻¹ = 0 kills the constant term, as intended.)

Equations

• ChabautyColeman.eulerAntideriv g d = (↑(Finsupp.degree d))⁻¹ * (MvPowerSeries.coeff d) g

theorem ChabautyColeman.coeff_eulerAntideriv {ι : Type u_1} {K : Type u_2} [Field K] (g : MvPowerSeries ι K) (d : ι →₀ ℕ) : (MvPowerSeries.coeff d) (eulerAntideriv g) = (↑(Finsupp.degree d))⁻¹ * (MvPowerSeries.coeff d) g

@[simp]

theorem ChabautyColeman.constantCoeff_eulerAntideriv {ι : Type u_1} {K : Type u_2} [Field K] (g : MvPowerSeries ι K) : MvPowerSeries.constantCoeff (eulerAntideriv g) = 0

The formal logarithm and exponential

noncomputable def ChabautyColeman.FormalGroupLaw.log {K : Type u_1} [Field K] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (Φ : FormalGroupLaw K ι) (i : ι) : MvPowerSeries ι K

The formal logarithm of a formal group law over a field of characteristic zero: the radial antiderivative of the row ∑_j (M⁻¹)_{ij} X_j of the invariant differential. That its differential is the invariant differential is proved with the invariance identities.

Equations

• Φ.log i = ChabautyColeman.eulerAntideriv (∑ j : ι, Φ.diffMatrix⁻¹ i j * MvPowerSeries.X j)

@[simp]

theorem ChabautyColeman.FormalGroupLaw.constantCoeff_log {K : Type u_1} [Field K] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (Φ : FormalGroupLaw K ι) (i : ι) : MvPowerSeries.constantCoeff (Φ.log i) = 0

theorem ChabautyColeman.FormalGroupLaw.coeff_single_log {K : Type u_1} [Field K] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (Φ : FormalGroupLaw K ι) (i j : ι) : (MvPowerSeries.coeff (Finsupp.single j 1)) (Φ.log i) = if i = j then 1 else 0

The linear term of the logarithm is X i.

theorem ChabautyColeman.FormalGroupLaw.log_sub_X_order {K : Type u_1} [Field K] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (Φ : FormalGroupLaw K ι) (i : ι) (e : ι →₀ ℕ) (he : Finsupp.degree e ≤ 1) : (MvPowerSeries.coeff e) (Φ.log i - MvPowerSeries.X i) = 0

The logarithm has zero constant term and identity linear part, so Λ i - X i has order ≥ 2.

noncomputable def ChabautyColeman.FormalGroupLaw.exp {K : Type u_1} [Field K] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (Φ : FormalGroupLaw K ι) (i : ι) : MvPowerSeries ι K

The formal exponential of a formal group law: the compositional inverse of the logarithm.

Equations

• Φ.exp i = MvPowerSeries.invSubst Φ.log i

theorem ChabautyColeman.FormalGroupLaw.log_comp_exp {K : Type u_1} [Field K] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (Φ : FormalGroupLaw K ι) (i : ι) : MvPowerSeries.subst Φ.exp (Φ.log i) = MvPowerSeries.X i

Λ ∘ Exp = X: the logarithm composed with the exponential is the identity.

theorem ChabautyColeman.FormalGroupLaw.exp_comp_log {K : Type u_1} [Field K] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (Φ : FormalGroupLaw K ι) (i : ι) : MvPowerSeries.subst Φ.log (Φ.exp i) = MvPowerSeries.X i

Exp ∘ Λ = X: the exponential composed with the logarithm is the identity.

theorem ChabautyColeman.FormalGroupLaw.pderiv_log {K : Type u_1} [Field K] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (Φ : FormalGroupLaw K ι) [CharZero K] (i k : ι) : (MvPowerSeries.pderiv k) (Φ.log i) = Φ.diffMatrix⁻¹ i k

The differential of the formal logarithm is the invariant differential: ∂_k Λ_i = (M⁻¹)_{ik}. This is where characteristic zero is used: the Euler operator plus one is invertible on coefficients.

theorem ChabautyColeman.FormalGroupLaw.log_subst_F {K : Type u_1} [Field K] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (Φ : FormalGroupLaw K ι) [CharZero K] (i : ι) : MvPowerSeries.subst (fun (j : ι) => Φ.F j) (Φ.log i) = MvPowerSeries.subst (fun (s : ι) => MvPowerSeries.X (Sum.inl s)) (Φ.log i) + MvPowerSeries.subst (fun (s : ι) => MvPowerSeries.X (Sum.inr s)) (Φ.log i)

The formal logarithm is additive on the formal group law: Λ(F(X,Y)) = Λ(X) + Λ(Y) as formal power series in the two blocks of variables.

Base change of the logarithm; p-adic denominator bounds

theorem ChabautyColeman.FormalGroupLaw.coeff_log_map {O : Type u_1} {K : Type u_2} [CommRing O] [Field K] {ι : Type u_3} [Fintype ι] [DecidableEq ι] (Φ : FormalGroupLaw O ι) (f : O →+* K) (i : ι) (d : ι →₀ ℕ) : (MvPowerSeries.coeff d) ((map f Φ).log i) = (↑(Finsupp.degree d))⁻¹ * f ((MvPowerSeries.coeff d) (∑ j : ι, Φ.diffMatrix⁻¹ i j * MvPowerSeries.X j))

The coefficients of the logarithm of a base-changed formal group law: the numerator f (coeff_d (∑_j (M⁻¹)_{ij} X_j)) is integral (in the image of f), and the only denominator is the total degree deg d. This is the "denominator bookkeeping" behind convergence of the logarithm.

theorem ChabautyColeman.FormalGroupLaw.coeff_log_map_padic {O : Type u_1} {K : Type u_2} [CommRing O] [Field K] {ι : Type u_3} [Fintype ι] [DecidableEq ι] (Φ : FormalGroupLaw O ι) [IsLocalRing O] {p : ℕ} (hp : Nat.Prime p) (hpmem : ↑p ∈ IsLocalRing.maximalIdeal O) (f : O →+* K) (hfp : f ↑p ≠ 0) (i : ι) (d : ι →₀ ℕ) : ∃ (c : O), f ↑p ^ padicValNat p (Finsupp.degree d) * (MvPowerSeries.coeff d) ((map f Φ).log i) = f c

The p-power denominator bound for the logarithm of a base-changed formal group law over a local ring of residue characteristic p: multiplying the degree-d coefficient by f(p)^(v_p(deg d)) clears the denominator, landing in the image of f. So the only denominators are powers of p, with exponent v_p(deg d).

theorem ChabautyColeman.FormalGroupLaw.coeff_log_map_scale {O : Type u_1} {K : Type u_2} [CommRing O] [Field K] {ι : Type u_3} [Fintype ι] [DecidableEq ι] (Φ : FormalGroupLaw O ι) [IsLocalRing O] {p : ℕ} (hp : Nat.Prime p) (hpmem : ↑p ∈ IsLocalRing.maximalIdeal O) (f : O →+* K) (hfp : f ↑p ≠ 0) (i : ι) (d : ι →₀ ℕ) : ∃ (c : O), f ↑p ^ Finsupp.degree d * (MvPowerSeries.coeff d) ((map f Φ).log i) = f (↑p ^ (Finsupp.degree d - padicValNat p (Finsupp.degree d)) * c)

The p-scaled logarithm has integral coefficients, with the growing p-power made explicit: p^(deg d) · coeff_d Λ = f(p^(deg d - v_p(deg d)) · c). Substituting X_j ↦ p·U_j therefore lands the logarithm in O⟦U⟧, and the exponent deg d - v_p(deg d) → ∞ drives convergence on (pO)^n.

The p-scaled integral logarithm

theorem ChabautyColeman.FormalGroupLaw.exists_integral_scaled_log {O : Type u_1} {K : Type u_2} [CommRing O] [IsLocalRing O] [UniformSpace O] [Fact (IsAdic (IsLocalRing.maximalIdeal O))] [Field K] {ι : Type u_3} [Fintype ι] [DecidableEq ι] (Φ : FormalGroupLaw O ι) {p : ℕ} (hp : Nat.Prime p) (hpmem : ↑p ∈ IsLocalRing.maximalIdeal O) (f : O →+* K) (hfp : f ↑p ≠ 0) (i : ι) : ∃ (H : MvPowerSeries ι O), (∀ (d : ι →₀ ℕ), f ((MvPowerSeries.coeff d) H) = f ↑p ^ Finsupp.degree d * (MvPowerSeries.coeff d) ((map f Φ).log i)) ∧ Filter.Tendsto (fun (d : ι →₀ ℕ) => (MvPowerSeries.coeff d) H) Filter.cofinite (nhds 0)

Convergence of the logarithm on (pO)^n: after scaling the variables by p, the logarithm of the base change f_*Φ descends to a power series H with coefficients in O that tend to 0. Concretely H is the integral form of Λ(pU): its base change is the p-scaled logarithm (f (coeff_d H) = f(p)^{deg d} · coeff_d Λ) and its coefficients lie in growing powers of 𝔪, so H — hence Λ on (pO)^n via evalT — converges.