feat(CommensurableLimit): modular forms over a commensurability class as a direct limit - #5214
Open
CBirkbeck wants to merge 5 commits into
Open
feat(CommensurableLimit): modular forms over a commensurability class as a direct limit#5214CBirkbeck wants to merge 5 commits into
CBirkbeck wants to merge 5 commits into
Conversation
… as a direct limit Define `ModularFormCommensurable Γ₀ k` as the `Module.DirectLimit` of `ModularForm Γ k` over the determinant-one subgroups `Γ` commensurable with `Γ₀`, ordered by reverse inclusion (with restriction as transition maps). Headline `ModularFormArithmetic k` at `Γ₀ = 𝒮ℒ` (the image of SL₂(ℤ)). New folder `projects/LeanModularForms/LeanModularForms/CommensurableLimit/`: - CommensurabilityClass.lean: index poset `ModularForm.CommIndex Γ₀` (reverse-inclusion Preorder, Nonempty, IsDirected via ⊓-closure), plus `Subgroup.HasDetOne.of_le` and `Subgroup.commensurable_inf`. - DirectLimit.lean: `ModularForm.restrictSubgroupₗ` (ℂ-linear restriction), the space with its AddCommGroup/Module ℂ structure, `ofLevel` (+ restriction compat, injectivity), and the `lift` universal property. Sorry-free; #print axioms only propext/Classical.choice/Quot.sound. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…nvariants theorem Add `CommensuratorAction.lean`: - `PComm Γ₀ := commensurator Γ₀ ⊓ GL(2,ℝ)⁺` acts on `ModularFormCommensurable Γ₀ k` by the weight-k slash action (`translateₗ`, a ℂ-linear translate for positive determinant), bundled as `commRep : Representation ℂ (PComm Γ₀) (ModularFormCommensurable Γ₀ k)`. - `toFunₗ : limit →ₗ[ℂ] (ℍ → ℂ)`, the injective underlying-function map, with `toFunₗ (g • x) = toFunₗ x ∣[k] g⁻¹`. The action axioms are proved through this intertwiner (slash_one / slash_mul), sidestepping the index transport. - **Theorem `range_ofLevel_eq_invariants`**: for a level `Γ`, the image of `ModularForm Γ.carrier k` in the limit equals the `Γ.carrier`-invariants of the action. Corollary `ofLevelInvariantsEquiv`: `ModularForm Γ.carrier k ≃ₗ[ℂ]` those invariants. Supporting gap lemmas: `HasDetOne.conj`, `commensurable_conj`, `commensurable_le_commensurator`. Cusp-boundedness transfers across the class via mathlib's `Commensurable.isCusp_iff`. Sorry-free; #print axioms only propext/Classical.choice/Quot.sound. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Style + golf pass to mathlib standards across CommensurabilityClass.lean, DirectLimit.lean, CommensuratorAction.lean (no statement/signature changes, no new sorries, axioms unchanged): - `fun … =>` → `fun … ↦` throughout (project style) - golf: `commensurable_le_commensurator` via `conjAct_pointwise_smul_eq_self`; `HasDetOne.conj` → `simpa`; inlined single-use `have`s; term-mode tidy-ups - removed the staged `/-! ## Stage N` dividers; proper Main definitions/results module docstrings - removed a stale `set_option linter.unusedSimpArgs false in` (no longer fires) - line-packing + docstring tidy-ups Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…j` wrapper Per the /mathlibable NO-composable verdict: `Subgroup.commensurable_conj` was a 3-call composition of mathlib's `Commensurable.conj` + `commensurator_mem_iff` + `.trans`. Inline it at its sole call site (`CommIndex.conj`) and drop the wrapper. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
… ℝ general version Refactor the construction over a shared, predicate-parametrized index and add the general ℝ-scalar version, deducing the existing ℂ det-one version as the special case. - CommensurabilityClass.lean: `Subgroup.IsConjInfClosed P` (closure under ⊓ + conjugation) and the parametrized index `ModularForm.CommIndex Γ₀ P` (instances for P = ⊤ and the det-one predicate `DetOnePred`). `CommIndex.conj` is now generic in P. - DirectLimit.lean / CommensuratorAction.lean: the ℂ construction is now the det-one instance `CommIndex Γ₀ DetOnePred`; public API unchanged (`ModularFormCommensurable`, `commRep`, `range_ofLevel_eq_invariants`, …). - Real.lean (new): the genuinely-general version over the WHOLE commensurability class (`P = fun _ ↦ True`), with NO determinant conditions — `ModularFormCommensurableReal` as an ℝ-vector space, the FULL commensurator acting ℝ-linearly (`σ` fixes ℝ via `σ_ofReal`, so no positivity needed), `commRepℝ : Representation ℝ (commensurator Γ₀) _`, and `range_ofLevelℝ_eq_invariants`. The det-one ℂ version (positive-det commensurator, ℂ-linear) is the specialization that upgrades the scalars. Sorry-free; axioms only propext/Classical.choice/Quot.sound for both. Co-Authored-By: Claude Opus 4.8 (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
2 participants
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.
Summary
Defines the space of modular forms of weight
kand any level, as a direct limit over the commensurability class of a fixed groupΓ₀ ≤ GL₂(ℝ).the colimit of
ModularForm Γ kover all determinant-one subgroupsΓcommensurable withΓ₀, ordered by reverse inclusion with restriction as the transition maps. Headline instanceModularFormArithmetic k := ModularFormCommensurable 𝒮ℒ k— the commensurability class ofSL₂(ℤ)(mathlib'sSubgroup.IsArithmetic), the natural home of the Hecke/commensurator action.New folder
projects/LeanModularForms/LeanModularForms/CommensurableLimit/:CommensurabilityClass.lean— the directed index posetModularForm.CommIndex Γ₀(reverse-inclusionPreorder,Nonempty,IsDirectedvia closure of the class under⊓), plus two reusable foundational lemmas mathlib lacks:Subgroup.HasDetOne.of_le(antitonicity) andSubgroup.commensurable_inf.DirectLimit.lean—ModularForm.restrictSubgroupₗ(theℂ-linear restrictionMₖ(Γ) → Mₖ(Γ′)forΓ′ ≤ Γ), the limit with itsAddCommGroup/Module ℂstructure,ofLevel(with restriction-compatibilityofLevel_restrictand injectivityofLevel_injective), and theliftuniversal property.Why det-one
ModularForm Γ kis aModule ℂonly whenΓ.HasDetOne(otherwise justℝ); indexing over det-one subgroups keeps the limit aℂ-vector space. Conjugation preserves det-one, so the commensurator action survives.Verification
lake buildgreen for both modules + the folder aggregator (wired into the lib root).sorry;#print axiomsfor all 9 public declarations → onlypropext, Classical.choice, Quot.sound(theClassical.choiceis the classicalDecidableEqon the subgroup index, required byModule.DirectLimit).Scope
Space + core API only (producer → cleanup handoff). Out of scope / follow-up: the commensurator (Hecke) action of
GL₂⁺(ℚ)on the limit — the project already has aHeckePair/HeckeActionlayer to build on.🤖 Generated with Claude Code