Fundamental domains for subgroups by coset tiling

If s is a fundamental domain for a group G acting on α, a subgroup H ≤ G with countable coset space has the [G : H]-fold tiling ⋃ q : G ⧸ H, (q.out)⁻¹ • s as a fundamental domain. This is how a fundamental domain for a finite-index subgroup (a congruence subgroup, say) is manufactured from a fundamental domain of the ambient group; countability of G ⧸ H — automatic at finite index — is what makes the tiling a countable union.

Main results

• MeasureTheory.IsFundamentalDomain.iUnion_smul_of_transversal: for any family r : ι → G with i ↦ ⟦(r i)⁻¹⟧ bijective onto G ⧸ H, the tiling ⋃ i, r i • s is an H-fundamental domain.
• MeasureTheory.IsFundamentalDomain.subgroup_iUnion_out_inv_smul: the special case of the canonical representatives, ⋃ q : G ⧸ H, (q.out)⁻¹ • s.
• MeasureTheory.IsFundamentalDomain.smul_of_eq_conjAct_pointwise_smul: an H₁-fundamental domain translates to a g H₁ g⁻¹-fundamental domain under g.
• MeasureTheory.IsFundamentalDomain.of_subgroupOf: a fundamental domain for H.subgroupOf K is one for H ⊓ K, the two subgroups being the same elements acting the same way.
• MeasureTheory.IsFundamentalDomain.iUnion_mul_smul_of_transversal: the double-coset tiling, at an arbitrary transversal — for any r : ι → Γ₂ with i ↦ ⟦(r i)⁻¹⟧ bijective onto Γ₂ ⧸ (δ⁻¹Γ₁δ ⊓ Γ₂), the translates ⋃ i, (δ · r i) • s tile a fundamental domain for Γ₁ ⊓ δΓ₂δ⁻¹.
• MeasureTheory.IsFundamentalDomain.iUnion_mul_out_inv_smul: the same at the canonical Quotient.out representatives, ⋃ᵥ (δ σᵥ⁻¹) • s over Γ₂ ⧸ (δ⁻¹Γ₁δ ⊓ Γ₂). A Hecke operator supplies its own representatives rather than Quotient.out's, so it is the transversal form above that applies there.
• MeasureTheory.IsFundamentalDomain.aedisjoint_smul_of_inv_mul_mem: translates g₁ • D, g₂ • D of an H-fundamental domain are a.e. disjoint whenever g₁ ≠ g₂ and g₁⁻¹ * g₂ ∈ H (needing only quasi-measure-preservation of the one translation).
• MeasureTheory.covolume_pos, MeasureTheory.covolume_conjAct_smul, MeasureTheory.covolume_eq_card_mul_covolume: for an invariant measure the covolume is positive, invariant under conjugation, and multiplied by the index on passing to a subgroup.

Ported from the AINTLIB LeanModularForms project, projects/LeanModularForms/Modularforms/PeterssonLevelN.lean (measure-theory section), as a prerequisite for fundamental domains of congruence subgroups.

theorem MeasureTheory.IsFundamentalDomain.iUnion_smul_of_transversal {G : Type u_1} {α : Type u_2} {ι : Type u_3} [Group G] [MeasurableSpace α] [MulAction G α] [Countable ι] {μ : Measure α} {H : Subgroup G} {s : Set α} (hs : IsFundamentalDomain G s μ) {r : ι → G} (hnull : ∀ (i : ι), NullMeasurableSet (r i • s) μ) (hr : Function.Bijective fun (i : ι) => ↑(r i)⁻¹) : IsFundamentalDomain (↥H) (⋃ (i : ι), r i • s) μ

Transversal coset tiling of a fundamental domain. If s is a fundamental domain for a group G acting on α, H ≤ G a subgroup, and r : ι → G a family such that i ↦ ⟦(r i)⁻¹⟧ enumerates the left cosets G ⧸ H bijectively, then ⋃ i, r i • s is a fundamental domain for the restricted H-action. The inverses make r a right transversal: each x ∈ G factors as h * r i with h ∈ H for exactly one i.

The index type must be countable ([Countable ι]), so that the tiling is a countable union. Beyond that, the only measure-theoretic hypothesis is null-measurability of the individual translates r i • s: measurability and invariance of the whole ambient action are not needed. subgroup_iUnion_out_inv_smul is the convenience form that supplies hnull from [MeasurableConstSMul G α] and [SMulInvariantMeasure G α μ].

theorem MeasureTheory.IsAddFundamentalDomain.iUnion_vadd_of_transversal {G : Type u_1} {α : Type u_2} {ι : Type u_3} [AddGroup G] [MeasurableSpace α] [AddAction G α] [Countable ι] {μ : Measure α} {H : AddSubgroup G} {s : Set α} (hs : IsAddFundamentalDomain G s μ) {r : ι → G} (hnull : ∀ (i : ι), NullMeasurableSet (r i +ᵥ s) μ) (hr : Function.Bijective fun (i : ι) => ↑(-r i)) : IsAddFundamentalDomain (↥H) (⋃ (i : ι), r i +ᵥ s) μ

Transversal coset tiling of a fundamental domain. If s is a fundamental domain for an additive group G acting on α, H ≤ G a subgroup, and r : ι → G a family over a countable index type ([Countable ι]) such that i ↦ ⟦-(r i)⟧ enumerates the cosets G ⧸ H bijectively, then ⋃ i, r i +ᵥ s is a fundamental domain for the restricted H-action. Beyond countability the only measure-theoretic hypothesis is null-measurability of the individual translates r i +ᵥ s.

theorem MeasureTheory.IsFundamentalDomain.subgroup_iUnion_out_inv_smul {G : Type u_1} {α : Type u_2} [Group G] [MeasurableSpace α] [MulAction G α] [MeasurableConstSMul G α] {μ : Measure α} [SMulInvariantMeasure G α μ] (H : Subgroup G) [Countable (G ⧸ H)] {s : Set α} (hs : IsFundamentalDomain G s μ) : IsFundamentalDomain (↥H) (⋃ (q : G ⧸ H), (Quotient.out q)⁻¹ • s) μ

Subgroup coset tiling of a fundamental domain. If s is a fundamental domain for a group G acting on α, then for any subgroup H ≤ G, the union of [G : H]-many translates (q.out)⁻¹ • s (for q ∈ G ⧸ H) is a fundamental domain for the restricted H-action on α: the inverses (q.out)⁻¹ of the canonical representatives form the right transversal. The coset space must be countable ([Countable (G ⧸ H)]) — in particular this covers every finite-index subgroup. This is IsFundamentalDomain.iUnion_smul_of_transversal at r q = (q.out)⁻¹.

theorem MeasureTheory.IsAddFundamentalDomain.addSubgroup_iUnion_out_neg_vadd {G : Type u_1} {α : Type u_2} [AddGroup G] [MeasurableSpace α] [AddAction G α] [MeasurableConstVAdd G α] {μ : Measure α} [VAddInvariantMeasure G α μ] (H : AddSubgroup G) [Countable (G ⧸ H)] {s : Set α} (hs : IsAddFundamentalDomain G s μ) : IsAddFundamentalDomain (↥H) (⋃ (q : G ⧸ H), -Quotient.out q +ᵥ s) μ

Subgroup coset tiling of a fundamental domain. If s is a fundamental domain for an additive group G acting on α, then for any subgroup H ≤ G whose coset space is countable ([Countable (G ⧸ H)], automatic at finite index), the union of the translates -q.out +ᵥ s (for q ∈ G ⧸ H) is a fundamental domain for the restricted H-action on α.

theorem MeasureTheory.IsFundamentalDomain.smul_of_eq_conjAct_pointwise_smul {G : Type u_1} {α : Type u_2} [Group G] [MeasurableSpace α] [MulAction G α] {μ : Measure α} {H₁ H₂ : Subgroup G} {s : Set α} (hs : IsFundamentalDomain (↥H₁) s μ) {g : G} (hg : Measure.QuasiMeasurePreserving (fun (x : α) => g⁻¹ • x) μ μ) (hgH : H₂ = ConjAct.toConjAct g • H₁) : IsFundamentalDomain (↥H₂) (g • s) μ

Conjugation-shift of a fundamental domain. If s is an H₁-fundamental domain (where H₁ ≤ G) and H₂ is the pointwise conjugate g · H₁ · g⁻¹ (in Subgroup pointwise smul form, via the ConjAct G-action), then g • s is an H₂-fundamental domain. Only quasi-measure-preservation of the single translation x ↦ g⁻¹ • x is required, not invariance under the whole group.

theorem MeasureTheory.IsFundamentalDomain.aedisjoint_smul_of_inv_mul_mem {G : Type u_1} {α : Type u_2} [Group G] [MeasurableSpace α] [MulAction G α] {μ : Measure α} {H : Subgroup G} {D : Set α} (hD : IsFundamentalDomain (↥H) D μ) {g₁ g₂ : G} (hg₁ : Measure.QuasiMeasurePreserving (fun (x : α) => g₁⁻¹ • x) μ μ) (h_mem : g₁⁻¹ * g₂ ∈ H) (h_ne : g₁ ≠ g₂) : AEDisjoint μ (g₁ • D) (g₂ • D)

AE-disjointness of arbitrary G-translates related by an H-element. Let D be a fundamental domain for a subgroup H ≤ G acting on α with a measure μ. For any distinct pair g₁, g₂ ∈ G whose relative position g₁⁻¹ * g₂ lies in H, the translates g₁ • D and g₂ • D are AE-disjoint with respect to μ — needing only quasi-measure-preservation of the single translation x ↦ g₁⁻¹ • x, not invariance under the whole group.

theorem MeasureTheory.IsAddFundamentalDomain.aedisjoint_vadd_of_neg_add_mem {G : Type u_1} {α : Type u_2} [AddGroup G] [MeasurableSpace α] [AddAction G α] {μ : Measure α} {H : AddSubgroup G} {D : Set α} (hD : IsAddFundamentalDomain (↥H) D μ) {g₁ g₂ : G} (hg₁ : Measure.QuasiMeasurePreserving (fun (x : α) => -g₁ +ᵥ x) μ μ) (h_mem : -g₁ + g₂ ∈ H) (h_ne : g₁ ≠ g₂) : AEDisjoint μ (g₁ +ᵥ D) (g₂ +ᵥ D)

AE-disjointness of arbitrary G-translates related by an H-element. Let D be a fundamental domain for a subgroup H ≤ G of an additive group acting on α with a measure μ. For any distinct pair g₁, g₂ ∈ G with -g₁ + g₂ ∈ H, the translates g₁ +ᵥ D and g₂ +ᵥ D are AE-disjoint, given quasi-measure-preservation of the single translation x ↦ -g₁ +ᵥ x.

theorem MeasureTheory.IsFundamentalDomain.of_subgroupOf {G : Type u_1} {α : Type u_2} [Group G] [MeasurableSpace α] [MulAction G α] {μ : Measure α} {H K : Subgroup G} {s : Set α} (hs : IsFundamentalDomain (↥(H.subgroupOf K)) s μ) : IsFundamentalDomain (↥(H ⊓ K)) s μ

A fundamental domain for a subgroup, read through a larger group it sits inside. If s is a fundamental domain for H.subgroupOf K acting through K, it is one for H ⊓ K acting through the ambient group: the two subgroups are the same set of elements and act the same way, so only the packaging differs.

theorem MeasureTheory.IsFundamentalDomain.iUnion_mul_smul_of_transversal {G : Type u_1} {α : Type u_2} {ι : Type u_3} [Group G] [MeasurableSpace α] [MulAction G α] [Countable ι] {μ : Measure α} {Γ₁ Γ₂ : Subgroup G} (δ : G) {s : Set α} (hs : IsFundamentalDomain (↥Γ₂) s μ) (hδ : Measure.QuasiMeasurePreserving (fun (x : α) => δ⁻¹ • x) μ μ) {r : ι → ↥Γ₂} (hnull : ∀ (i : ι), NullMeasurableSet (↑(r i) • s) μ) (hr : Function.Bijective fun (i : ι) => ↑(r i)⁻¹) : IsFundamentalDomain (↥(Γ₁ ⊓ ConjAct.toConjAct δ • Γ₂)) (⋃ (i : ι), (δ * ↑(r i)) • s) μ

The double-coset tiling of a fundamental domain, at an arbitrary transversal. Let s be a fundamental domain for Γ₂ and let δ be any element acting quasi-measure-preservingly. If r : ι → Γ₂ is a family with i ↦ ⟦(r i)⁻¹⟧ a bijection onto Γ₂ ⧸ (δ⁻¹Γ₁δ ⊓ Γ₂), then the translates (δ · r i) • s tile a fundamental domain for Γ₁ ⊓ δΓ₂δ⁻¹.

iUnion_mul_out_inv_smul below is this at r v = σᵥ⁻¹ for the canonical representatives, and is the statement to reach for when the family is not already fixed. The transversal form is what a Hecke operator needs, because the elements it sums over are supplied by the double-coset machinery rather than chosen by Quotient.out: two transversals of the same coset space give different translates, so a tiling stated only at Quotient.out does not transfer to them. That is the same reason iUnion_smul_of_transversal sits under subgroup_iUnion_out_inv_smul above.

Note the hypotheses this does not take: no measurability of the ambient action and no invariance of μ under it, only the null-measurability of the individual translates and quasi-measure-preservation of the single translation by δ⁻¹.

theorem MeasureTheory.IsFundamentalDomain.iUnion_mul_out_inv_smul {G : Type u_1} {α : Type u_2} [Group G] [MeasurableSpace α] [MulAction G α] {μ : Measure α} {Γ₁ Γ₂ : Subgroup G} [MeasurableConstSMul (↥Γ₂) α] [SMulInvariantMeasure (↥Γ₂) α μ] (δ : G) {s : Set α} (hs : IsFundamentalDomain (↥Γ₂) s μ) (hδ : Measure.QuasiMeasurePreserving (fun (x : α) => δ⁻¹ • x) μ μ) [Countable (↥Γ₂ ⧸ (ConjAct.toConjAct δ⁻¹ • Γ₁).subgroupOf Γ₂)] : IsFundamentalDomain (↥(Γ₁ ⊓ ConjAct.toConjAct δ • Γ₂)) (⋃ (v : ↥Γ₂ ⧸ (ConjAct.toConjAct δ⁻¹ • Γ₁).subgroupOf Γ₂), (δ * (↑(Quotient.out v))⁻¹) • s) μ

The double-coset tiling of a fundamental domain. Let s be a fundamental domain for Γ₂, and let δ be any element acting quasi-measure-preservingly. The translates (δ · σᵥ⁻¹) • s, taken over the canonical representatives σᵥ of Γ₂ ⧸ (δ⁻¹Γ₁δ ⊓ Γ₂), tile a fundamental domain for Γ₁ ⊓ δΓ₂δ⁻¹.

The index type is TauCeti.DoubleCoset.DecompQuotient Γ₂ Γ₁ δ⁻¹, the one a Hecke decomposition Γ₁ δ Γ₂ = ⊔ᵥ Γ₁ (δ σᵥ⁻¹) is indexed by — but σᵥ here is Quotient.out's choice, and a Hecke operator's σᵥ comes from the double-coset machinery instead. Two transversals of the same coset space give different translates, so this statement does not transfer to them; iUnion_mul_smul_of_transversal is the form that does.

Ported from AINTLIB (github.com/CBirkbeck/AINTLIB @ 6d87d596a5372d5b122c47b7082d4c3afa9b7c3b, Apache-2.0), projects/LeanModularForms/LeanModularForms/HeckeRIngs/GL2/AdjointTheory/ FDTransport.lean, which proves this for Γ₁(N) and a concrete α.

theorem MeasureTheory.covolume_pos {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] [MeasurableSpace α] [Countable G] [MeasurableConstSMul G α] {μ : Measure α} [SMulInvariantMeasure G α μ] [HasFundamentalDomain G α μ] (hμ : μ ≠ 0) : 0 < covolume G α μ

Covolume is positive: a countable group acting with a fundamental domain for a nonzero invariant measure has positive covolume.

@[simp]

theorem MeasureTheory.covolume_conjAct_smul {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] [MeasurableSpace α] [MeasurableConstSMul G α] {μ : Measure α} [SMulInvariantMeasure G α μ] (Γ : Subgroup G) [Countable ↥Γ] [HasFundamentalDomain (↥Γ) α μ] (g : G) : covolume (↥(ConjAct.toConjAct g • Γ)) α μ = covolume (↥Γ) α μ

Covolume is a conjugacy invariant: for an invariant measure, a countable subgroup Γ with a fundamental domain and its conjugate g Γ g⁻¹ have the same covolume.

theorem MeasureTheory.covolume_eq_card_mul_covolume {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] [MeasurableSpace α] {μ : Measure α} {Γ Δ : Subgroup G} [MeasurableConstSMul (↥Γ) α] [SMulInvariantMeasure (↥Γ) α μ] [Countable ↥Γ] [HasFundamentalDomain (↥Γ) α μ] (h : Δ ≤ Γ) : covolume (↥Δ) α μ = ↑(ENat.card (↥Γ ⧸ Δ.subgroupOf Γ)) * covolume (↥Γ) α μ

Covolume is multiplicative in the index: for a measure invariant under subgroups Δ ≤ Γ with Γ countable and having a fundamental domain, the covolume of Δ is the index [Γ : Δ], counted in ℕ∞, times the covolume of Γ.