Skip to content

[Merged by Bors] - Add(NumberTheory/ModularForms/Identities): periods of modular forms.#12601

Closed
CBirkbeck wants to merge 10 commits intomasterfrom
modular_form_period_lemmas
Closed

[Merged by Bors] - Add(NumberTheory/ModularForms/Identities): periods of modular forms.#12601
CBirkbeck wants to merge 10 commits intomasterfrom
modular_form_period_lemmas

Conversation

@CBirkbeck
Copy link
Copy Markdown
Collaborator

@CBirkbeck CBirkbeck commented May 2, 2024 •
edited by Ruben-VandeVelde
Loading

Add some basic results about ModularGroup.T relating to slash invariant forms of level Gamma(N) and moving elements into verticalStrips. Needed for #12456

Open in Gitpod

@CBirkbeck CBirkbeck mentioned this pull request May 2, 2024
Closed
5 tasks
@CBirkbeck CBirkbeck marked this pull request as ready for review May 2, 2024 15:17
Ruben-VandeVelde
Ruben-VandeVelde reviewed May 5, 2024
View reviewed changes
Copy link
Copy Markdown
Contributor

@Ruben-VandeVelde Ruben-VandeVelde left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I can't really judge the mathematics, but the lean seems fine

@Ruben-VandeVelde Ruben-VandeVelde added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels May 5, 2024
@CBirkbeck CBirkbeck added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels May 7, 2024
@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 15, 2024
github-actions[bot]
github-actions bot reviewed May 22, 2024
View reviewed changes
CBirkbeck and others added 2 commits May 22, 2024 15:36
@CBirkbeck @github-actions
Update Mathlib.lean
6e00927 
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
@CBirkbeck
mathlib fix
2321d6e
@ghost ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 22, 2024
@Ruben-VandeVelde
Copy link
Copy Markdown
Contributor

Ruben-VandeVelde commented May 24, 2024

maintainer merge

(preferably a maintainer who knows about modular forms)

@github-actions
Copy link
Copy Markdown

github-actions bot commented May 24, 2024

🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde.

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label May 24, 2024
jcommelin
jcommelin reviewed May 25, 2024
View reviewed changes
Mathlib/NumberTheory/ModularForms/Identities.lean Outdated

namespace SlashInvariantForm

theorem lvl_N_periodic (N : ℕ) (k : ℤ) (f : SlashInvariantForm (Gamma N) k) (z : ℍ) (n : ℤ):
Copy link
Copy Markdown
Member

@jcommelin jcommelin May 25, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
theorem lvl_N_periodic (N : ℕ) (k : ℤ) (f : SlashInvariantForm (Gamma N) k) (z : ℍ) (n : ℤ):
theorem lvl_N_periodic (N : ℕ) (k : ℤ) (f : SlashInvariantForm (Gamma N) k) (z : ℍ) (n : ℤ) :

Copy link
Copy Markdown
Member

@jcommelin jcommelin May 25, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't really like the name lvl_N_periodic, since it refers to the variable N. (Just like I'm not a fan of the name padic_int.)

This name suggest that you maybe want a definition of what it means to be LevelPeriodic? And then you can prove with this lemma that SlashInvariantForms satisfy that predicate?

Copy link
Copy Markdown
Collaborator Author

@CBirkbeck CBirkbeck May 27, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hmm good point, so LevelPeriodic should be the width period, but we dont yet have the widths of cusps ( because we dont have cusps yet). How about I put width in the name (instead of N) for now and once we have cusps I can update the names if needed as this will be a special case of a more general result for any level?

Mathlib/NumberTheory/ModularForms/CongruenceSubgroups.lean
#align Gamma_zero_bot Gamma_zero_bot

lemma ModularGroup_T_pow_mem_Gamma (N M : ℤ) (hNM : N ∣ M) :
(ModularGroup.T ^ M) ∈ _root_.Gamma (Int.natAbs N) := by
Copy link
Copy Markdown
Member

@jcommelin jcommelin May 25, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hmm, should Gamma really be in the root namespace? I think it should be namespaced. (But not in this PR.)

Copy link
Copy Markdown
Collaborator Author

@CBirkbeck CBirkbeck May 27, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah yes I agree, I'll make a new PR after this and put it in a namespace.

@jcommelin jcommelin added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels May 25, 2024
@CBirkbeck CBirkbeck added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels May 27, 2024
@CBirkbeck CBirkbeck added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label May 27, 2024
@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label May 27, 2024
@jcommelin
Copy link
Copy Markdown
Member

jcommelin commented May 28, 2024

Thanks 🎉

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels May 28, 2024
mathlib-bors bot pushed a commit that referenced this pull request May 28, 2024
@CBirkbeck
Add(NumberTheory/ModularForms/Identities): periods of modular forms. (#…
f389222 
…12601)

Add some basic results about `ModularGroup.T` relating to slash invariant forms of level Gamma(N) and moving elements into verticalStrips. Needed for #12456
 


Co-authored-by: Chris Birkbeck <c.birkbeck@uea.ac.uk>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented May 28, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title Add(NumberTheory/ModularForms/Identities): periods of modular forms. [Merged by Bors] - Add(NumberTheory/ModularForms/Identities): periods of modular forms. May 28, 2024
@mathlib-bors mathlib-bors bot closed this May 28, 2024
@mathlib-bors mathlib-bors bot deleted the modular_form_period_lemmas branch May 28, 2024 14:16
callesonne pushed a commit that referenced this pull request Jun 4, 2024
@CBirkbeck @callesonne
Add(NumberTheory/ModularForms/Identities): periods of modular forms. (#…
066dff2 
…12601)

Add some basic results about `ModularGroup.T` relating to slash invariant forms of level Gamma(N) and moving elements into verticalStrips. Needed for #12456
 


Co-authored-by: Chris Birkbeck <c.birkbeck@uea.ac.uk>
js2357 pushed a commit that referenced this pull request Jun 18, 2024
@CBirkbeck @js2357
Add(NumberTheory/ModularForms/Identities): periods of modular forms. (#…
6d57923 
…12601)

Add some basic results about `ModularGroup.T` relating to slash invariant forms of level Gamma(N) and moving elements into verticalStrips. Needed for #12456
 


Co-authored-by: Chris Birkbeck <c.birkbeck@uea.ac.uk>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@jcommelin jcommelin jcommelin left review comments

@github-actions github-actions[bot] github-actions[bot] left review comments

@Ruben-VandeVelde Ruben-VandeVelde Ruben-VandeVelde left review comments

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@CBirkbeck @Ruben-VandeVelde @jcommelin