Hecke rings: the double coset API #
Basic API for the double cosets HeckeCoset indexing a Hecke coset module, following
Shimura, Chapter 3. This file provides representatives of double cosets, the
characterisation of when two elements give the same double coset, and the quotient
Γ₁ ⧸ (Γ₁ ∩ gΓ₂g⁻¹) indexing the left cosets inside a double coset Γ₁gΓ₂, which is used to
define the Hecke product in later files and is finite for a Hecke triple. It also houses
the basis-element API of the coset module: HeckeCosetModule.single with its evaluation,
summation, and additivity laws, the induction_linear principle, and the transported
Module instance — placed at this layer so every later file (convolution, one, and the
coset actions) can build on one shared vocabulary. Finally it defines the degree of a
double coset, the number of left cosets in its decomposition, together with its
relative-index form, since that count is read straight off DecompQuotient.
The coset vocabulary is vendored from the in-review mathlib4 PR
#41253 (Chris Birkbeck), per the
ModularForms roadmap's dependency policy; migrate to Mathlib and delete it when that stack
merges. The degree section is instead ported from the AINTLIB LeanModularForms project
(LeanModularForms/HeckeRIngs/AbstractHeckeRing/Degree.lean, Chris Birkbeck,
https://github.com/CBirkbeck/AINTLIB/tree/main/projects/LeanModularForms).
Main definitions #
HeckeCoset.toSet: the underlying setH₁gH₂of a double coset.HeckeCoset.rep: a chosen representative inΔ.HeckeCoset.map: functoriality in the triple(Δ, H₁, H₂)along inclusions — widening the coefficient subgroups can only merge double cosets, never split them. Its computation rule ismap_mkand its functor laws aremap_idandmap_map;HeckeRing.GL2.toLevelOneCoset(HeckeRing/GL2/Gamma0/CosetMap.lean) is itsΓ₀-specialisation.HeckeCoset.restrictandHeckeCoset.restrictEquiv: a Hecke coset re-read over a subgroupHcontaining its whole triple, and the resulting equivalence of quotients. WhereHeckeCoset.mapmoves a coset along inclusions within a fixed ambient group, these move it between ambient groups — the case a theorem needs when it is applied along a homomorphism defined only on a subgroup.DoubleCoset.DecompQuotient: the quotientΓ₁ ⧸ (Γ₁ ∩ gΓ₂g⁻¹)indexing the left cosets inΓ₁gΓ₂; finite for a Hecke triple. Its mirrorDecompQuotient Γ₂ Γ₁ g⁻¹indexes the right cosetsΓ₁a, and is finite too.DoubleCoset.decompQuotientEquivMapOfInjective: that quotient transported along an injective homomorphism, withDoubleCoset.map_subgroupOf_smulfor the subgroup underneath it;DoubleCoset.decompQuotientEquivMap(HeckeRing/Multiplicity/Equiv.lean) is its special case at an isomorphism.DoubleCoset.decompQuotientEquivMapOfKerInfLe: the same transport without injectivity, under an ambient subgroupHcontainingΓ₂and receivingg⁻¹ Γ₁ g, andφ.ker ⊓ H ≤ Γ₂. The target element is supplied by an equationhd : φ g = d, so a consumer holding(φ g)⁻¹rather thanφ g⁻¹needs no type transport of its own. This is the version a fundamental-domain statement needs: the group that acts faithfully onℍis a quotient, so the homomorphism reaching it is deliberately non-injective, and the kernel is absorbed by the denominator instead.HeckeCosetModule.single: the basis elementb • [D]of the Hecke coset module, withsingle_apply,sum_single_index,smul_single_one,single_add,induction_linear, and theModule RinstanceHeckeCosetModule.instModule.Pointwise evaluation of the coset module:
zero_apply,add_apply,smul_apply,mem_support_iff,notMem_support_iff,sum_def,sum_applyandsum_smul_index.HeckeCosetModuleis adefoverFinsuppcarrying transported instances, so Mathlib'sFinsuppevaluation lemmas hold definitionally — they can be applied in term mode — butrw,simpandgrindmatch syntactically and so cannot see through the wrapper. These restatements are what makes those facts usable tactically.In particular these do not compete with their
Finsupporiginals: at this typesimp [Finsupp.mem_support_iff]reports the argument as unused andsimp [Finsupp.add_apply]makes no progress, because neither left-hand side matches through the wrapper. The wrapper restatement is the only formsimpcan apply.HeckeCoset.degree: the number of left cosets in the decomposition of a double coset, withdegree_eq_relIndexanddegree_mkpresenting it as a relative index,degree_eq_natCard_decompQuotientas the (hypothesis-free) count of that quotient, anddegree_onethe identity coset.
Main results #
HeckeCoset.eq_iff:mk H₁ H₂ g = mk H₁ H₂ h ↔ H₁gH₂ = H₁hH₂.HeckeCoset.toSet_injective: a double coset is determined by its underlying set.DoubleCoset.doubleCoset_eq_iUnion_rightCosetsandDoubleCoset.op_mul_out_inv_smul_injective: Shimura's decompositionΓ₁gΓ₂ = ⊔ᵥ Γ₁(gτᵥ⁻¹)into right cosets, indexed without repetition byDecompQuotient Γ₂ Γ₁ g⁻¹— the mirror ofDoubleCoset.doubleCoset_eq_iUnion_leftCosetsandmk_out_mul_injective.DoubleCoset.doubleCoset_eq_iUnion_rightCosets_of_forall_exists: a criterion for a supplied family of right-coset representatives to cover a double coset.DoubleCoset.rightCosetRep_mem,DoubleCoset.exists_mem_out_mul_inv_eq_mul_rightCosetRepandDoubleCoset.exists_bijective_rightCosetRep_smul_eq: the representativesδ τᵥ⁻¹lie in any submonoid containingδandΓ₂; an elementδ h₂⁻¹of the double coset is aΓ₁-multiple of the representative ofh₂'s class; and any family of representatives of the right cosets is matched with the chosen one by a bijection — the coset bookkeeping every operator built by summing over the decomposition (slash sums, Hecke sums on a representation) reindexes with.DoubleCoset.card_filter_eq_of_rightCosetRep_smul_eq: a family naming each right coset of the double coset exactlymtimes has exactlymmembers over each chosen representative — the counting half of collapsing such a sum tom •the operator.DoubleCoset.doubleCoset_mul_doubleCoset_eq_iUnion_rightCosets: Shimura's covering identity — the productsaᵢbⱼof two families of right-coset representatives cover the product setΓ₁δ₁Γ₂ · Γ₂δ₂Γ₃, though not without repetition.IsHeckeTriple.commensurable_conjAct_inv_left, and theFiniteinstance beside it: that right-coset index is finite, the mirror of theFintypeinstance onDecompQuotient H₁ H₂ g.HeckeCoset.restrict_bijective, withHeckeCoset.restrict_injectiveandHeckeCoset.restrict_surjective: restriction loses nothing — the double cosets ofΔand those ofΔ.comap H.subtypeare the same objects described twice.
References #
The underlying set H₁gH₂ of a double coset, well-defined on the quotient.
The @[simp] lemma toSet_mk evaluates it at a representative and toSet_eq_doubleCoset_rep at
the chosen rep. Mathlib's DoubleCoset.quotToDoubleCoset is the analogue for the double cosets
of the whole group G rather than of the submonoid Δ.
Equations
- D.toSet = Quotient.lift (fun (g : ↥Δ) => DoubleCoset.doubleCoset ↑g ↑H₁ ↑H₂) ⋯ D
Instances For
The chosen representative in Δ of a double coset D, picked by Quotient.out: it lies
in D.toSet (rep_mem), and mk_rep recovers D from it. The choice is arbitrary —
(mk H₁ H₂ w).rep need not be w; it only spans the same double coset (doubleCoset_rep_mk).
Equations
- D.rep = Quotient.out D
Instances For
The chosen representative of a double coset D is Quotient.out D.
The double coset of a chosen representative is the double coset it was chosen from.
Two elements of Δ define the same HeckeCoset iff their double cosets coincide.
The right-hand side is an equality of subsets of the ambient group G, so g and h are
identified through elements of H₁ and H₂ that need not lie in Δ. Use
HeckeCoset.mk_eq_mk_of_mem for the one-directional form starting from a membership.
The underlying set of the double coset of g is H₁gH₂.
For an arbitrary double coset, rather than an explicit mk H₁ H₂ g, use
toSet_eq_doubleCoset_rep.
The underlying set of a double coset is the double coset of its chosen representative.
For an explicit mk H₁ H₂ g use toSet_mk instead; rep_mem is the membership fact this
yields.
Membership in the underlying set characterises the double coset: for g : Δ, the element
g lies in D.toSet exactly when D is the double coset of g.
This is the elimination rule for toSet: it turns a membership into an equation between double
cosets, so a consumer need not unfold the quotient. It is the Δ-indexed analogue of Mathlib's
DoubleCoset.mem_quotToDoubleCoset_iff, which characterises membership for the double cosets of
the whole group G.
A double coset is determined by its underlying set.
This is eq_iff read at the level of double cosets rather than of representatives; the Iff form
D₁.toSet = D₂.toSet ↔ D₁ = D₂ is toSet_injective.eq_iff.
The chosen representative of a double coset lies in its underlying set.
The membership form of toSet_eq_doubleCoset_rep, for an arbitrary double coset. At an explicit
mk H₁ H₂ w, use rep_mk_mem_doubleCoset instead.
The chosen representative of mk H₁ H₂ w lies in the double coset of w.
The toSet-evaluated form of rep_mem at an explicit mk H₁ H₂ w. Its mirror
mem_doubleCoset_rep_mk states the same relation with the two elements exchanged: w left of
the ∈ and the representative inside the doubleCoset.
mk and rep name the same double coset: the chosen representative of mk H₁ H₂ w
spans the double coset w was taken from.
The cancellation holds only inside doubleCoset: (mk H₁ H₂ w).rep = w is false in general, as
the representative is chosen arbitrarily from the coset. mem_doubleCoset_rep_mk and
rep_mk_mem_doubleCoset are its membership forms.
w lies in the double coset of the chosen representative of mk H₁ H₂ w.
The mirror of rep_mk_mem_doubleCoset, which places the representative left of the membership and
w inside the double coset; both hold because doubleCoset_rep_mk identifies the two sets.
mk H₁ H₂ g₁ = mk H₁ H₂ g₂ when g₁ lies in the double coset of g₂.
The one-directional form of eq_iff, starting from a membership rather than an equality of sets.
The membership is between the images in G, so call sites typically supply it as
DoubleCoset.mem_doubleCoset.mpr ⟨l, hl, r, hr, _⟩ after unfolding any Δ-side coercion.
Mathlib's DoubleCoset.mk_eq_of_doubleCoset_eq does not cover this: its conclusion lands in the
double coset quotient of all of G, not in HeckeCoset Δ H₁ H₂.
Functoriality of HeckeCoset in its triple. Inclusions Δ ≤ Δ', H₁ ≤ H₁' and
H₂ ≤ H₂' send H₁ g H₂ to H₁' g H₂': widening the coefficient subgroups can only merge
double cosets, never split them.
Compute with map_mk: the underlying element of G is unchanged, only retyped into Δ' by
Submonoid.inclusion. The functor laws are map_id and map_map; all three are @[simp].
This widens subgroups inside one fixed ambient group — transporting a double coset along a
homomorphism G →* G' is a different operation, carried out for the decomposition quotient by
DoubleCoset.decompQuotientEquivMapOfInjective.
Equations
- HeckeCoset.map hΔ h₁ h₂ = Quotient.map ⇑(Submonoid.inclusion hΔ) ⋯
Instances For
The computation rule for map: it keeps the representative, re-typed by the inclusion hΔ.
The representative lands in Δ', not in G, so a call site holding g : Δ needs no coercion of
its own. Its neighbours map_id and map_map are instead stated for an arbitrary coset.
Induction: to prove something for all double cosets, prove it for mk H₁ H₂ g.
Two-argument induction for double cosets.
Restriction to a smaller ambient group #
map above moves a Hecke coset along inclusions within a fixed G. This moves one between
ambient groups: when the whole triple (Δ, H₁, H₂) lies inside a subgroup H, the double
cosets are the same sets read inside ↥H, so the quotient is the same quotient.
Why it is wanted: a theorem quantified over the ambient group is applied along a homomorphism out
of that group, and the available homomorphisms are frequently defined only on a subgroup — the
motivating case being TauCeti.ratPosToPSL2R, whose source is GL(2, ℚ)⁺, while the Hecke cosets
of interest live in GL (Fin 2) ℚ.
Re-read a Hecke coset over a subgroup containing its whole triple. With Δ ≤ H,
H₁ ≤ H and H₂ ≤ H, the double coset H₁ g H₂ of g : Δ is a subset of H, and this is
that same double coset read in ↥H.
Like map, this is induced on the quotient rather than defined through a chosen representative,
so restrict_mk is its defining equation.
Instances For
Restriction of an explicitly constructed coset.
Restriction is an equivalence. With the whole triple inside H, the double cosets of
Δ and those of Δ.comap H.subtype are the same objects described twice, so the two quotients
are canonically equivalent — restrict is the forward direction, and the inverse simply forgets
that a representative lies in H.
Equations
- One or more equations did not get rendered due to their size.
Instances For
restrictEquiv computes as restrict in the forward direction.
The inverse of restrictEquiv on an explicitly constructed coset: it simply forgets that the
representative lies in H.
The round trip through restrictEquiv is the identity, in the direction that starts in
the ambient group.
The round trip through restrictEquiv is the identity, in the direction that starts in
the subgroup.
restrict is bijective.
restrict is injective.
restrict is surjective.
The decomposition quotient Γ₁ ⧸ (Γ₁ ∩ gΓ₂g⁻¹), indexing the left cosets of Γ₂ inside
the double coset Γ₁gΓ₂; see DoubleCoset.doubleCoset_eq_iUnion_leftCosets.
Equations
- DoubleCoset.DecompQuotient Γ₁ Γ₂ g = (↥Γ₁ ⧸ (ConjAct.toConjAct g • Γ₂).subgroupOf Γ₁)
Instances For
The left cosets σᵢ g Γ₂ of the decomposition of Γ₁gΓ₂ are pairwise distinct: the map
i ↦ σᵢ g Γ₂ into G ⧸ Γ₂ is injective.
The conjugation criterion for the stabilizer subgroup indexing DecompQuotient: an element
of (ConjAct.toConjAct g • H₂).subgroupOf H₁ conjugates by g into H₂.
The stabilizer indexing the decomposition transports along an injective homomorphism:
the image of (gΓ₂g⁻¹) ∩ Γ₁ inside φ(Γ₁) is (φ(g) φ(Γ₂) φ(g)⁻¹) ∩ φ(Γ₁). Injectivity is what
gives the inclusion that is not formal: an element of φ(Γ₁) conjugating into φ(Γ₂) must come
from one of Γ₁ conjugating into Γ₂.
The decomposition quotient transports along an injective homomorphism. For φ injective,
Γ₁ ⧸ (Γ₁ ∩ gΓ₂g⁻¹) and φ(Γ₁) ⧸ (φ(Γ₁) ∩ φ(g)φ(Γ₂)φ(g)⁻¹) are in bijection, by φ on
representatives.
This is index transport along an injective map, and nothing more: it identifies the two
decomposition quotients, leaving the acting group unchanged. G and G' are arbitrary groups
here, with no action in sight.
It does not supply a fundamental-domain tiling, and the reason is specific to the modular
setting rather than general: there the target acts on ℍ through a matrix group modulo scalars, so
an injective φ retains -I ∈ Γ₂, whose image is a non-identity element acting trivially — and
MeasureTheory.IsFundamentalDomain then holds for no set of positive measure, its disjointness
being Pairwise over distinct group elements. decompQuotientEquivMapOfKerInfLe is the version for
that application: it drops injectivity for a kernel condition, which is what leaves room for a
faithful action downstream.
Equations
- DoubleCoset.decompQuotientEquivMapOfInjective φ hφ Γ₁ Γ₂ g = TauCeti.QuotientGroup.congrOfMapEq (Γ₁.equivMapOfInjective φ hφ) ⋯
Instances For
The stabilizer of the decomposition transports along φ. The image under φ of
(gΓ₂g⁻¹ ∩ Γ₁), viewed inside Γ₁, is (φ(g)φ(Γ₂)φ(g)⁻¹ ∩ φ(Γ₁)) viewed inside φ(Γ₁).
Injectivity of φ is not required. In its place: an ambient subgroup H containing Γ₂ and
receiving g⁻¹ Γ₁ g, together with φ.ker ⊓ H ≤ Γ₂. The kernel may therefore be
nontrivial, which is what lets the decomposition reach a group acting faithfully on ℍ; the
injective version is map_subgroupOf_smul.
The decomposition quotient transports without injectivity, under an ambient subgroup. The kernel is absorbed by the denominator, so the index is unchanged.
Equations
- DoubleCoset.decompQuotientEquivMapOfKerInfLe φ Γ₁ Γ₂ H g hd h₂ hconj hker = hd ▸ TauCeti.QuotientGroup.congrOfSurjectiveOfKerLe (φ.subgroupMap Γ₁) ⋯ ⋯ ⋯
Instances For
Equality of classes in DecompQuotient H₁ H₂ g gives the conjugation relation between their
representatives: u₁⁻¹ u₂ lies in the stabilizer indexing the decomposition, so conjugating it
by g lands in H₂.
Note the two subgroups play different roles: the representatives live in H₁, which indexes the
quotient, while the conclusion lands in H₂, which is the one being conjugated. They coincide in
the common case DecompQuotient H H g.
Shimura's decomposition of a double coset into right cosets. Γ₁gΓ₂ is the union of the
right cosets Γ₁ · (g τᵥ⁻¹), where τᵥ runs over representatives of Γ₂ ⧸ (Γ₂ ∩ g⁻¹Γ₁g) — the
mirror of DoubleCoset.doubleCoset_eq_iUnion_leftCosets, and of Mathlib's
doubleCoset_union_rightCoset, which is indexed by all of Γ₂ and so repeats each coset.
The inverse on τᵥ is what converts the left-coset quotient Γ₂ ⧸ (Γ₂ ∩ g⁻¹Γ₁g) into an index
for the right cosets: Γ₁ g τ = Γ₁ g τ' exactly when τ'τ⁻¹ ∈ Γ₂ ∩ g⁻¹Γ₁g.
It lives here rather than beside doubleCoset_eq_iUnion_leftCosets because it is phrased with
DecompQuotient, which this file defines.
A right-coset decomposition criterion. Suppose every product a * g with g ∈ Γ₂
factors as d * rep i with d ∈ Γ₁, and conversely every rep i equals a * g for some
g ∈ Γ₂. Then the double coset Γ₁ a Γ₂ is the union of the right cosets
Γ₁ · rep i.
This criterion proves coverage only; injectivity of the representative family is a separate property.
The right cosets of doubleCoset_eq_iUnion_rightCosets are pairwise distinct, so that union
is a partition and the sum of a Γ₁-invariant function over it counts each coset once.
Shimura's covering identity for a product of double cosets (§3.4). If Γ₁ δ₁ Γ₂ is the
union of the right cosets Γ₁ aᵢ and Γ₂ δ₂ Γ₃ is the union of the right cosets Γ₂ bⱼ, then
the pointwise product Γ₁ δ₁ Γ₂ · Γ₂ δ₂ Γ₃ is the union of the right cosets Γ₁ aᵢ bⱼ.
The two double cosets splice because Γ₂ Γ₂ = Γ₂: an element of the product is u v with
u ∈ Γ₁ δ₁ Γ₂ and v ∈ Γ₂ δ₂ Γ₃; writing v = g bⱼ with g ∈ Γ₂ moves g into u, and u g
is again in Γ₁ δ₁ Γ₂, hence in some Γ₁ aᵢ.
⚠ The union is not disjoint, and the family (i, j) ↦ Γ₁ aᵢ bⱼ is in general far from
injective. Any repetitions here are right-coset collisions; this theorem neither counts them nor
identifies them with DoubleCoset.multiplicity, which uses left-coset representatives. The
identity supplies coverage only, exactly as
doubleCoset_eq_iUnion_rightCosets_of_forall_exists does for a single double coset.
Representatives of the right cosets in a double-coset decomposition #
The representative δ τᵥ⁻¹ of the v-th right coset Γ₁ aᵥ in the decomposition
Γ₁ δ Γ₂ = ⊔ᵥ Γ₁ aᵥ, where δ is the chosen representative of the double coset D and τᵥ
runs over the chosen representatives of Γ₂ ⧸ (Γ₂ ∩ δ⁻¹Γ₁δ).
This is the named form of the union in doubleCoset_eq_iUnion_rightCosets above, at g := D.out.
It is pure group theory — δ τᵥ⁻¹ in any group — which is why it sits here rather than with the
modular-forms slash action that consumes it.
The inverse is what converts the left-coset quotient Mathlib supplies into the right-coset index the decomposition needs.
Equations
- DoubleCoset.rightCosetRep D v = ↑(Quotient.out D) * (↑(Quotient.out v))⁻¹
Instances For
Defining equation for rightCosetRep. Since rightCosetRep is not @[expose], a
downstream module rewrites with this instead of unfolding the body.
Shimura's decomposition of the double coset, in the rightCosetRep spelling:
Γ₁ δ Γ₂ = ⋃ᵥ Γ₁ (δ τᵥ⁻¹). Since rightCosetRep is not @[expose], this is how a downstream
module reads DoubleCoset.doubleCoset_eq_iUnion_rightCosets at the representatives the slash sum
is defined with.
The pieces of that decomposition are pairwise distinct, in the same spelling:
DoubleCoset.op_mul_out_inv_smul_injective read at rightCosetRep.
Each representative lies in the double coset, being a member of its own piece.
Every member of the double coset shares its right coset with a chosen representative: it
lies in one of the pieces, and two right cosets of Γ₁ that meet are equal.
Each representative δ τᵥ⁻¹ lies in any submonoid Δ' containing the chosen δ and the
group Γ₂. Only Γ₂ and δ are constrained: nothing is asked of Γ₁, nor of Δ beyond
supplying δ. The hypothesis on Γ₂ is used at τᵥ⁻¹, which lies in Γ₂ because Γ₂ is a
group.
An element δ h₂⁻¹ of the double coset is a Γ₁-multiple of the representative attached
to h₂'s class. For h₂ ∈ Γ₂, δ h₂⁻¹ = γ₁ · rightCosetRep D ⟦h₂⟧ for some γ₁ ∈ Γ₁, where
δ = D.out: if u is the chosen representative of ⟦h₂⟧ then δ (u⁻¹ h₂) δ⁻¹ ∈ Γ₁
(conj_mem_of_mk_eq), and γ₁ is its inverse.
hh₂ is part of the statement rather than a side condition: the right-hand side names the class
⟦⟨h₂, hh₂⟩⟧. Membership is a Prop, so any proof of h₂ ∈ Γ₂ names the same class. This is
the per-summand step behind Shimura's Proposition 3.37: right multiplication by an element of
Γ₂ permutes the right cosets Γ₁ aᵥ, and a Γ₁-invariant summand does not see γ₁.
Two families of representatives of the same right cosets are matched by a bijection.
If the cosets Γ₁ aᵢ are pairwise distinct and cover Γ₁ D.out Γ₂, then the index type ι is
matched with DecompQuotient Γ₂ Γ₁ (D.out)⁻¹ — the index Shimura's decomposition sums over — by a
bijection φ carrying each Γ₁ aᵢ to Γ₁ (rightCosetRep D (φ i)).
This is pure coset bookkeeping. It identifies the two index sets compatibly with the cosets they
name, and only that: the matched representatives aᵢ and rightCosetRep D (φ i) differ by a
factor of Γ₁, so a summand that can see the representative still distinguishes them. Equating
two sums over the families needs, in addition, a summand depending only on the coset — for a
slash term, HeckeRing.GL2.slash_eq_of_rightCoset_eq on a Γ₁-invariant function; for a
representation, Representation.comp_eq_of_rightCoset_eq.
Each fibre of the naming map has m elements. Let g name, for each index i, the
right coset that aᵢ lies in — Γ₁ aᵢ = Γ₁ (rightCosetRep D (g i)) — and let every right coset
of the double coset be named by exactly m members of the family. Then g i = v for exactly
m indices i, whatever v.
The hypothesis counts indices by the coset they name and the conclusion counts them by their
image under g; the two agree because rightCosetRep names distinct cosets by distinct
elements (op_rightCosetRep_smul_injective).
Like exists_bijective_rightCosetRep_smul_eq this is pure coset bookkeeping. It is the counting
half of the multiplicity-weighted collapse of a sum over a family that names each right coset m
times: each fibre has m elements. Reaching m • a single operator needs the other half too —
that the terms on a fibre agree, which is what a summand depending only on the right coset
supplies.
Every member of the double coset H₁gH₂ of an element of Δ lies in Δ.
For a Hecke triple, the decomposition quotient of any g : Δ is finite: Δ
commensurates H₂, which is commensurable with H₁.
Conjugating the left subgroup by the inverse of an element of Δ gives a subgroup
commensurable with the right one. This is commensurable_conjAct_right on the other flank:
the commensurator is a subgroup, so it contains g⁻¹ along with g.
It is what makes DecompQuotient H₂ H₁ g⁻¹ — the index of Shimura's decomposition of H₁gH₂
into right cosets H₁a — finite.
For a Hecke triple, the right-coset decomposition quotient of any g : Δ is finite.
This is the companion of the instance above on the other flank, and it is the finiteness the
slash sum over Shimura's decomposition H₁gH₂ = ⊔ᵥ H₁aᵥ needs. Finite rather than Fintype:
no enumeration is chosen here, and a second Fintype on a quotient of the same shape would
compete with the one above.
The degree of a double coset: the number of left cosets σᵢgH₂ in the decomposition
H₁gH₂ = ⊔ᵢ σᵢgH₂, i.e. the relative index [H₁ : H₁ ∩ gH₂g⁻¹]. Stating it needs no
finiteness — Subgroup.relIndex is a Nat.card, which is 0 when the index is infinite;
the Hecke-triple hypothesis enters only where the count is genuinely finite.
Instances For
The degree as a relative index: deg(H₁gH₂) = [H₁ : H₁ ∩ gH₂g⁻¹]. This is the form in
which concrete degree computations identify the count with a congruence-subgroup index.
The degree at an explicit representative: the count computed from any g, not only
from the chosen rep. This is the form concrete coset calculations use, since they present
a double coset as mk H H g.
The degree counts the decomposition quotient. No finiteness is involved: a relative
index is by definition the Nat.card of exactly this quotient, so the two sides are the
same term.
Under the Hecke-triple hypothesis the decomposition quotient is finite, so the degree is
its Fintype.card. The hypothesis is needed only for the Fintype instance, not for the
count itself — see degree_eq_natCard_decompQuotient.
Every double coset has positive degree.
A basis element of the Hecke coset module: single R D b is the formal sum b • [D]. As
for Finsupp itself, this is the type-correct way to produce elements of
HeckeCosetModule Δ H₁ H₂ R. Only [Zero R] is assumed, so consumers with coefficient
assumptions below Semiring (the left-coset scalar operations) can use it.
Equations
- HeckeCosetModule.single R D b = Finsupp.single D b
Instances For
Finsupp.sum_single_index, as a wrapper-level equation: summing over a basis element
evaluates the summand at its point.
Finsupp.single_zero, as a wrapper-level equation.
Every element is the sum of its basis components.
Finsupp.single_add, as a wrapper-level equation.
Finsupp.induction_linear, restated for the wrapper type HeckeCosetModule Δ H₁ H₂ R in
its basis vocabulary single, in the same way that MonoidAlgebra.induction_linear restates
it for MonoidAlgebra: to prove a property of all elements, prove it for 0, for sums, and
for basis elements.
The R-module structure of the Hecke coset module, transporting the standard Finsupp
module structure to the wrapper type.
Equations
- HeckeCosetModule.instModule R = { smul := HeckeCosetModule.instModule._aux_1 R, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }
Pointwise evaluation #
HeckeCosetModule is a def over Finsupp, so Mathlib's Finsupp evaluation lemmas hold
definitionally but neither rw nor simp can match them through the wrapper. These are the
wrapper-level restatements; without them every consumer re-derives its own private copies.
Each is stated at the coefficient assumptions its underlying operation actually needs: the
FunLike coercion and Finsupp.support need only [Zero R], while the wrapper's 0, +
and • come from its AddCommMonoid and Module instances.
Finsupp.mem_support_iff, at the wrapper type.
Finsupp.notMem_support_iff, at the wrapper type: the elimination form of
mem_support_iff. Deliberately unannotated — mem_support_iff is the @[simp] normal form,
and simp discharges this direction from it.
Finsupp.sum unfolded to a Finset.sum, at the wrapper type.
Finsupp.sum_apply, at the wrapper type: evaluation commutes with a Finsupp.sum. The
target coefficients are independent of the source's.
Finsupp.zero_apply, at the wrapper type. Not @[grind =]: unlike Mathlib's
Finsupp.zero_apply, where M is recoverable from (0 : α →₀ M), the wrapper's coercion
leaves R and its AddCommMonoid uninstantiable, and grind rejects the pattern.
Finsupp.add_apply, at the wrapper type.
Finsupp.smul_apply, at the wrapper type.
Finsupp.sum_smul_index, at the wrapper type: a scalar pushes into a Finsupp.sum.