Adjoining the centre to a subgroup of SL(2, ℤ)

Subgroup.withCenter adjoins the centre of the ambient group. For Γ ≤ SL(2, ℤ) that centre is {±I}, by Matrix.SpecialLinearGroup.mem_center_iff_eq_one_or_eq_neg_one, so the general characterisation Subgroup.mem_withCenter_iff — an element of Γ·Z(G) is one of Γ times a central one — sharpens to the concrete reading recorded here: Γ·{±I} is exactly Γ together with its negatives.

This is the form every SL(2, ℤ) consumer wants, and it depends on nothing beyond the general withCenter API and the description of the centre of SpecialLinearGroup, so it sits here rather than inside any one consumer.

The last section records the geometric counterpart: because Γ·{±I} contains both 1 and -1, the translates of the open fundamental domain 𝒟ᵒ indexed by the cosets of Γ·{±I} are pairwise disjoint. This needs no more about Γ than the membership description above, so it sits here too.

Main results

• Subgroup.mem_withCenter_iff_exists_eq_or_eq_neg: membership in Γ·{±I} is being ± an element of Γ.
• Subgroup.inf_withCenter_eq_of_le: for Γ' ≤ Γ with -I ∈ Γ → -I ∈ Γ', the part of Γ'·{±I} inside Γ is Γ'.
• TauCeti.ModularForm.index_eq_two_mul_index_withCenter_of_neg_one_notMem and TauCeti.ModularForm.relIndex_withCenter_eq_two_of_neg_one_notMem: when -I ∉ Γ, [SL₂(ℤ) : Γ] = 2 · [SL₂(ℤ) : ±Γ].
• ModularGroup.pairwise_disjoint_smul_fdo_out_withCenter: the translates of 𝒟ᵒ indexed by the cosets of Γ·{±I} are pairwise disjoint.

@[simp]

theorem Subgroup.mem_withCenter_iff_exists_eq_or_eq_neg {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {γ : Matrix.SpecialLinearGroup (Fin 2) ℤ} : γ ∈ Γ.withCenter ↔ ∃ γ' ∈ Γ, γ = γ' ∨ γ = -γ'

Membership in Γ·{±I}: its elements are exactly ± the elements of Γ. The adjoined centre of SL₂(ℤ) is {±I}, so the supremum only adds the negatives.

theorem Subgroup.inf_withCenter_eq_of_le {Γ Γ' : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} (hle : Γ' ≤ Γ) (hneg : -1 ∈ Γ → -1 ∈ Γ') : Γ ⊓ Γ'.withCenter = Γ'

Adjoining ±I to a subgroup adds nothing back inside a larger group that it does not already contain. For Γ' ≤ Γ with -I ∈ Γ → -I ∈ Γ', an element of Γ lying in Γ'·{±I} lies in Γ' itself: it is ± an element of Γ', and the minus sign can only occur when -I is in Γ, hence in Γ'.

This is what makes the cosets Γ / Γ' and Γ·{±I} / Γ'·{±I} match up, so that a sum over the former can be compared with the Petersson product, which is a sum over cosets of Γ'·{±I}.

theorem TauCeti.ModularForm.index_eq_two_mul_index_withCenter_of_neg_one_notMem {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} (h : -1 ∉ Γ) : Γ.index = 2 * Γ.withCenter.index

The ±Γ factor of two, index form: when -I ∉ Γ, the index of Γ in SL(2, ℤ) is twice the projective index [SL₂(ℤ) : ±Γ].

This is the conversion the general-level valence formula and the Sturm bound are stated against: both read k · [SL₂(ℤ) : ±Γ] / 12, while a full-coset norm product is computed over Γ-cosets, which is twice as many.

theorem TauCeti.ModularForm.relIndex_withCenter_eq_two_of_neg_one_notMem {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} (h : -1 ∉ Γ) : Γ.relIndex Γ.withCenter = 2

The ±Γ factor of two, relative-index form: Γ has index 2 inside Γ·{±I} when -I ∉ Γ. The geometric reading of index_eq_two_mul_index_withCenter_of_neg_one_notMem: adjoining -I exactly halves the number of cosets.

theorem ModularGroup.pairwise_disjoint_smul_fdo_out_withCenter (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) : Pairwise (Function.onFun Disjoint fun (q : Matrix.SpecialLinearGroup (Fin 2) ℤ ⧸ Γ.withCenter) => (Quotient.out q)⁻¹ • fdo)

The translates of 𝒟ᵒ indexed by the cosets of Γ·{±I} are pairwise disjoint. By ModularGroup.disjoint_smul_fdo it suffices that the chosen representatives of two distinct cosets differ neither by 1 nor by −1; and both 1 and −1 lie in Γ·{±I}, so either coincidence would identify the two cosets.