Commit 2026-10-13 19:23 1dd49d02

View on Github →

feat(NumberTheory/ModularForms): arithmetic subgroup improvements (#43742) Some modest additions to the theory of subgroups of GL(2, ℝ), and other general linear groups:

generalize adjoinNeg to arbitrary base rings & show it is functorial under suitable maps;
show intersection of an arithmetic subgroup with SL(2, ℝ) is also arithmetic;
show any two arithmetic subgroups are commensurable. These are used in the proof of finite-dimensionality of modular forms spaces.

Estimated changes

Modified Mathlib/NumberTheory/ModularForms/ArithmeticSubgroups.lean

modified def Subgroup.adjoinNegOne

added theorem Subgroup.adjoinNegOne_conj

modified theorem Subgroup.adjoinNegOne_eq_self_iff

added theorem Subgroup.adjoinNegOne_mono

modified theorem Subgroup.commensurable_adjoinNegOne_self

added theorem Subgroup.detOnePart_le

added theorem Subgroup.isArithmetic_conj_of_mem

modified theorem Subgroup.le_adjoinNegOne

added theorem Subgroup.map_adjoinNegOne

modified theorem Subgroup.mem_adjoinNegOne_iff

added theorem Subgroup.mem_detOnePart

deleted theorem Subgroup.negOne_mem_adjoinNegOne

added theorem Subgroup.neg_one_mem_adjoinNegOne

modified theorem Subgroup.relIndex_adjoinNegOne_eq_two

modified theorem Subgroup.relIndex_adjoinNegOne_ne_zero

added theorem adjoinNegOne_detOnePart