Multiplicativity of a linear extension is a basis-level condition

A Z-linear map out of the Hecke ring is determined by its values on the basis elements single Z D 1, one for each double coset. The same is true of its multiplicativity: F (x * y) = F x * F y for all x and y follows from the special case where both arguments are basis elements, and likewise for the reversed identity F (x * y) = F y * F x.

The reversed identity

The Hecke ring acts on modular forms through the slash, which is a right action, while Module.End multiplies by composition; that is what motivates recording the reversed order alongside the plain one, so a consumer whose basis identity comes out reversed — as HeckeRing.GL2.twistedHeckeSlashRingCharLinearMap_mul_single_single does — need not route through MulOpposite itself. Both live in the LinearMap namespace, so a consumer writes F.map_mul_of_basis.

Main results

• LinearMap.map_mul_of_basis: a linear map that is multiplicative on basis elements is multiplicative.
• LinearMap.map_mul_reverse_of_basis: the same with the factors on the right-hand side in the opposite order.

References

• G. Shimura, Introduction to the arithmetic theory of automorphic functions, §3.1 (the Hecke ring as a free module on the double cosets).

theorem LinearMap.map_mul_of_basis {G : Type u_1} [Group G] {Δ : Submonoid G} {H : Subgroup G} [IsHeckeTriple Δ H H] {Z : Type u_2} [Semiring Z] {A : Type u_3} [NonUnitalNonAssocSemiring A] [Module Z A] [IsScalarTower Z A A] [SMulCommClass Z A A] (F : HeckeRing Δ H Z →ₗ[Z] A) (h : ∀ (D₁ D₂ : HeckeCoset Δ H H), F (HeckeCosetModule.single Z D₁ 1 * HeckeCosetModule.single Z D₂ 1) = F (HeckeCosetModule.single Z D₁ 1) * F (HeckeCosetModule.single Z D₂ 1)) (x y : HeckeRing Δ H Z) : F (x * y) = F x * F y

Multiplicativity is a basis-level condition. A Z-linear map out of the Hecke ring that is multiplicative on the basis elements HeckeCosetModule.single Z D 1 is multiplicative.

theorem LinearMap.map_mul_reverse_of_basis {G : Type u_1} [Group G] {Δ : Submonoid G} {H : Subgroup G} [IsHeckeTriple Δ H H] {Z : Type u_2} [Semiring Z] {A : Type u_3} [NonUnitalNonAssocSemiring A] [Module Z A] [IsScalarTower Z A A] [SMulCommClass Z A A] (F : HeckeRing Δ H Z →ₗ[Z] A) (h : ∀ (D₁ D₂ : HeckeCoset Δ H H), F (HeckeCosetModule.single Z D₁ 1 * HeckeCosetModule.single Z D₂ 1) = F (HeckeCosetModule.single Z D₂ 1) * F (HeckeCosetModule.single Z D₁ 1)) (x y : HeckeRing Δ H Z) : F (x * y) = F y * F x

Anti-multiplicativity is a basis-level condition. A Z-linear map out of the Hecke ring that sends a product of basis elements to the product of their images in the opposite order does so on all of the ring.

This is the order a right action produces, so it is the shape a slash-derived extension arrives in.