The scaled formal logarithm of a formal group law

Source: MichaelStollBayreuth/EllipticCurves at commit 3f8c39c0fc4c0fd0a40e693aa2a9bbda08d9ee1f.

This file generalizes the p-scaling machinery of the vendored kit file EllipticCurves.Mathlib.Chabauty.LogIso from the natural number p to an arbitrary ring element c (for the application: a power π^e of a uniformizer of 𝒪_v, where e is the absolute ramification index). The c-scaled formal group law ChabautyColeman.FormalGroupLaw.scaledFC is F(cX, cY)/c; the additivity identity of the formal logarithm descends along an injective base-change map f : O →+* K to the c-scaled integral logarithm (ChabautyColeman.FormalGroupLaw.subst_scaledFC_descent).

The second part specializes to the valuation ring 𝒪_v of the completion of a global field at a finite place: for c = π^e the scaled logarithm has integral coefficients (WeierstrassCurve is not needed here; this works for any formal group law over 𝒪_v), with linear coefficient 1, so it has an integral compositional inverse (ChabautyColeman.invSubst), and evaluation at points of the maximal ideal produces a group isomorphism onto (𝔪, +).

instance IsDedekindDomain.HeightOneSpectrum.factIsAdic_adicCompletionIntegers {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : Fact (IsAdic (IsLocalRing.maximalIdeal ↥(adicCompletionIntegers K v)))

The topology on 𝒪_v is the 𝔪-adic topology; this activates the vendored kit.

theorem ChabautyColeman.map_eq_rescale_of_forall_coeff {O : Type u_1} [CommRing O] {ι : Type u_2} {K : Type u_3} [CommRing K] {f : O →+* K} {c : O} {H : MvPowerSeries ι O} {L : MvPowerSeries ι K} (hH : ∀ (d : ι →₀ ℕ), f ((MvPowerSeries.coeff d) H) = f c ^ Finsupp.degree d * (MvPowerSeries.coeff d) L) : (MvPowerSeries.map f) H = (MvPowerSeries.rescale fun (x : ι) => f c) L

General-scale version of ChabautyColeman.map_eq_rescale: scaling by an arbitrary ring element c instead of a natural number p.

The c-scaled formal group law

noncomputable def ChabautyColeman.FormalGroupLaw.scaledFC {O : Type u_1} [CommRing O] {ι : Type u_2} (Φ : FormalGroupLaw O ι) (c : O) (j : ι) : MvPowerSeries (ι ⊕ ι) O

The c-scaled formal group law: F(cX, cY)/c, integral because F has no constant term.

Equations

• Φ.scaledFC c j d = c ^ (Finsupp.degree d - 1) * (MvPowerSeries.coeff d) (Φ.F j)

@[simp]

theorem ChabautyColeman.FormalGroupLaw.coeff_scaledFC {O : Type u_1} [CommRing O] {ι : Type u_2} (Φ : FormalGroupLaw O ι) (c : O) (j : ι) (d : ι ⊕ ι →₀ ℕ) : (MvPowerSeries.coeff d) (Φ.scaledFC c j) = c ^ (Finsupp.degree d - 1) * (MvPowerSeries.coeff d) (Φ.F j)

theorem ChabautyColeman.FormalGroupLaw.constantCoeff_scaledFC {O : Type u_1} [CommRing O] {ι : Type u_2} (Φ : FormalGroupLaw O ι) (c : O) (j : ι) : MvPowerSeries.constantCoeff (Φ.scaledFC c j) = 0

theorem ChabautyColeman.FormalGroupLaw.hasSubst_scaledFC {O : Type u_1} [CommRing O] {ι : Type u_2} (Φ : FormalGroupLaw O ι) (c : O) [Finite ι] : MvPowerSeries.HasSubst (Φ.scaledFC c)

Descent of the logarithm additivity to the c-scaled level

theorem ChabautyColeman.FormalGroupLaw.map_scaledFC_smul {O : Type u_1} [CommRing O] {ι : Type u_2} [Finite ι] {K : Type u_3} [Field K] {f : O →+* K} {c : O} (Φ : FormalGroupLaw O ι) (j : ι) : f c • (MvPowerSeries.map f) (Φ.scaledFC c j) = (MvPowerSeries.rescale fun (x : ι ⊕ ι) => f c) ((map f Φ).F j)

The c-scaled formal group law is the c-rescaling of F, over the fraction field.

theorem ChabautyColeman.FormalGroupLaw.subst_scaledFC_descent {O : Type u_1} [CommRing O] {ι : Type u_2} [Finite ι] {K : Type u_3} [Field K] {f : O →+* K} {c : O} (Φ : FormalGroupLaw O ι) [Fintype ι] [DecidableEq ι] [CharZero K] (hf : Function.Injective ⇑f) {HL : ι → MvPowerSeries ι O} (hHL : ∀ (j : ι), (MvPowerSeries.map f) (HL j) = (MvPowerSeries.rescale fun (x : ι) => f c) ((map f Φ).log j)) (i : ι) : MvPowerSeries.subst (Φ.scaledFC c) (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 c-scaled logarithm is additive for the c-scaled formal group law, over O.

The multiplication-by-m series

noncomputable def ChabautyColeman.FormalGroupLaw.mulSeries {O : Type u_1} [CommRing O] (Φ : FormalGroupLaw O Unit) : ℕ → MvPowerSeries Unit O

The multiplication-by-m series of a one-parameter formal group law: ψ_0 = 0 and ψ_{m+1} = F(X, ψ_m).

Equations

• Φ.mulSeries 0 = 0
• Φ.mulSeries m.succ = MvPowerSeries.subst (Sum.elim (fun (x : Unit) => MvPowerSeries.X ()) fun (x : Unit) => Φ.mulSeries m) (Φ.F ())

theorem ChabautyColeman.FormalGroupLaw.mulSeries_zero {O : Type u_1} [CommRing O] (Φ : FormalGroupLaw O Unit) : Φ.mulSeries 0 = 0

theorem ChabautyColeman.FormalGroupLaw.mulSeries_succ {O : Type u_1} [CommRing O] (Φ : FormalGroupLaw O Unit) (m : ℕ) : Φ.mulSeries (m + 1) = MvPowerSeries.subst (Sum.elim (fun (x : Unit) => MvPowerSeries.X ()) fun (x : Unit) => Φ.mulSeries m) (Φ.F ())

theorem ChabautyColeman.FormalGroupLaw.constantCoeff_mulSeries {O : Type u_1} [CommRing O] (Φ : FormalGroupLaw O Unit) (m : ℕ) : MvPowerSeries.constantCoeff (Φ.mulSeries m) = 0

theorem ChabautyColeman.FormalGroupLaw.hasSubst_mulSeries_pair {O : Type u_1} [CommRing O] (Φ : FormalGroupLaw O Unit) (m : ℕ) : MvPowerSeries.HasSubst (Sum.elim (fun (x : Unit) => MvPowerSeries.X ()) fun (x : Unit) => Φ.mulSeries m)

theorem ChabautyColeman.FormalGroupLaw.hasSubst_mulSeries {O : Type u_1} [CommRing O] (Φ : FormalGroupLaw O Unit) (m : ℕ) : MvPowerSeries.HasSubst fun (x : Unit) => Φ.mulSeries m

theorem ChabautyColeman.FormalGroupLaw.map_mulSeries {O : Type u_1} [CommRing O] (Φ : FormalGroupLaw O Unit) {O' : Type u_2} [CommRing O'] (f : O →+* O') (m : ℕ) : (MvPowerSeries.map f) (Φ.mulSeries m) = (map f Φ).mulSeries m

The logarithm of the multiplication series and its derivative

theorem ChabautyColeman.FormalGroupLaw.subst_mulSeries_log {K : Type u_1} [Field K] [CharZero K] (Φ : FormalGroupLaw K Unit) (m : ℕ) : MvPowerSeries.subst (fun (x : Unit) => Φ.mulSeries m) (Φ.log ()) = m • Φ.log ()

The formal logarithm turns the multiplication-by-m series into m • log.

theorem ChabautyColeman.FormalGroupLaw.subst_mulSeries_diffInv_mul_pderiv {K : Type u_1} [Field K] [CharZero K] (Φ : FormalGroupLaw K Unit) (m : ℕ) : MvPowerSeries.subst (fun (x : Unit) => Φ.mulSeries m) (Φ.diffMatrix⁻¹ () ()) * (MvPowerSeries.pderiv ()) (Φ.mulSeries m) = m • Φ.diffMatrix⁻¹ () ()

Differentiating the logarithm identity: (M⁻¹ ∘ ψ_m) · ψ_m′ = m • M⁻¹.

The scaled integral logarithm over the valuation ring of a completion

theorem ChabautyColeman.exists_valued_eq_exp_neg {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} {x : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)} (hx : x ∈ IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (hx0 : x ≠ 0) : ∃ (e : ℕ), 1 ≤ e ∧ Valued.v ↑x = WithZero.exp (-↑e)

The valuation of a nonzero element of the maximal ideal is exp (-e) for some e ≥ 1.

theorem ChabautyColeman.exists_scaledLog {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} [Finite (R ⧸ v.asIdeal)] [CharZero K] (Φ : FormalGroupLaw (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) Unit) : ∃ (n : ℕ) (π : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (lhat : MvPowerSeries Unit ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (ehat : MvPowerSeries Unit ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)), 1 ≤ n ∧ π ≠ 0 ∧ IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v) = Ideal.span {π} ∧ MvPowerSeries.constantCoeff lhat = 0 ∧ MvPowerSeries.constantCoeff ehat = 0 ∧ MvPowerSeries.subst (fun (x : Unit) => ehat) lhat = MvPowerSeries.X () ∧ MvPowerSeries.subst (fun (x : Unit) => lhat) ehat = MvPowerSeries.X () ∧ MvPowerSeries.subst (Φ.scaledFC (π ^ n)) lhat = MvPowerSeries.subst (fun (s : Unit) => MvPowerSeries.X (Sum.inl s)) lhat + MvPowerSeries.subst (fun (s : Unit) => MvPowerSeries.X (Sum.inr s)) lhat

The scaled-logarithm package over 𝒪_v: a level n ≥ 1, a uniformizer π, and a pair of integral power series lhat, ehat — the divided π^n-scaled logarithm and its compositional inverse — with the composition identities and the additivity of lhat for the π^n-scaled formal group law.

The evaluated scaled logarithm on the maximal ideal

theorem ChabautyColeman.eval_unit_mem {O : Type u_1} [CommRing O] [IsLocalRing O] [UniformSpace O] [Fact (IsAdic (IsLocalRing.maximalIdeal O))] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] {t : O} (ht : t ∈ IsLocalRing.maximalIdeal O) {h : MvPowerSeries Unit O} (hcc : MvPowerSeries.constantCoeff h = 0) : MvPSeries.eval (fun (x : Unit) => t) h ∈ IsLocalRing.maximalIdeal O

Evaluation of a one-variable series without constant term maps 𝔪 to 𝔪.

theorem ChabautyColeman.eval_eval_of_subst_eq_X {O : Type u_1} [CommRing O] [IsLocalRing O] [UniformSpace O] [Fact (IsAdic (IsLocalRing.maximalIdeal O))] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] {t : O} (ht : t ∈ IsLocalRing.maximalIdeal O) {g h : MvPowerSeries Unit O} (hg0 : MvPowerSeries.constantCoeff g = 0) (hcomp : MvPowerSeries.subst (fun (x : Unit) => g) h = MvPowerSeries.X ()) : MvPSeries.eval (fun (x : Unit) => MvPSeries.eval (fun (x : Unit) => t) g) h = t

Evaluating a composition identity h ∘ g = X: the evaluations of g and h are mutually inverse on 𝔪.

theorem ChabautyColeman.eval_scaledFC_add {O : Type u_1} [CommRing O] [IsLocalRing O] [UniformSpace O] [Fact (IsAdic (IsLocalRing.maximalIdeal O))] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] (Φ : FormalGroupLaw O Unit) {c : O} {lhat : MvPowerSeries Unit O} (hadd : MvPowerSeries.subst (Φ.scaledFC c) lhat = MvPowerSeries.subst (fun (s : Unit) => MvPowerSeries.X (Sum.inl s)) lhat + MvPowerSeries.subst (fun (s : Unit) => MvPowerSeries.X (Sum.inr s)) lhat) {s₁ s₂ : O} (h₁ : s₁ ∈ IsLocalRing.maximalIdeal O) (h₂ : s₂ ∈ IsLocalRing.maximalIdeal O) : MvPSeries.eval (fun (x : Unit) => MvPSeries.eval (Sum.elim (fun (x : Unit) => s₁) fun (x : Unit) => s₂) (Φ.scaledFC c ())) lhat = MvPSeries.eval (fun (x : Unit) => s₁) lhat + MvPSeries.eval (fun (x : Unit) => s₂) lhat

Additivity of the evaluated scaled logarithm: evaluating the descended identity at a pair of points of 𝔪.

theorem ChabautyColeman.eval_F_eq_mul_eval_scaledFC {O : Type u_1} [CommRing O] [IsLocalRing O] [UniformSpace O] [Fact (IsAdic (IsLocalRing.maximalIdeal O))] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] (Φ : FormalGroupLaw O Unit) (c : O) {s₁ s₂ : O} (h₁ : s₁ ∈ IsLocalRing.maximalIdeal O) (h₂ : s₂ ∈ IsLocalRing.maximalIdeal O) : MvPSeries.eval (Sum.elim (fun (x : Unit) => c * s₁) fun (x : Unit) => c * s₂) (Φ.F ()) = c * MvPSeries.eval (Sum.elim (fun (x : Unit) => s₁) fun (x : Unit) => s₂) (Φ.scaledFC c ())

Compatibility of the scaled formal group sum with the original one: evaluating F at (c·s₁, c·s₂) is c times the evaluated scaled sum.

Divisibility of the multiplication-by-p coefficients over 𝒪_v

theorem ChabautyColeman.coeff_single_mulSeries {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} (Φ : FormalGroupLaw (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) Unit) [CharZero K] (m : ℕ) : (MvPowerSeries.coeff fun₀ | () => 1) (Φ.mulSeries m) = ↑m

The linear coefficient of the multiplication-by-m series is m.

theorem ChabautyColeman.coeff_mulSeries_mem_span {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} (Φ : FormalGroupLaw (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) Unit) [CharZero K] {p : ℕ} (hp : Nat.Prime p) (hpmem : ↑p ∈ IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) {d : Unit →₀ ℕ} (hd : ¬p ∣ d ()) : (MvPowerSeries.coeff d) (Φ.mulSeries p) ∈ Ideal.span {↑p}

The coefficients of ψ_p in degrees not divisible by p are divisible by p.