Hecke Rings: Associativity #
The IsScalarTower instance proving that the module action is compatible with multiplication,
which is equivalent to associativity of multiplication in the Hecke ring. This is Shimura
Proposition 3.4.
theorem
HeckeRing.heckeMultiplicity_uniform
{G : Type u_1}
[Group G]
(P : HeckePair G)
(g₂ g₁ : ↥P.Δ)
(D : HeckeCoset P)
(q₀ : decompQuot P D.rep)
:
Uniform distribution of multiplicities: the count of coset pairs (i,j) mapping
to a given left coset q₀H within double coset D is independent of the choice of q₀
(Shimura Proposition 3.4).
instance
HeckeRing.instIsScalarTower
{G : Type u_1}
[Group G]
(P : HeckePair G)
:
IsScalarTower (𝕋 P ℤ) (𝕋 P ℤ) (HeckeModule P ℤ)
The module action satisfies the scalar tower property (x * y) • z = y • (x • z),
which is equivalent to associativity of multiplication (Shimura Proposition 3.4).