feat(NumberTheory/ModularForms): E₄ and E₆ generate the graded ring of level-1 modular forms#38813
Draft
CBirkbeck wants to merge 44 commits intoleanprover-community:masterfrom
Draft
feat(NumberTheory/ModularForms): E₄ and E₆ generate the graded ring of level-1 modular forms#38813CBirkbeck wants to merge 44 commits intoleanprover-community:masterfrom
CBirkbeck wants to merge 44 commits intoleanprover-community:masterfrom
Conversation
…e dimension formula Adds `CuspFormSubmodule.lean` providing the cusp form submodule of modular forms together with API, and `DimensionFormulas/LevelOne.lean` proving the classical dimension formula for spaces of level one modular forms. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Targeted fixes from PR leanprover-community#37789 review: - `cuspFormSubmodule` and `equivCuspFormSubmodule`: make `Γ`/`k` explicit - `isCuspForm_iff`: shorter proof - `ofMulDiscriminant`: simplify cusp-form coeff zero argument - `divDiscriminant.holo'`: golf by inlining the differentiability subgoals - `rank_eq_one_add_rank_cuspForm`: take `hk : 3 ≤ k` over `ℕ` - `discriminant_eq_E4_cube_sub_E6_sq`: restate as `Δ = (E₄³ - E₆²)/1728`, drop inline proof comments, fold redundant `have`s - `exists_smul_eq_of_rank_one`: use `finrank_eq_one_iff_of_nonzero'` from mathlib - Move `one_mem_strictPeriods_SL` to `LevelOne.lean` so the haveI workaround in `EisensteinSeries.E_qExpansion_coeff` can be dropped Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…ula proofs - `discriminant_eq_E4_cube_sub_E6_sq`: hoist `hmcast` (used 3x) above its use, drop redundant calc step `_ = (CuspForm.toModularFormₗ g) z := rfl` - `weight_two_eq_zero_of_not_cuspForm`: drop `hc0`, fold the c4/c6 substitutions directly into `heq4`/`heq6` rather than via separate `hc4_eq`/`hc6_eq` + `rw`, replace the by_contra finale with `pow_eq_zero_iff`/`mul_eq_zero` Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Add public `noncomputable abbrev`s `ModularForm.E₄ : ModularForm 𝒮ℒ 4` and `ModularForm.E₆ : ModularForm 𝒮ℒ 6` for the normalised level 1 Eisenstein series of weights 4 and 6. Use them throughout `DimensionFormulas/LevelOne.lean` to drop the awkward `E (show 3 ≤ 4 by norm_num)` and `set E4 := …` patterns. The `abbrev` (rather than `def` or notation) is required so all uses share a single underlying proof of `3 ≤ 4` / `3 ≤ 6`, which lets simp lemmas about their q-expansions match consistently. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…oor_sub_div` Adds the lemma `⌊k / a⌋₊ = 1 + ⌊(k - a) / a⌋₊` for `0 < a ≤ k` over a linear ordered field, generalising the local `floor_lem1` helper that was buried in `DimensionFormulas/LevelOne.lean`. Inline the helper at its single use site in `dimension_level_one`. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…lpers up to DedekindEta
Adds three q-coordinate lemmas to `DedekindEta.lean`:
- `multipliable_one_sub_pow {q : ℂ} (hq : ‖q‖ < 1)`: pointwise multipliability
- `multipliableLocallyUniformlyOn_one_sub_pow`: local uniform convergence on the
open unit disc
- `differentiableOn_tprod_one_sub_pow_pow (k : ℕ)`: differentiability of the
k-th power of the product on the open unit disc
These cover the case `q = 0` (the cusp at infinity), which the existing eta-side
lemmas (`multipliableLocallyUniformlyOn_eta` etc., stated on `ℍₒ`) cannot.
In `Discriminant.lean`, deletes the three private helpers
`multipliable_one_sub_pow`, `tendstoLocallyUniformlyOn_eta_prod`,
`differentiableWithinAt_eta_prod_pow`, and rewrites `discriminant_cuspFunction_eqOn`
and `discriminant_qExpansion_coeff_one` to work on the full open unit disc
`Metric.ball 0 1` (instead of the arbitrary `Metric.ball 0 (1/2)`) and to call
the new helpers from `DedekindEta.lean`.
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…-coord base Rather than having parallel q-coord and z-coord proofs of the same convergence facts about the eta product, derive the z-coord versions from the q-coord ones by composing with `Periodic.qParam 1 : ℍₒ → Metric.ball 0 1`. - `multipliableLocallyUniformlyOn_eta` is now derived from `multipliableLocallyUniformlyOn_one_sub_pow` via `TendstoLocallyUniformlyOn.comp`, shrinking the proof from ~14 lines to ~7. - `differentiableAt_eta_tprod` now derives from `differentiableOn_tprod_one_sub_pow` by chain rule (instead of going through the eta-side multipliable lemma). - `summable_eta_q` switched to `norm_qParam_lt_one` (which the q-coord material already uses) for consistency. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…lyOn_eta` `hasProdLocallyUniformlyOn_iff_tendstoLocallyUniformlyOn` is `Iff.rfl`, so the two `rw` calls in the previous proof are unnecessary — a type ascription on the underlying `HasProdLocallyUniformlyOn` is enough to invoke `TendstoLocallyUniformlyOn.comp` via dot notation. Collapse the proof to a 6-line term-mode expression. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Extracts helper lemmas to shorten the two main proofs: - `tendsto_valueAtInfty`: a modular form whose `valueAtInfty` is `c` tends to `c` along `atImInfty`. Used in `E4_cube_sub_E6_sq_form_isCuspForm`. - `E4_cube_sub_E6_sq_form` (def): the explicit `ModularForm 𝒮ℒ 12` whose pointwise value is `E₄³ - E₆²`, with companion lemmas `_apply`, `_isCuspForm`, `_qExpansion_coeff_one`. The main theorem `discriminant_eq_E4_cube_sub_E6_sq` is now ~15 lines instead of ~70. - `coeffZero_eq_zero_of_pow_eq_smul`: the algebraic core of the weight-2 vanishing argument as a pure power-series fact (no modular forms). `weight_two_eq_zero_of_not_cuspForm` becomes a thin wrapper that transports the modular-form identities into the power-series form, shrinking from ~50 lines to ~25. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…ter decomposition - `discriminant_eq_E4_cube_sub_E6_sq`: move `hgΔ` back inside the local `hc_eq` block (it's only used there), inline `hgF`, and use `simpa` for the final step. - `E4_cube_sub_E6_sq_form_qExpansion_coeff_one`: minor simplification collapsing the chained `mcast`/`hmcast` rewrites. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Wraps several lines in the dimension-formula proofs to fit within mathlib's 100-character line length limit. No semantic changes. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…sion lemmas `E₄` and `E₆` are `noncomputable abbrev`s, so they reduce automatically and the explicit `show E₄ = E (...) from rfl` step in `E₄_qExpansion_coeff_one` and `E₆_qExpansion_coeff_one` was unnecessary. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Adds `CuspForm.toModularForm` and a `Coe (CuspForm Γ k) (ModularForm Γ k)` instance so cusp forms can be viewed as modular forms automatically. Refactors `CuspForm.toModularFormₗ` to delegate to this plain function and updates call sites. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…ubmodule Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Restores ModularForm.discriminant_eq_E4_cube_sub_E6_sq, ported from earlier work (commit 8d90310) and updated to current master's API: - discriminantCuspForm → CuspForm.discriminant - cuspForm_twelve_smul_discriminant → CuspForm.exists_smul_discriminant_of_weight_eq_twelve - qExpansion_sub/qExpansion_smul → ModularFormClass.qExpansion_sub/qExpansion_smul - The `IsCuspForm` proof uses an algebraic q-expansion split rather than the no-longer-available tendsto_valueAtInfty. Adds supporting lemmas in Discriminant.lean: - discriminant_cuspFunction_eqOn (private) - differentiableWithinAt_eta_prod_pow (private; shorter than original since differentiableOn_tprod_one_sub_pow_pow is now in mathlib) - discriminant_qExpansion_coeff_one Also drops merge-induced duplicates of master lemmas (summable_eta_q, multipliableLocallyUniformlyOn_eta, differentiableOn_tprod_one_sub_pow, differentiableOn_tprod_one_sub_pow_pow, one_mem_strictPeriods_SL) and removes two unused/duplicating helpers (floor_div_eq_one_add_floor_sub_div, which is too specific for a top-level file and unused, and ModularForm.ofSubgroupEq, which duplicates mcast).
Applies findings from /simplify code review: - Extract the duplicated `qExpansion_sub` rewrite chain into a shared `E₄CubeSubE₆SqForm_qExpansion_eq` helper. Both `_isCuspForm` and `_qExpansion_coeff_one` now reduce to a one-line `rw` of this helper (~16 lines saved). - `linear_combination (1 / 1728 : ℂ) * h1728` → `linear_combination h1728 / 1728`. - Rename `E4_cube_sub_E6_sq_form` → `E₄CubeSubE₆SqForm` (camelCase + subscripts per mathlib def naming convention) and `discriminant_eq_E4_cube_sub_E6_sq` → `discriminant_eq_E₄_cube_sub_E₆_sq`. - Use `ball 0 1` instead of `ball 0 (1/2)` in `discriminant_cuspFunction_eqOn` and `discriminant_qExpansion_coeff_one` (the actual constraint is `‖q‖ < 1`), which lets `differentiableOn_tprod_one_sub_pow_pow` apply directly and removes the now-unnecessary `differentiableWithinAt_eta_prod_pow` helper.
Drops `(... : ℍ → ℂ)` type ascriptions where the surrounding term already forces the coercion (`qExpansion 1 E₄`, `cuspFunction 1 Δ`, `qExpansion 1 E₄CubeSubE₆SqForm`, etc.). Also reflows the affected declarations to fit the 100-character line limit.
…²) / 1728
Adds `ModularForm.discriminant_eq_E₄_cube_sub_E₆_sq_graded`, the analogue of
`discriminant_eq_E₄_cube_sub_E₆_sq` in the graded ring `⨁ k, ModularForm 𝒮ℒ k`:
DirectSum.of (ModularForm 𝒮ℒ) 12 (CuspForm.discriminant : ModularForm 𝒮ℒ 12) =
(1 / 1728 : ℂ) • (DirectSum.of (ModularForm 𝒮ℒ) 4 E₄ ^ 3 -
DirectSum.of (ModularForm 𝒮ℒ) 6 E₆ ^ 2)
The proof reduces to the pointwise identity via `DirectSum.of_mul_of`, `congr 1`,
and `ext`, then closes by `discriminant_eq_E₄_cube_sub_E₆_sq` and `ring`.
In `discriminant_eq_E₄_cube_sub_E₆_sq_graded`, replace `(by norm_num)` proofs of `4 + 4 + 4 = 12` and `6 + 6 = 12` with `(by decide)` (kernel reduction).
Adds `@[simp]` lemmas `ModularForm.mcast_apply` and `CuspForm.mcast_apply` saying `mcast h f hΓ z = f z` (true by `rfl`). These let `simp` automatically unfold `mcast` in pointwise reasoning, and are useful API for any future proofs that mix `ModularForm.mcast`/`CuspForm.mcast` with `simp`-based function-level rewriting.
The simp lemmas were unused — `change` in `discriminant_eq_E₄_cube_sub_E₆_sq_graded` goes through defeq directly, and the `simp only`-based alternatives I tried didn't close the goal. Removing per "no unused API" guideline; can be re-added later when there's a proof that benefits. This reverts commit 8de2aff.
…adedRing.lean Splits the `Δ = (E₄³ - E₆²) / 1728` results out of `DimensionFormulas/LevelOne.lean` into a new file `DimensionFormulas/GradedRing.lean`. This new file is intended to collect structural results about the graded ring `⨁ k, ModularForm 𝒮ℒ k` of level-1 modular forms (e.g. that `E₄, E₆` generate the full graded ring, to come). Moved declarations: - `E₄CubeSubE₆SqForm` (private) - `E₄CubeSubE₆SqForm_apply` (private) - `E₄CubeSubE₆SqForm_qExpansion_eq` (private) - `E₄CubeSubE₆SqForm_isCuspForm` (private) - `E₄CubeSubE₆SqForm_qExpansion_coeff_one` (private) - `discriminant_eq_E₄_cube_sub_E₆_sq` - `discriminant_eq_E₄_cube_sub_E₆_sq_graded`
…s/ root Move `DimensionFormulas/GradedRing.lean` → `GradedRing.lean`. The graded-ring results aren't specifically about dimension formulas, so they belong at the top of the `ModularForms/` directory.
…ed ring Adds the evaluation homomorphism `evalE₄E₆ : ℂ[X₀, X₁] →ₐ[ℂ] ⨁ k, ModularForm 𝒮ℒ k` and signposts the surjectivity / injectivity results (currently `sorry`) used to conclude that `E₄, E₆` generate the graded ring of level-1 modular forms. The proofs will be ported from <https://github.com/CBirkbeck/LeanModularForms> (Modularforms/Generators/) in follow-up commits. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
PR summary 177caf0bccImport changes for modified filesNo significant changes to the import graph Import changes for all files
|
github-actions
Bot
added
the
t-number-theory
…urjectivity scaffolding) Brings over the bulk of the surjectivity argument from LeanModularForms/Modularforms/Generators/. The remaining `sorry`s are scoped to: * `monomial_qExpansion_coeff_zero_eq_one`: q-expansion 0th coefficient of a homogeneous monomial in `(of _ 4 E₄, of _ 6 E₆)`. * the cusp-form predicate inside `surj_at_weight_inductive` (linearity step). * `evalE₄E₆_injective` (still entirely TODO). The strong-induction surjectivity proof, base cases, and weight-rank lemmas for weights 8/10 are now complete. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
… surjectivity Closes the `cuspForm_eq_discriminant_mul` helper and the inductive cusp-form decomposition step inside `surj_at_weight_inductive`. Remaining `sorry`s: * `monomial_qExpansion_coeff_zero_eq_one`: q-expansion identity for homogeneous monomials in `(of _ 4 E₄, of _ 6 E₆)`. * `evalE₄E₆_injective`: injectivity of the evaluation homomorphism (TODO). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…o_eq_one` Uses the `qExpansionRingHom` ring homomorphism plus the fact that the monomial `(of _ 4 E₄)^a * (of _ 6 E₆)^b` is concentrated at weight `n = 4a + 6b`. Surjectivity is now fully proved. Only `evalE₄E₆_injective` (the algebraic independence of E₄ and E₆) remains as `sorry`. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Adds the full structural framework for `evalE₄E₆_injective`: - `discriminantPoly = (1/1728)(X₀³ - X₁²)` - weight helpers `weight_eq_4a_6b`, `weight_fin2_cast`, `no_wt_monomial_of_*` - per-weight machinery: `whomog_unique_monomial`, `evalE₄E₆_*_grade` - weighted-homogeneous-component evaluation helpers - structural induction over the weight in `per_weight_injective` - main theorem `evalE₄E₆_injective` derived from per-weight injectivity 4 `sorry`s remain (component decomposition, Δ-mul cusp form, weight-0 base case, and the Δ-poly inductive step), to be filled in subsequent commits. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
… case Remaining `sorry`s: * `evalE₄E₆_discriminantPoly_mul_coeff_zero` (Δ_poly * s gives a cusp form at weight n) * `per_weight_injective_inductive_step` (the Δ_poly divisibility induction) Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…_imp + helper Close `evalE₄E₆_discriminantPoly_mul_coeff_zero` (uses the discriminant identity and the cusp form property of Δ) and `eval_discriminantPoly_mul_zero_imp` (uses that `Δ z ≠ 0`). Remaining `sorry`s: * `whomog_poly_Delta_decomp` (induction on `∑ d ∈ p.support, d 0`) * `reduced_part_eq_zero` (q-expansion-coeff-0 argument) Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Uses the q-expansion-coeff-0 argument: take qExpansion of the identity `r + Δ_poly * s` evaluated at weight n, the Δ_poly term contributes 0, the r term equals its leading scalar `c`, hence `c = 0`. Last remaining `sorry`: `whomog_poly_Delta_decomp`, the polynomial decomposition by induction on the support sum of `d 0` exponents. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Final piece of the injectivity proof. The polynomial decomposition is by strong induction on `∑ d ∈ p.support, d 0`: each step uses the identity `X₀³ = X₁² + 1728 • Δ_poly` to replace a monomial with `d 0 ≥ 3` by a combination with strictly smaller support sum. The full result is now established: - `evalE₄E₆_surjective`: `evalE₄E₆` is surjective. - `evalE₄E₆_injective`: E₄ and E₆ are algebraically independent. - `modularFormsEquivMvPolynomial`: `ℂ[X₀, X₁] ≃ₐ[ℂ] ⨁ k, ModularForm 𝒮ℒ k`. - `E₄E₆_generate`: E₄, E₆ generate the graded ring. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* Replace deprecated `push_neg` with `push Not` (4 sites). * Replace `show` with `change` where the tactic actually changes the goal, silencing `linter.style.show`. * Remove unused private helpers `X0_cubed_eq_smul_discriminantPoly` and `X0_pow_mul_X1_pow_isWeightedHomogeneous'`. * Strip narrative inline `-- ...` comments from proof bodies; keep docstrings and section dividers. No semantic changes; the file builds with zero warnings. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Apply user-stated rule: each tactic on its own line (no `; ` chaining).
Combine the duplicate `weight_eight_rank_one` / `weight_ten_rank_one` into
a single parametric `rank_one_of_lt_twelve {k : ℕ} (hk3 : 3 ≤ k) (hk2 : Even k)
(hk12 : k < 12) : Module.rank ℂ (ModularForm 𝒮ℒ ↑k) = 1`.
* Split every `tac1; tac2` chain across two lines (~30 sites).
* Combine the two near-identical rank lemmas into one parametric helper.
* Move the `rcases hk_odd with ⟨r, hr⟩; omega` odd-case dismissals inside
`surj_of_weight` to two-line `obtain`/`omega` form.
No semantic changes; the file builds with zero warnings.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…ines) Apply mathlib-style golf to all new declarations from PR leanprover-community#38813. Highlights: * Reorganize so `discriminantPoly` and `evalE₄E₆_discriminantPoly` come before `discriminant_mem_range_evalE₄E₆`, collapsing the latter to a one-line term-mode proof. * Extract a `cast_modularForm_apply` helper used in `evalE₄E₆_discriminantPoly_mul_coeff_zero` and `eval_discriminantPoly_mul_zero_imp`. * Replace `obtain ⟨r, hr⟩ := hk_odd; omega` odd-case dismissals in `surj_of_weight` with `exact absurd hk_odd (by decide)`. * Inline single-use `have foo := bar` statements throughout. * Collapse three sequential `rw [show ... from by ring]` blocks in `discriminantPoly_piece_eq_monomial_sub` into one (~30 lines saved). * Use `simp [...]` in place of `rw [...]; simp` chains where applicable. * Apply `Finsupp.weight_apply` + `Finsupp.sum_fintype` in `weight_eq_4a_6b` (per code-reuse review). * Apply `Finsupp.prod_fintype` in `monomial_fin2_eq` (per code-reuse review). Hard constraints respected: * Each tactic on its own line; sequential `rw` calls combined into one. * No `tac1; tac2` chains introduced. * Build clean with zero warnings. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Establishes that
E₄andE₆generate the graded ring⨁ k, ModularForm 𝒮ℒ kof level-1 modular forms freely as aℂ-algebra.Status
Draft / WIP: the file currently contains scaffolding with two
sorrys that mark the surjectivity and injectivity proofs of the evaluation homomorphismevalE₄E₆ : ℂ[X₀, X₁] →ₐ[ℂ] ⨁ k, ModularForm 𝒮ℒ k. Both proofs will be ported in follow-up commits from https://github.com/CBirkbeck/LeanModularForms (Modularforms/Generators/).Main definitions
ModularForm.E₄E₆Weight: the weight functionFin 2 → ℕmapping0 ↦ 4,1 ↦ 6.ModularForm.evalE₄E₆: the evaluation homomorphismℂ[X₀, X₁] →ₐ[ℂ] ⨁ k, ModularForm 𝒮ℒ ksendingX₀ ↦ E₄,X₁ ↦ E₆.Main results
ModularForm.evalE₄E₆_surjective:evalE₄E₆is surjective.ModularForm.evalE₄E₆_injective:evalE₄E₆is injective (E₄ and E₆ are algebraically independent).ModularForm.modularFormsEquivMvPolynomial: the algebra isomorphismℂ[X₀, X₁] ≃ₐ[ℂ] ⨁ k, ModularForm 𝒮ℒ k.ModularForm.E₄E₆_generate:E₄, E₆generate the graded ring as aℂ-algebra.Dependencies
This PR depends on #38806 (
Δ = (E₄³ - E₆²) / 1728) for the discriminant identity in the graded ring.