feat(NumberTheory/ModularForms): E₄, E₆ surjectively map onto level-1 graded ring#39258
Draft
CBirkbeck wants to merge 67 commits into
Draft
feat(NumberTheory/ModularForms): E₄, E₆ surjectively map onto level-1 graded ring#39258CBirkbeck wants to merge 67 commits into
CBirkbeck wants to merge 67 commits into
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.
* 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>
Per the cleanup convention, docstrings should only appear on key public declarations. Remove docstrings from all private helpers introduced by this PR (and trim the multi-paragraph section divider at the start of the generators section to a single line). Public declarations that retain a one-sentence docstring: * `E₄E₆Weight`, `evalE₄E₆` * `evalE₄E₆_surjective`, `evalE₄E₆_injective` * `modularFormsEquivMvPolynomial`, `E₄E₆_generate` * (plus the discriminant identity theorems from PR leanprover-community#38806). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* Remove all section divider headers in the new content (per review). * Inline `finsupp_of_fin2` (it was a one-liner used once). * Replace `mul_modularForm_ne_zero_of_qExpansion_coeff_zero_eq_one` with the cleaner `mul_ne_zero` that takes `f ≠ 0` and `g ≠ 0` directly, using `qExpansion_eq_zero_iff` and the integral domain structure of `PowerSeries ℂ`. * Extract `sub_smul_qExpansion_coeff_zero_isCuspForm` and `directSumOf_evalE₄E₆_monomial_apply` as separate helpers, breaking down the `surj_at_weight_inductive` proof. * Drop the redundant explicit `d'` parameter from `discriminantPoly_piece_eq_monomial_sub` and rewrite the proof to use `monomial_fin2_eq` and `ring`, removing ~25 lines of manual algebra. Build clean. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Extract two helpers from the proof: * `reduced_isWeightedHomogeneous_eq_monomial`: a reduced (`d 0 < 3` for all support `d`) weighted-homogeneous polynomial of weight `n` equals the monomial at any of its support points. * `evalE₄E₆_monomial_qExpansion_coeff_zero`: the q-expansion-coeff-0 of `evalE₄E₆ (monomial d c)` evaluated at the matching weight equals `c`. `reduced_part_eq_zero` is now 36 lines instead of 62. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…p` and `surj_of_weight` * Extract `support_sum_lt_after_sub_δ_piece` from `whomog_poly_Delta_decomp` (the support-sum-decreases sub-proof, ~16 lines). * Extract `evalE₄E₆_X_sq` and `evalE₄E₆_X0_X1` simp-style API lemmas, used in the weight-8 and weight-10 base cases of `surj_of_weight`. `whomog_poly_Delta_decomp`: 67 → 52 lines. `surj_of_weight`: 51 → 45 lines. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…-length fixes * Rename `whomog_*` → `weightedHomogeneous_*` * Rename `mvpoly_*` → `mvPolynomial_*` * Rename `eval_discriminantPoly_mul_zero_imp` → `eval_discriminantPoly_mul_eq_zero_imp_eval_eq_zero` * Rename `unique_small_weight_soln` → `unique_small_weight_solution` * Rename `no_wt_monomial_*` → `no_weight_monomial_*` * Remove the `Δ = (E₄³ - E₆²) / 1728` section header * Reformat a few long signatures. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Reformat declaration signatures and proof terms that exceeded the 100-char
linter limit; reformat the `surj_of_weight` weight-{4,6,8,10} branches and
the `E₄E₆_generate` proof header.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…surj_of_weight` Replace `interval_cases n` (12 sub-goals, half of which only dismiss odd n) with a single `obtain rfl | rfl | rfl | rfl | rfl | rfl : n = 0 ∨ ... ∨ n = 10` so the proof has 6 branches instead of 12. `surj_of_weight`: 51 → 47 lines. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…uspForm_eq_discriminant_mul` * Reformat `mul_ne_zero`, `directSumOf_cast_eq`, `cast_modularForm_apply`, `discriminant_mem_range_evalE₄E₆`, `directSumOf_evalE₄E₆_monomial_apply`, and `evalE₄E₆_whc_grade` to fit within 100 chars. * Use `refine ... <| ... ?_` to merge the four `apply`/`refine` lines at the top of `cuspForm_eq_discriminant_mul` (28 → 24 lines). Down to 3 lines (all 103–105 chars) over the linter limit. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…Fin 2 → ℕ)` Drop the standalone `E₄E₆Weight` definition (a junk one-liner with no API) and inline it at each use site as `(![4, 6] : Fin 2 → ℕ)`. The type ascription is necessary: without it, `![4, 6]` elaborates to different `M`'s in `Finsupp.weight (w : σ → M)` depending on the surrounding context (`Fin 2 → ℕ` vs `Fin 2 → ℤ`), which breaks rewrites between sibling lemmas. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…nd tactic split * Split the surviving `;`-chained tactic in `cuspForm_eq_discriminant_mul` (`change ...; ring` → two-line bullet). * Reformat declaration signatures and proof bodies that exceeded the 100-char linter limit (mostly induced by the inlined `(![4, 6] : Fin 2 → ℕ)`). No remaining lines exceed 100 chars. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Make several helpers ready to be lifted to mathlib core in a separate PR: * `mul_ne_zero` → `modularForm_mul_ne_zero`: generalize from `𝒮ℒ` to any `Γ` with `[HasDetPlusMinusOne]` and any `(hh : 0 < h)` (`hΓ : h ∈ Γ.strictPeriods`). * `directSumOf_cast_eq` → `directSum_of_eq_cast`: generalize from `ModularForm 𝒮ℒ` to any indexed family `β : ι → Type*` of `AddCommMonoid`s. * `cast_modularForm_apply` → `modularForm_cast_apply`: generalize from `𝒮ℒ` to any `Γ`. * `weightedHomogeneous_eq_zero_of_no_monomials`, `weightedHomogeneous_unique_monomial`: generalize from `(![4, 6] : Fin 2 → ℕ)` to any weight function `w : σ → M` and any `CommSemiring R`. Plus another `surj_of_weight` golf: weight-0 case 4 → 3 lines. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* `monomial_fin2_eq`: generalize from `ℂ` to any `CommSemiring R`. * Extract `weight_fin2 : Finsupp.weight w d = d 0 * w 0 + d 1 * w 1` (general Fin-2 weight identity) and let `weight_eq_4a_6b` be a one-line specialization. These continue to prepare helpers for migration to mathlib core in the forthcoming Group-A / Group-B PR splits. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…s, proof tightening Naming (no abbreviations): - evalE₄E₆_whc_grade → evalE₄E₆_apply_eq_zero_of_ne - evalE₄E₆_whc_eq_single → evalE₄E₆_eq_of_apply - evalE₄E₆_mono_grade → evalE₄E₆_X_pow_mul_apply_eq_zero_of_ne - evalE₄E₆_monomial_grade → evalE₄E₆_monomial_apply_eq_zero_of_ne - directSumOf_evalE₄E₆_monomial_apply → directSum_of_E₄_pow_mul_E₆_pow_apply New general helpers (candidates for upstream PRs): - weightedHomogeneous_sub: sub of weighted-homogeneous polys - directSum_of_eq_sub_add_smul: of i f = of i (f - c•g) + c • of i g Proof simplifications: - monomial_qExpansion_coeff_zero_eq_one: factor through qExpansionRingHom_apply directly - discriminantPoly_isWeightedHomogeneous: use weightedHomogeneous_sub - evalE₄E₆_apply_eq_zero_of_ne / evalE₄E₆_component_eq: DirectSum.sum_apply, DirectSum.add_apply - discriminantPoly_piece_eq_monomial_sub: clean up inline show chains - per_weight_injective_zero: use weightedHomogeneous_unique_monomial - reduced_part_eq_zero: collapse two-step Q.map_add → coeff into one rewrite - surj_at_weight_inductive: use directSum_of_eq_sub_add_smul helper Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…y#38806 - Discriminant.lean: convert single `simp` for `discriminant_qExpansion_coeff_one` to a 3-step `calc` proof for robustness. - Basic.lean: add `ModularForm.pow` (with `coe_pow` simp lemma). - QExpansion.lean: add `ModularForm.qExpansion_pow`. - GradedRing.lean: use `pow` and `qExpansion_pow` in the `E₄³ - E₆²` def. - QExpansion.lean: move `cuspFunction_smul/neg/add/sub` and `qExpansion_smul/neg/add/sub` from `ModularFormClass` to `ModularForm` namespace, per the convention that lemmas about `Foo` go in the `Foo` namespace even when their input is class-generic. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…dedRing This was missed by the cherry-pick because the graded-ring branch has an extra usage in `sub_smul_qExpansion_coeff_zero_isCuspForm` that wasn't on the discriminant branch. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…aded ring Adds five lemmas extracted from the upcoming graded-ring PR (leanprover-community#38813), so that that PR can be reviewed in smaller pieces: * `DirectSum.of_eq_of_eq` (Algebra/DirectSum/Basic): cast indices in `of`. * `DirectSum.of_eq_sub_add_smul` (Algebra/DirectSum/Module): the identity `of i f = of i (f - c•g) + c • of i g`. * `ModularForm.cast_apply` (NumberTheory/ModularForms/Basic): a ModularForm cast through a weight equality has the same pointwise values. * `ModularForm.mul_ne_zero` (NumberTheory/ModularForms/QExpansion): the product of two non-zero modular forms is non-zero (via integral domain structure of `PowerSeries ℂ`). * `ModularForm.sub_smul_isCuspForm` (NumberTheory/ModularForms/CuspFormSubmodule): for level-1 forms `f, g` with `(qExpansion 1 g).coeff 0 = 1`, the form `f - (qExpansion 1 f).coeff 0 • g` is a cusp form. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…f_no_monomials, eq_monomial_of_unique_weight Adds three weighted-homogeneous API lemmas extracted from the upcoming graded-ring PR (leanprover-community#38813): * `IsWeightedHomogeneous.sub`: difference of weighted-homogeneous polynomials of degree `n` is weighted-homogeneous of degree `n` (mirrors `add`, requires `CommRing R`). * `IsWeightedHomogeneous.eq_zero_of_no_monomials`: a weighted-homogeneous polynomial of degree `n` is zero if no monomial has weight `n`. * `IsWeightedHomogeneous.eq_monomial_of_unique_weight`: a weighted-homogeneous polynomial of degree `n` whose support is concentrated at a single `d₀` equals `monomial d₀ (coeff d₀ φ)`. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Removes ~70 lines of local API helpers from GradedRing.lean now that they are added to the appropriate mathlib files via the two prerequisite PRs: * From `Mathlib/NumberTheory/ModularForms/Basic.lean`: `ModularForm.cast_apply`. * From `Mathlib/Algebra/DirectSum/Basic.lean`: `DirectSum.of_eq_of_eq`. * From `Mathlib/Algebra/DirectSum/Module.lean`: `DirectSum.of_eq_sub_add_smul`. * From `Mathlib/NumberTheory/ModularForms/QExpansion.lean`: `ModularForm.mul_ne_zero`. * From `Mathlib/NumberTheory/ModularForms/CuspFormSubmodule.lean`: `ModularForm.sub_smul_isCuspForm`. * From `Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean`: `IsWeightedHomogeneous.sub`, `eq_zero_of_no_monomials`, `eq_monomial_of_unique_weight`. Also fixes the proof of `DirectSum.of_eq_sub_add_smul` to avoid an instance ambiguity between `AddCommMonoid` and `AddCommGroup` from the section variables; the proof now uses an explicit `M` declaration. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…aded-ring # Conflicts: # Mathlib/NumberTheory/ModularForms/Basic.lean # Mathlib/NumberTheory/ModularForms/Discriminant.lean # Mathlib/NumberTheory/ModularForms/QExpansion.lean
2 tasks
PR summary 834e51690b
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.NumberTheory.ModularForms.QExpansion | 2776 | 2782 | +6 (+0.22%) |
Import changes for all files
| Files | Import difference |
|---|---|
6 filesMathlib.NumberTheory.ModularForms.Bounds Mathlib.NumberTheory.ModularForms.LevelOne.Basic Mathlib.NumberTheory.ModularForms.LevelOne Mathlib.NumberTheory.ModularForms.NormTrace Mathlib.NumberTheory.ModularForms.Petersson Mathlib.NumberTheory.ModularForms.QExpansion |
6 |
Mathlib.NumberTheory.ModularForms.GradedRing (new file) |
3109 |
Declarations diff
+ cast_apply
+ cuspForm_eq_discriminant_mul
+ directSum_of_E₄_pow_mul_E₆_pow_apply
+ discriminantPoly
+ discriminant_mem_range_evalE₄E₆
+ eq_monomial_of_unique_weight
+ eq_zero_of_no_monomials
+ evalE₄E₆
+ evalE₄E₆_C
+ evalE₄E₆_X0
+ evalE₄E₆_X0_X1
+ evalE₄E₆_X1
+ evalE₄E₆_X_sq
+ evalE₄E₆_discriminantPoly
+ evalE₄E₆_monomial
+ evalE₄E₆_surjective
+ exists_monomial_weight
+ monomial_qExpansion_coeff_zero_eq_one
+ mul_ne_zero
+ of_eq_of_eq
+ of_eq_sub_add_smul
+ one_ne_zero_modularForm
+ rank_one_of_lt_twelve
+ sub
+ sub_smul_isCuspForm
+ surj_at_small_weight
+ surj_at_weight_inductive
+ surj_of_rank_one
+ surj_of_weight
+ surj_of_zero_form
You can run this locally as follows
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>
## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.
No changes to strong technical debt.
No changes to weak technical debt.
mathlib-dependent-issues
Bot
added
the
blocked-by-other-PR
|
This PR/issue depends on:
|
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.
Defines the evaluation homomorphism
evalE₄E₆ : ℂ[X₀, X₁] →ₐ[ℂ] ⨁ k, ModularForm 𝒮ℒ ksendingX₀ ↦ E₄,X₁ ↦ E₆, and proves it is surjective: every level-1 modular form is a polynomial inE₄andE₆.First half of the original PR #38813 (the injectivity argument + final equivalence lands in #38813 after this merges).
Main results
ModularForm.evalE₄E₆: the evaluation homomorphism.ModularForm.evalE₄E₆_surjective.depends on: feat(NumberTheory/ModularForms): API lemmas for level-1 graded ring #38908
This PR was done with the help of Claude Code.