The coinvariant kernel of representations

Let k be a commutative ring and ρ a k-linear representation of a monoid G. The coinvariant kernel Representation.Coinvariants.ker ρ is the submodule spanned by the elements ρ g v - v. This file records its functoriality and describes it through the augmentation ideal, orbit sums and generators.

Under ρ.asModuleEquiv, the coinvariant kernel is the augmentation ideal times the associated monoid-algebra module ρ.asModule. This identifies the representation-theoretic and module-theoretic descriptions of the augmentation submodule over any commutative ring.

Precomposing with a monoid homomorphism shrinks the augmentation submodule; surjective precomposition leaves it unchanged. An action-compatible linear map carries the augmentation submodule into that of its target, even when the function between acting monoids is not a homomorphism.

• For the permutation representation k[X] of a group action on a type X, it is the kernel of the orbit-sum map k[X] → k[X ⧸ G], which sums the coefficients of an element along each G-orbit.
• For an arbitrary representation of a group generated by a set s, it is the sum of the ranges of ρ g - 1 for g ∈ s. In particular, if G is generated by a single element g it is the range of ρ g - 1; unlike Representation.FiniteCyclicGroup.coinvariantsKer_eq_range, no finiteness of G is needed.
• For an arbitrary representation of a finite monoid, it is the set of sums ∑ g, (ρ g (y g) - y g) with one term for each monoid element.

Combining the first two gives, for any action of a group G on X and any g : G, a criterion for membership in the range of ρ g - 1 on k[X]: an element lies in it if and only if its coefficients sum to zero along every orbit of the cyclic subgroup generated by g.

For a finite group and any semiring k, the orbit sums of the norm ∑ g, g • v of v ∈ k[X] are |G| times those of v. Over a commutative ring, when multiplication by |G| is injective on k, an element of norm zero has vanishing orbit sums and lies in the coinvariant kernel: the degree -1 Tate cohomology of a permutation module vanishes.

Finally, if a finset s ⊆ X meets every G-orbit in exactly one point, then for r : k the element ∑ x ∈ s, single x r has every orbit sum equal to r.

Main results

• Representation.coinvariantsKer_eq_map_ker_augmentation_smul_top: the coinvariant kernel is the augmentation ideal times ρ.asModule, transported along ρ.asModuleEquiv.
• Representation.coinvariantsKer_map_le: an action-compatible linear map carries the augmentation submodule into that of its target.
• Representation.coinvariantsKer_comp_le: precomposition with a monoid homomorphism shrinks the augmentation submodule.
• Representation.coinvariantsKer_comp_of_surjective: surjective precomposition preserves the augmentation submodule.
• Representation.coinvariantsKer_ofMulAction_eq_ker: the coinvariant kernel of the permutation representation k[X] is the kernel of the orbit-sum map k[X] → k[X ⧸ G].
• MonoidAlgebra.mapDomainLinearMap_orbitRel_mk_norm_ofMulAction: over a semiring, the orbit sums of the norm of v : k[X] are |G| times those of v.
• Representation.ker_norm_ofMulAction_le_coinvariantsKer: if multiplication by |G| is injective on k, the kernel of the norm of k[X] lies in the coinvariant kernel.
• Representation.coinvariantsKer_eq_iSup_range: if s generates G, the coinvariant kernel is ⨆ g ∈ s, range (ρ g - 1).
• Representation.coinvariantsKer_eq_range_of_forall_mem_zpowers: if g generates G, the coinvariant kernel is range (ρ g - 1).
• Representation.mem_coinvariantsKer_iff_exists_sum: for finite G, the coinvariant kernel is the set of sums ∑ g, (ρ g (y g) - y g).
• Representation.mem_range_ofMulAction_sub_id_iff: an element of k[X] lies in the range of ρ g - 1 if and only if its coefficient sums along the orbits of ⟨g⟩ vanish.
• MonoidAlgebra.coeff_mapDomainLinearMap_orbitRel_sum_single: the orbit sums of ∑ x ∈ s, single x r are all equal to r when the finset s is a set of orbit representatives.

Implementation notes

As in Mathlib's Representation.FiniteCyclicGroup.coinvariantsKer_eq_range, the operator ρ g - 1 is written ρ g - LinearMap.id. The orbit-sum map is MonoidAlgebra.mapDomainLinearMap k k (Quotient.mk (MulAction.orbitRel G X)). Its kernel lies in the coinvariant kernel by Representation.sub_mapDomainLinearMap_mem_coinvariantsKer, applied to the map Quotient.out ∘ Quotient.mk _ that sends each point of X to a chosen representative of its orbit. A set s of orbit representatives is described by the two hypotheses ∀ x, ∃ g : G, g • x ∈ s (every orbit meets s) and ∀ x ∈ s, ∀ g : G, g • x ∈ s → g • x = x (every orbit meets s at most once).

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 motivating application is the period relation (A) of §1; in §3 an element ζ of the permutation module ℚ[ℳ] is shown to lie in (1 - T) ℚ[ℳ] if and only if its coefficients sum to zero along every T-orbit.

The augmentation ideal description

@[simp]

theorem Representation.Coinvariants.mk_asAlgebraHom {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommRing k] [Monoid G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) (r : MonoidAlgebra k G) (v : V) : (mk ρ) ((ρ.asAlgebraHom r) v) = (TauCeti.MonoidAlgebra.augmentation k G) r • (mk ρ) v

On coinvariants, the monoid-algebra action is scalar multiplication by augmentation.

theorem Representation.coinvariantsKer_eq_map_ker_augmentation_smul_top {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommRing k] [Monoid G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) : Coinvariants.ker ρ = Submodule.map (↑ρ.asModuleEquiv) (Submodule.restrictScalars k (RingHom.ker (TauCeti.MonoidAlgebra.augmentation k G) • ⊤))

The coinvariant kernel is the augmentation ideal times the associated monoid-algebra module, transported back to the representation by asModuleEquiv.

theorem Representation.mem_coinvariantsKer_iff_mem_ker_augmentation_smul_top {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommRing k] [Monoid G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) {v : V} : v ∈ Coinvariants.ker ρ ↔ ρ.asModuleEquiv.symm v ∈ RingHom.ker (TauCeti.MonoidAlgebra.augmentation k G) • ⊤

An element belongs to the coinvariant kernel exactly when its associated-module image lies in the augmentation ideal times the module.

Change of representation and acting monoid

theorem Representation.coinvariantsKer_map_le {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommRing k] [Monoid G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) {K : Type u_4} {G' : Type u_5} {V' : Type u_6} [CommRing K] [SMul k K] [Monoid G'] [AddCommGroup V'] [Module k V'] [Module K V'] [IsScalarTower k K V'] {ρ' : Representation K G' V'} (e : G → G') (φ : V →ₗ[k] V') (hφ : ∀ (g : G) (x : V), φ ((ρ g) x) = (ρ' (e g)) (φ x)) : Submodule.map φ (Coinvariants.ker ρ) ≤ Submodule.restrictScalars k (Coinvariants.ker ρ')

An intertwining linear map carries the augmentation submodule into the augmentation submodule over a compatible scalar tower. The scalar action on K need not come from an algebra structure, and the function e between acting monoids need not be a homomorphism.

theorem Representation.coinvariantsKer_comp_le {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommRing k] [Monoid G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) {G' : Type u_4} [Monoid G'] (ψ : G' →* G) : Coinvariants.ker (MonoidHom.comp ρ ψ) ≤ Coinvariants.ker ρ

Restricting a representation along a monoid homomorphism shrinks its augmentation submodule.

@[simp]

theorem Representation.coinvariantsKer_comp_of_surjective {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommRing k] [Monoid G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) {G' : Type u_4} [Monoid G'] (ψ : G' →* G) (hψ : Function.Surjective ⇑ψ) : Coinvariants.ker (MonoidHom.comp ρ ψ) = Coinvariants.ker ρ

Precomposing a representation with a surjective monoid homomorphism does not change its augmentation submodule.

Orbit sums are invariant

@[simp]

theorem Representation.mapDomainLinearMap_orbitRel_mk_ofMulAction {k : Type u_1} {G : Type u_2} {X : Type u_3} [Semiring k] [Group G] [MulAction G X] (g : G) (v : MonoidAlgebra k X) : (MonoidAlgebra.mapDomainLinearMap k k (Quotient.mk (MulAction.orbitRel G X))) (((ofMulAction k G X) g) v) = (MonoidAlgebra.mapDomainLinearMap k k (Quotient.mk (MulAction.orbitRel G X))) v

The orbit-sum map k[X] → k[X ⧸ G] is invariant under the permutation representation.

@[simp]

theorem MonoidAlgebra.mapDomainLinearMap_orbitRel_mk_norm_ofMulAction {k : Type u_1} {G : Type u_2} {X : Type u_3} [Semiring k] [Group G] [Fintype G] [MulAction G X] (v : MonoidAlgebra k X) : (mapDomainLinearMap k k (Quotient.mk (MulAction.orbitRel G X))) ((Representation.ofMulAction k G X).norm v) = Fintype.card G • (mapDomainLinearMap k k (Quotient.mk (MulAction.orbitRel G X))) v

The orbit sums of the norm ∑ g, g • v of v : k[X] are |G| times those of v.

The coinvariant kernel of a permutation representation

theorem Representation.sub_mapDomainLinearMap_mem_coinvariantsKer {k : Type u_1} {G : Type u_2} {X : Type u_3} [CommRing k] [Monoid G] [MulAction G X] {f : X → X} (hf : ∀ (x : X), ∃ (g : G), g • f x = x) (v : MonoidAlgebra k X) : v - (MonoidAlgebra.mapDomainLinearMap k k f) v ∈ Coinvariants.ker (ofMulAction k G X)

If every x : X lies in the G-orbit of f x, then v minus its pushforward along f lies in the coinvariant kernel of the permutation representation k[X].

theorem Representation.coinvariantsKer_ofMulAction_eq_ker {k : Type u_1} {G : Type u_2} {X : Type u_3} [CommRing k] [Group G] [MulAction G X] : Coinvariants.ker (ofMulAction k G X) = (MonoidAlgebra.mapDomainLinearMap k k (Quotient.mk (MulAction.orbitRel G X))).ker

The coinvariant kernel of a permutation representation. An element of k[X] lies in the coinvariant kernel of the permutation representation if and only if its coefficients sum to zero along every G-orbit.

theorem Representation.ker_norm_ofMulAction_le_coinvariantsKer {k : Type u_1} {G : Type u_2} {X : Type u_3} [CommRing k] [Group G] [Fintype G] [MulAction G X] (hk : IsSMulRegular k (Fintype.card G)) : LinearMap.ker (ofMulAction k G X).norm ≤ Coinvariants.ker (ofMulAction k G X)

If multiplication by |G| is injective on the coefficient ring, an element of the permutation representation k[X] of a finite group G with vanishing norm lies in the coinvariant kernel: its orbit sums are killed by |G|, hence vanish.

The coinvariant kernel of a representation of a generated group

theorem Representation.coinvariantsKer_eq_iSup_range {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommRing k] [Group G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) {s : Set G} (hs : Subgroup.closure s = ⊤) : Coinvariants.ker ρ = ⨆ g ∈ s, (ρ g - LinearMap.id).range

If s generates G, the coinvariant kernel of ρ is the sum of the ranges of ρ g - 1 for g ∈ s.

theorem Representation.coinvariantsKer_eq_range_of_forall_mem_zpowers {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommRing k] [Group G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) : Coinvariants.ker ρ = (ρ g - LinearMap.id).range

If g generates G, the coinvariant kernel of ρ is the range of ρ g - 1. Unlike Representation.FiniteCyclicGroup.coinvariantsKer_eq_range, G need not be finite.

The coinvariant kernel of a representation of a finite monoid

theorem Representation.mem_coinvariantsKer_iff_exists_sum {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommRing k] [Monoid G] [Fintype G] [AddCommGroup V] [Module k V] {ρ : Representation k G V} {x : V} : x ∈ Coinvariants.ker ρ ↔ ∃ (y : G → V), ∑ g : G, ((ρ g) (y g) - y g) = x

For a finite monoid G, the coinvariant kernel of ρ consists of the sums ∑ g, (ρ g (y g) - y g), with one term for each monoid element.

Orbit sums

theorem Representation.mem_range_ofMulAction_sub_id_iff {k : Type u_1} {G : Type u_2} {X : Type u_3} [CommRing k] [Group G] [MulAction G X] (g : G) {v : MonoidAlgebra k X} : v ∈ ((ofMulAction k G X) g - LinearMap.id).range ↔ (MonoidAlgebra.mapDomainLinearMap k k (Quotient.mk (MulAction.orbitRel (↥(Subgroup.zpowers g)) X))) v = 0

Membership in the range of ρ g - 1 via orbit sums. For the permutation representation k[X], an element lies in the range of ρ g - 1 if and only if its coefficients sum to zero along every orbit of the cyclic subgroup generated by g.

theorem MonoidAlgebra.coeff_mapDomainLinearMap_orbitRel_sum_single {k : Type u_1} {G : Type u_2} {X : Type u_3} [Semiring k] [Group G] [MulAction G X] {s : Finset X} (hex : ∀ (x : X), ∃ (g : G), g • x ∈ s) (hfix : ∀ x ∈ s, ∀ (g : G), g • x ∈ s → g • x = x) (r : k) (q : MulAction.orbitRel.Quotient G X) : ((mapDomainLinearMap k k (Quotient.mk (MulAction.orbitRel G X))) (∑ x ∈ s, single x r)).coeff q = r

If a finset s meets every G-orbit exactly once, then the element ∑ x ∈ s, single x r of k[X] has all its orbit sums equal to r.