The logarithm isomorphism #
The formal logarithm Λ of a formal group law is an injective homomorphism on (pO)ⁿ
when p is odd and O is unramified (𝔪 = pO). The p-scaled log HL (with
f(coeff_d HL) = f(p)^{deg d}·coeff_d Λ) has an injective evaluation map
y ↦ (evalT y (HL i))ᵢ (ChabautyColeman.FormalGroupLaw.log_injective), which turns the
p-scaled formal group sum ChabautyColeman.FormalGroupLaw.scaledF — F(pX, pY)/p,
integral with decaying coefficients, so convergent on all of Oⁿ × Oⁿ — into addition
(ChabautyColeman.FormalGroupLaw.log_addHom); Λ(p·y) = f(evalT y (HL i)).
Both halves descend a K-power-series identity to the p-scaled integral forms — via
rescale/subst_comp_subst_apply/map_subst and f injective — and then evaluate it
with evalT_subst: injectivity descends Exp ∘ Λ = id (exp_comp_log, through
subst_descent), additivity descends Λ(F(X,Y)) = Λ(X) + Λ(Y) (log_subst_F, through
subst_scaledF_descent). The scaled log is uniquely determined by its scaling relation
(ChabautyColeman.FormalGroupLaw.scaled_log_unique), so the two packages agree.
Blueprint node: thm:log-iso.
theorem
ChabautyColeman.FormalGroupLaw.map_eq_rescale
{O : Type u_1}
[CommRing O]
{ι : Type u_2}
{K : Type u_3}
[CommRing K]
{f : O →+* K}
{p : ℕ}
{H : MvPowerSeries ι O}
{L : MvPowerSeries ι K}
(hH : ∀ (d : ι →₀ ℕ), f ((MvPowerSeries.coeff d) H) = f ↑p ^ Finsupp.degree d * (MvPowerSeries.coeff d) L)
:
theorem
ChabautyColeman.FormalGroupLaw.map_injective_of_injective
{O : Type u_1}
[CommRing O]
{ι : Type u_2}
{K : Type u_3}
[CommRing K]
{f : O →+* K}
(hf : Function.Injective ⇑f)
:
theorem
ChabautyColeman.FormalGroupLaw.map_smul_natCast
{O : Type u_1}
[CommRing O]
{ι : Type u_2}
{K : Type u_3}
[CommRing K]
{f : O →+* K}
(n : ℕ)
(h : MvPowerSeries ι O)
:
theorem
ChabautyColeman.FormalGroupLaw.rescale_const_eq_subst
{ι : Type u_2}
{K : Type u_3}
[CommRing K]
(c : K)
(L : MvPowerSeries ι K)
:
(MvPowerSeries.rescale fun (x : ι) => c) L = MvPowerSeries.subst (fun (j : ι) => c • MvPowerSeries.X j) L
theorem
ChabautyColeman.FormalGroupLaw.subst_descent
{O : Type u_1}
[CommRing O]
{ι : Type u_2}
{K : Type u_3}
[Field K]
{f : O →+* K}
{p : ℕ}
[Finite ι]
(hf : Function.Injective ⇑f)
{HL HE Hh : ι → MvPowerSeries ι O}
{Lg : ι → MvPowerSeries ι K}
{E : MvPowerSeries ι K}
{i : ι}
(hHL : ∀ (j : ι), (MvPowerSeries.map f) (HL j) = (MvPowerSeries.rescale fun (x : ι) => ↑p) (Lg j))
(hHE : (MvPowerSeries.map f) (HE i) = (MvPowerSeries.rescale fun (x : ι) => ↑p) E)
(hHh : ∀ (j : ι), ↑p • Hh j = HL j)
(hHh0 : ∀ (j : ι), MvPowerSeries.constantCoeff (Hh j) = 0)
(hLg : MvPowerSeries.HasSubst Lg)
(hcomp : MvPowerSeries.subst Lg E = MvPowerSeries.X i)
:
theorem
ChabautyColeman.FormalGroupLaw.decay_nsmul
{O : Type u_1}
[CommRing O]
[UniformSpace O]
[IsTopologicalRing O]
{ι : Type u_2}
{h : MvPowerSeries ι O}
(n : ℕ)
(hh : Filter.Tendsto (fun (d : ι →₀ ℕ) => (MvPowerSeries.coeff d) h) Filter.cofinite (nhds 0))
:
Filter.Tendsto (fun (d : ι →₀ ℕ) => (MvPowerSeries.coeff d) (n • h)) Filter.cofinite (nhds 0)
theorem
ChabautyColeman.FormalGroupLaw.evalT_nsmul
{O : Type u_1}
[CommRing O]
[IsLocalRing O]
[UniformSpace O]
[Fact (IsAdic (IsLocalRing.maximalIdeal O))]
[IsUniformAddGroup O]
[CompleteSpace O]
[T2Space O]
[IsTopologicalRing O]
{ι : Type u_2}
(z : ι → O)
(n : ℕ)
{h : MvPowerSeries ι O}
(hh : Filter.Tendsto (fun (d : ι →₀ ℕ) => (MvPowerSeries.coeff d) h) Filter.cofinite (nhds 0))
:
theorem
ChabautyColeman.FormalGroupLaw.evalT_natCast_smul
{O : Type u_1}
[CommRing O]
[IsLocalRing O]
[UniformSpace O]
[Fact (IsAdic (IsLocalRing.maximalIdeal O))]
[IsUniformAddGroup O]
[CompleteSpace O]
[T2Space O]
[IsTopologicalRing O]
{ι : Type u_2}
(z : ι → O)
(n : ℕ)
{h : MvPowerSeries ι O}
(hh : Filter.Tendsto (fun (d : ι →₀ ℕ) => (MvPowerSeries.coeff d) h) Filter.cofinite (nhds 0))
:
theorem
ChabautyColeman.FormalGroupLaw.decay_X
{O : Type u_1}
[CommRing O]
[UniformSpace O]
{ι : Type u_2}
(i : ι)
:
Filter.Tendsto (fun (d : ι →₀ ℕ) => (MvPowerSeries.coeff d) (MvPowerSeries.X i)) Filter.cofinite (nhds 0)
theorem
ChabautyColeman.FormalGroupLaw.tendsto_cancel_smul
{O : Type u_1}
[CommRing O]
[IsDomain O]
[IsLocalRing O]
[UniformSpace O]
[Fact (IsAdic (IsLocalRing.maximalIdeal O))]
{ι : Type u_2}
{p : ℕ}
{g : (ι →₀ ℕ) → O}
(hpm : IsLocalRing.maximalIdeal O = Ideal.span {↑p})
(hp0 : ↑p ≠ 0)
(hg : Filter.Tendsto (fun (d : ι →₀ ℕ) => ↑p * g d) Filter.cofinite (nhds 0))
:
theorem
ChabautyColeman.FormalGroupLaw.log_injective
{O : Type u_1}
[CommRing O]
[IsDomain O]
[IsLocalRing O]
[UniformSpace O]
[Fact (IsAdic (IsLocalRing.maximalIdeal O))]
[IsUniformAddGroup O]
[CompleteSpace O]
[T2Space O]
[IsTopologicalRing O]
{ι : Type u_2}
[Fintype ι]
[DecidableEq ι]
{K : Type u_3}
[Field K]
[CharZero K]
{f : O →+* K}
{p : ℕ}
(hp : Nat.Prime p)
(hp2 : p ≠ 2)
(hpm : IsLocalRing.maximalIdeal O = Ideal.span {↑p})
(hf : Function.Injective ⇑f)
(Φ : FormalGroupLaw O ι)
:
∃ (HL : ι → MvPowerSeries ι O),
(∀ (i : ι) (d : ι →₀ ℕ),
f ((MvPowerSeries.coeff d) (HL i)) = f ↑p ^ Finsupp.degree d * (MvPowerSeries.coeff d) ((map f Φ).log i)) ∧ Function.Injective fun (y : ι → O) (i : ι) => MvPSeries.evalT y (HL i)
Injectivity of the formal logarithm on (pO)ⁿ (p odd, unramified 𝔪 = pO).
The p-scaled log HL (with f(coeff_d HL) = f(p)^{deg d} · coeff_d Λ) has injective
evaluation map y ↦ (evalT y (HL i))ᵢ; hence Λ is injective on (pO)ⁿ.
The p-scaled formal group law #
noncomputable def
ChabautyColeman.FormalGroupLaw.scaledF
{O : Type u_4}
[CommRing O]
{ι : Type u_5}
(Φ : FormalGroupLaw O ι)
(p : ℕ)
(j : ι)
:
MvPowerSeries (ι ⊕ ι) O
The p-scaled formal group law: F(pX, pY)/p, integral because F has no constant
term. Its coefficients decay p-adically, so it evaluates on all of Oⁿ × Oⁿ.
Equations
- Φ.scaledF p j d = ↑p ^ (Finsupp.degree d - 1) * (MvPowerSeries.coeff d) (Φ.F j)
Instances For
@[simp]
theorem
ChabautyColeman.FormalGroupLaw.coeff_scaledF
{O : Type u_4}
[CommRing O]
{ι : Type u_5}
(Φ : FormalGroupLaw O ι)
(p : ℕ)
(j : ι)
(d : ι ⊕ ι →₀ ℕ)
:
(MvPowerSeries.coeff d) (Φ.scaledF p j) = ↑p ^ (Finsupp.degree d - 1) * (MvPowerSeries.coeff d) (Φ.F j)
theorem
ChabautyColeman.FormalGroupLaw.constantCoeff_scaledF
{O : Type u_4}
[CommRing O]
{ι : Type u_5}
(Φ : FormalGroupLaw O ι)
(p : ℕ)
(j : ι)
:
theorem
ChabautyColeman.FormalGroupLaw.hasSubst_scaledF
{O : Type u_4}
[CommRing O]
{ι : Type u_5}
(Φ : FormalGroupLaw O ι)
(p : ℕ)
[Finite ι]
:
theorem
ChabautyColeman.FormalGroupLaw.decay_scaledF
{O : Type u_4}
[CommRing O]
[IsLocalRing O]
[UniformSpace O]
[Fact (IsAdic (IsLocalRing.maximalIdeal O))]
{ι : Type u_5}
[Finite ι]
(Φ : FormalGroupLaw O ι)
{p : ℕ}
(hpm : IsLocalRing.maximalIdeal O = Ideal.span {↑p})
(j : ι)
:
Filter.Tendsto (fun (d : ι ⊕ ι →₀ ℕ) => (MvPowerSeries.coeff d) (Φ.scaledF p j)) Filter.cofinite (nhds 0)
The coefficients of the scaled group law tend to zero.
theorem
ChabautyColeman.FormalGroupLaw.map_scaledF_smul
{O : Type u_4}
[CommRing O]
{ι : Type u_5}
[Finite ι]
{K : Type u_6}
[Field K]
{f : O →+* K}
{p : ℕ}
(Φ : FormalGroupLaw O ι)
(j : ι)
:
↑p • (MvPowerSeries.map f) (Φ.scaledF p j) = (MvPowerSeries.rescale fun (x : ι ⊕ ι) => ↑p) ((map f Φ).F j)
The p-scaled formal group law is the p-rescaling of F, over the fraction
field.
theorem
ChabautyColeman.FormalGroupLaw.scaled_log_unique
{O : Type u_4}
[CommRing O]
{ι : Type u_5}
[Fintype ι]
[DecidableEq ι]
{K : Type u_6}
[Field K]
{f : O →+* K}
{p : ℕ}
(Φ : FormalGroupLaw O ι)
(hf : Function.Injective ⇑f)
{HL HL' : ι → MvPowerSeries ι O}
(h :
∀ (i : ι) (d : ι →₀ ℕ),
f ((MvPowerSeries.coeff d) (HL i)) = f ↑p ^ Finsupp.degree d * (MvPowerSeries.coeff d) ((map f Φ).log i))
(h' :
∀ (i : ι) (d : ι →₀ ℕ),
f ((MvPowerSeries.coeff d) (HL' i)) = f ↑p ^ Finsupp.degree d * (MvPowerSeries.coeff d) ((map f Φ).log i))
:
The p-scaled logarithms over O are uniquely determined by their scaling relation
(the base-change map f is injective), so the packages produced by
ChabautyColeman.FormalGroupLaw.log_injective and
ChabautyColeman.FormalGroupLaw.log_addHom contain the same series.
theorem
ChabautyColeman.FormalGroupLaw.subst_scaledF_descent
{O : Type u_4}
[CommRing O]
{ι : Type u_5}
[Fintype ι]
[DecidableEq ι]
{K : Type u_6}
[Field K]
{f : O →+* K}
{p : ℕ}
(Φ : FormalGroupLaw O ι)
[CharZero K]
(hf : Function.Injective ⇑f)
{HL : ι → MvPowerSeries ι O}
(hHL : ∀ (j : ι), (MvPowerSeries.map f) (HL j) = (MvPowerSeries.rescale fun (x : ι) => ↑p) ((map f Φ).log j))
(i : ι)
:
MvPowerSeries.subst (Φ.scaledF p) (HL i) = MvPowerSeries.subst (fun (s : ι) => MvPowerSeries.X (Sum.inl s)) (HL i) + MvPowerSeries.subst (fun (s : ι) => MvPowerSeries.X (Sum.inr s)) (HL i)
The descended additivity identity: the p-scaled logarithm is additive for the
p-scaled formal group law, over O.
The homomorphism property of the logarithm #
theorem
ChabautyColeman.FormalGroupLaw.log_addHom
{O : Type u_4}
[CommRing O]
[IsLocalRing O]
[UniformSpace O]
[Fact (IsAdic (IsLocalRing.maximalIdeal O))]
[IsUniformAddGroup O]
[CompleteSpace O]
[T2Space O]
[IsTopologicalRing O]
{ι : Type u_5}
[Fintype ι]
[DecidableEq ι]
{K : Type u_6}
[Field K]
[CharZero K]
{f : O →+* K}
{p : ℕ}
(hp : Nat.Prime p)
(hpm : IsLocalRing.maximalIdeal O = Ideal.span {↑p})
(hf : Function.Injective ⇑f)
(Φ : FormalGroupLaw O ι)
:
∃ (HL : ι → MvPowerSeries ι O),
(∀ (i : ι) (d : ι →₀ ℕ),
f ((MvPowerSeries.coeff d) (HL i)) = f ↑p ^ Finsupp.degree d * (MvPowerSeries.coeff d) ((map f Φ).log i)) ∧ ∀ (y z : ι → O) (i : ι),
MvPSeries.evalT (fun (j : ι) => MvPSeries.evalT (Sum.elim y z) (Φ.scaledF p j)) (HL i) = MvPSeries.evalT y (HL i) + MvPSeries.evalT z (HL i)
The formal logarithm is a homomorphism on (pO)ⁿ (p odd, unramified 𝔪 = pO):
the p-scaled log HL turns the (everywhere-convergent) p-scaled formal group sum
into addition. Together with ChabautyColeman.FormalGroupLaw.log_injective this makes
Λ an injective group homomorphism on (pO)ⁿ.
The canonical scaled logarithm #
noncomputable def
ChabautyColeman.FormalGroupLaw.scaledLog
{O : Type u_4}
[CommRing O]
[IsLocalRing O]
[UniformSpace O]
[Fact (IsAdic (IsLocalRing.maximalIdeal O))]
{ι : Type u_5}
[Fintype ι]
[DecidableEq ι]
{K : Type u_6}
[Field K]
{p : ℕ}
(Φ : FormalGroupLaw O ι)
(hp : Nat.Prime p)
(hpmem : ↑p ∈ IsLocalRing.maximalIdeal O)
(f : O →+* K)
(hfp : f ↑p ≠ 0)
(i : ι)
:
MvPowerSeries ι O
The p-scaled logarithm of a formal group law, as a power series over O: the
integral form of Λ(pU), so that y ↦ evalT y (scaledLog i) represents Λ(p·y).
Instances For
theorem
ChabautyColeman.FormalGroupLaw.coeff_scaledLog_map
{O : Type u_4}
[CommRing O]
[IsLocalRing O]
[UniformSpace O]
[Fact (IsAdic (IsLocalRing.maximalIdeal O))]
{ι : Type u_5}
[Fintype ι]
[DecidableEq ι]
{K : Type u_6}
[Field K]
{f : O →+* K}
{p : ℕ}
(Φ : FormalGroupLaw O ι)
(hp : Nat.Prime p)
(hpmem : ↑p ∈ IsLocalRing.maximalIdeal O)
(hfp : f ↑p ≠ 0)
(i : ι)
(d : ι →₀ ℕ)
:
f ((MvPowerSeries.coeff d) (Φ.scaledLog hp hpmem f hfp i)) = f ↑p ^ Finsupp.degree d * (MvPowerSeries.coeff d) ((map f Φ).log i)
theorem
ChabautyColeman.FormalGroupLaw.decay_scaledLog
{O : Type u_4}
[CommRing O]
[IsLocalRing O]
[UniformSpace O]
[Fact (IsAdic (IsLocalRing.maximalIdeal O))]
{ι : Type u_5}
[Fintype ι]
[DecidableEq ι]
{K : Type u_6}
[Field K]
{f : O →+* K}
{p : ℕ}
(Φ : FormalGroupLaw O ι)
(hp : Nat.Prime p)
(hpmem : ↑p ∈ IsLocalRing.maximalIdeal O)
(hfp : f ↑p ≠ 0)
(i : ι)
:
Filter.Tendsto (fun (d : ι →₀ ℕ) => (MvPowerSeries.coeff d) (Φ.scaledLog hp hpmem f hfp i)) Filter.cofinite (nhds 0)
theorem
ChabautyColeman.FormalGroupLaw.evalT_scaledLog_injective
{O : Type u_4}
[CommRing O]
[IsDomain O]
[IsLocalRing O]
[UniformSpace O]
[Fact (IsAdic (IsLocalRing.maximalIdeal O))]
[IsUniformAddGroup O]
[CompleteSpace O]
[T2Space O]
[IsTopologicalRing O]
{ι : Type u_5}
[Fintype ι]
[DecidableEq ι]
{K : Type u_6}
[Field K]
[CharZero K]
{f : O →+* K}
{p : ℕ}
(Φ : FormalGroupLaw O ι)
(hp : Nat.Prime p)
(hp2 : p ≠ 2)
(hpm : IsLocalRing.maximalIdeal O = Ideal.span {↑p})
(hf : Function.Injective ⇑f)
(hpmem : ↑p ∈ IsLocalRing.maximalIdeal O)
(hfp : f ↑p ≠ 0)
:
Function.Injective fun (y : ι → O) (i : ι) => MvPSeries.evalT y (Φ.scaledLog hp hpmem f hfp i)
Injectivity of the formal logarithm, for the canonical scaled log.
theorem
ChabautyColeman.FormalGroupLaw.evalT_scaledLog_add
{O : Type u_4}
[CommRing O]
[IsLocalRing O]
[UniformSpace O]
[Fact (IsAdic (IsLocalRing.maximalIdeal O))]
[IsUniformAddGroup O]
[CompleteSpace O]
[T2Space O]
[IsTopologicalRing O]
{ι : Type u_5}
[Fintype ι]
[DecidableEq ι]
{K : Type u_6}
[Field K]
[CharZero K]
{f : O →+* K}
{p : ℕ}
(Φ : FormalGroupLaw O ι)
(hp : Nat.Prime p)
(hpm : IsLocalRing.maximalIdeal O = Ideal.span {↑p})
(hf : Function.Injective ⇑f)
(hpmem : ↑p ∈ IsLocalRing.maximalIdeal O)
(hfp : f ↑p ≠ 0)
(y z : ι → O)
(i : ι)
:
MvPSeries.evalT (fun (j : ι) => MvPSeries.evalT (Sum.elim y z) (Φ.scaledF p j)) (Φ.scaledLog hp hpmem f hfp i) = MvPSeries.evalT y (Φ.scaledLog hp hpmem f hfp i) + MvPSeries.evalT z (Φ.scaledLog hp hpmem f hfp i)
Additivity of the formal logarithm, for the canonical scaled log.
Evaluation of the scaled group law at scaled points #
theorem
ChabautyColeman.FormalGroupLaw.natCast_mul_evalT_scaledF
{O : Type u_4}
[CommRing O]
[IsLocalRing O]
[UniformSpace O]
[Fact (IsAdic (IsLocalRing.maximalIdeal O))]
[IsUniformAddGroup O]
[CompleteSpace O]
[T2Space O]
[IsTopologicalRing O]
{ι : Type u_5}
(Φ : FormalGroupLaw O ι)
[Finite ι]
{p : ℕ}
(hpm : IsLocalRing.maximalIdeal O = Ideal.span {↑p})
(y : ι ⊕ ι → O)
(j : ι)
:
Evaluating the p-scaled group law and rescaling recovers the group law at the
p-scaled point: p · (F(py, pz)/p) = F(py, pz) at the level of evalT.