Commuting permutation representations

If monoids G and H act on a type X and the two actions commute, then the permutation representations Representation.ofMulAction k G X and Representation.ofMulAction k H X on the free k-module k[X] commute with each other. For the left and right multiplication actions of a group G, that is, commuting actions of G and Gᵐᵒᵖ, this makes k[X] a k[G]-bimodule. On k[G] itself, the left regular representation Representation.ofMulAction k G G is left multiplication by the monomials single g 1. Its equivariant endomorphism corresponding to x : k[G] under Rep.leftRegularHomEquiv is right multiplication by x.

When G and H are groups, G permutes the H-orbits, and the orbit sums of k[X] along the H-orbits are equivariant: the sum of the coefficients of g • v along the H-orbit of g • x is the sum of the coefficients of v along the H-orbit of x. Hence if g fixes ∑ i ∈ s, h i • v for a family h : ι → H and #s is cancellable in k, then the H-orbit sums of v are invariant under g. The orbit sums of v are the finitely supported function v.coeff.mapDomain (Quotient.mk (MulAction.orbitRel H X)) on the orbit space.

For a finite group G, the coefficient of the norm ∑ g, g • v at x is ∑ g, v(g • x). In particular the norm of the basis vector at x has coefficient |G_x| at x and vanishes off the orbit of x, while a vector fixed by G has constant coefficients along each orbit, so it is determined by its coefficients at a set of orbit representatives. These are the inputs of the computation of the low-degree Tate cohomology of k[X].

Main results

• TauCeti.commute_ofMulAction: commuting actions on X give commuting permutation representations on k[X].
• TauCeti.single_mul_eq_smul_ofMulAction: on k[G], left multiplication by a monomial single g c is c times the left regular action of g.
• Rep.leftRegularHomEquiv_symm_apply: equivariant endomorphisms of the left regular representation are right multiplications.
• TauCeti.mapDomain_orbitRel_mk_coeff_ofMulAction: the orbit sums of k[X] are invariant under the permutation representation.
• TauCeti.mapDomain_orbitRel_mk_coeff_ofMulAction_smul: for commuting actions of G and H, the H-orbit sums of g • v at g • x are those of v at x.
• TauCeti.mapDomain_orbitRel_mk_coeff_smul_of_ofMulAction_sum: if g fixes ∑ i ∈ s, h i • v and #s is cancellable, the H-orbit sums of v are g-invariant.
• TauCeti.coeff_smul_of_forall_ofMulAction_eq: a fixed vector of k[X] has the same coefficient at every point of an orbit.
• TauCeti.eq_of_coeff_out_eq_of_forall_ofMulAction_eq: two fixed vectors of k[X] agreeing at the chosen representative of every orbit are equal.
• TauCeti.coeff_norm_ofMulAction: the coefficients of the norm of a vector of k[X].
• TauCeti.coeff_norm_ofMulAction_single_self, TauCeti.coeff_norm_ofMulAction_single_of_notMem_orbit: the norm of the basis vector at x has coefficient |G_x| at x and vanishes off the orbit of x.

References

• A. Popa and D. Zagier, An elementary proof of the Eichler–Selberg trace formula, J. Reine Angew. Math. 762 (2020), 105–122, arXiv:1711.00327. The right coset sums ⟨ξ, K⟩ of §3 Theorem 2(a) are the orbit sums for the right action of PSL(2, ℤ) on the integral matrices of positive determinant, which commutes with the left action.

theorem TauCeti.commute_ofMulAction {k : Type u_1} {G : Type u_2} {H : Type u_3} {X : Type u_4} [Semiring k] [Monoid G] [Monoid H] [MulAction G X] [MulAction H X] [SMulCommClass G H X] (g : G) (h : H) : Commute ((Representation.ofMulAction k G X) g) ((Representation.ofMulAction k H X) h)

If the actions of G and H on X commute, then so do the permutation representations of G and H on k[X].

theorem TauCeti.single_mul_eq_smul_ofMulAction {k : Type u_1} {G : Type u_2} [Semiring k] [Monoid G] (g : G) (c : k) (a : MonoidAlgebra k G) : MonoidAlgebra.single g c * a = c • ((Representation.ofMulAction k G G) g) a

On the monoid algebra k[G], left multiplication by the monomial single g c is c times the left regular representation of g.

@[simp]

theorem Rep.leftRegularHomEquiv_symm_apply {k : Type u_5} {G : Type u_6} [CommRing k] [Monoid G] (x a : MonoidAlgebra k G) : (Hom.hom ((leftRegular k G).leftRegularHomEquiv.symm x)) a = a * x

The endomorphism of the left regular representation k[G] corresponding to x under Rep.leftRegularHomEquiv is right multiplication by x.

Orbit sums

@[simp]

theorem TauCeti.mapDomain_orbitRel_mk_coeff_ofMulAction {k : Type u_1} {X : Type u_4} [Semiring k] {G : Type u_5} [Group G] [MulAction G X] (g : G) (v : MonoidAlgebra k X) : Finsupp.mapDomain (Quotient.mk (MulAction.orbitRel G X)) (((Representation.ofMulAction k G X) g) v).coeff = Finsupp.mapDomain (Quotient.mk (MulAction.orbitRel G X)) v.coeff

The orbit sums k[X] → (X ⧸ G →₀ k) are invariant under the permutation representation.

@[simp]

theorem TauCeti.mapDomain_orbitRel_mk_coeff_ofMulAction_smul {k : Type u_1} {X : Type u_4} [Semiring k] {G : Type u_5} {H : Type u_6} [Group G] [Group H] [MulAction G X] [MulAction H X] [SMulCommClass G H X] (g : G) (v : MonoidAlgebra k X) (x : X) : (Finsupp.mapDomain (Quotient.mk (MulAction.orbitRel H X)) (((Representation.ofMulAction k G X) g) v).coeff) ⟦g • x⟧ = (Finsupp.mapDomain (Quotient.mk (MulAction.orbitRel H X)) v.coeff) ⟦x⟧

Equivariance of orbit sums. If the actions of G and H on X commute, then the sum of the coefficients of g • v along the H-orbit of g • x is the sum of the coefficients of v along the H-orbit of x.

theorem TauCeti.mapDomain_orbitRel_mk_coeff_smul_of_ofMulAction_sum {k : Type u_1} {X : Type u_4} [Semiring k] {G : Type u_5} {H : Type u_6} [Group G] [Group H] [MulAction G X] [MulAction H X] [SMulCommClass G H X] {ι : Type u_7} {s : Finset ι} {h : ι → H} {g : G} {v : MonoidAlgebra k X} (hs : IsSMulRegular k s.card) (hfix : ((Representation.ofMulAction k G X) g) (∑ i ∈ s, ((Representation.ofMulAction k H X) (h i)) v) = ∑ i ∈ s, ((Representation.ofMulAction k H X) (h i)) v) (x : X) : (Finsupp.mapDomain (Quotient.mk (MulAction.orbitRel H X)) v.coeff) ⟦g • x⟧ = (Finsupp.mapDomain (Quotient.mk (MulAction.orbitRel H X)) v.coeff) ⟦x⟧

If the actions of G and H on X commute, h : ι → H, #s is cancellable in k and g • w = w for w = ∑ i ∈ s, h i • v, then the H-orbit sums of v are invariant under g: the coefficients of v have the same sum along the H-orbits of g • x and of x.

Norms and invariant vectors

theorem TauCeti.coeff_smul_of_forall_ofMulAction_eq {k : Type u_1} {X : Type u_4} [Semiring k] {G : Type u_5} [Group G] [MulAction G X] {v : MonoidAlgebra k X} (hv : ∀ (g : G), ((Representation.ofMulAction k G X) g) v = v) (g : G) (x : X) : v.coeff (g • x) = v.coeff x

A vector of k[X] fixed by the permutation representation has the same coefficient at every point of an orbit.

theorem TauCeti.eq_of_coeff_out_eq_of_forall_ofMulAction_eq {k : Type u_1} {X : Type u_4} [Semiring k] {G : Type u_5} [Group G] [MulAction G X] {v w : MonoidAlgebra k X} (hv : ∀ (g : G), ((Representation.ofMulAction k G X) g) v = v) (hw : ∀ (g : G), ((Representation.ofMulAction k G X) g) w = w) (h : ∀ (ω : MulAction.orbitRel.Quotient G X), v.coeff (Quotient.out ω) = w.coeff (Quotient.out ω)) : v = w

Two vectors of k[X] fixed by the permutation representation are equal as soon as they agree at the chosen representative of every orbit.

@[simp]

theorem TauCeti.coeff_norm_ofMulAction {k : Type u_1} {X : Type u_4} [Semiring k] {G : Type u_5} [Group G] [MulAction G X] [Fintype G] (v : MonoidAlgebra k X) (x : X) : ((Representation.ofMulAction k G X).norm v).coeff x = ∑ g : G, v.coeff (g • x)

The coefficient of the norm ∑ g, g • v of v : k[X] at x is the sum of the coefficients of v at the points g • x.

theorem TauCeti.coeff_norm_ofMulAction_single_self {k : Type u_1} {X : Type u_4} [Semiring k] {G : Type u_5} [Group G] [MulAction G X] [Fintype G] (x : X) (r : k) : ((Representation.ofMulAction k G X).norm (MonoidAlgebra.single x r)).coeff x = Nat.card ↥(MulAction.stabilizer G x) • r

The norm of single x r has coefficient |G_x| • r at x, where G_x is the stabilizer of x.

theorem TauCeti.coeff_norm_ofMulAction_single_of_notMem_orbit {k : Type u_1} {X : Type u_4} [Semiring k] {G : Type u_5} [Group G] [MulAction G X] [Fintype G] {x y : X} (h : y ∉ MulAction.orbit G x) (r : k) : ((Representation.ofMulAction k G X).norm (MonoidAlgebra.single x r)).coeff y = 0

The norm of single x r vanishes off the orbit of x.