The permutation module of a G-set is the permutation representation

A monoid G acting on a type X acts on the finitely supported functions X →₀ R by pushing the support forward (Finsupp.comapDistribMulAction), and that action is R-linear (TauCeti.comapSMulCommClass), so X →₀ R is a representation of G over R. It is the permutation representation Representation.ofMulAction R G X on R[X], read through the coefficient identification MonoidAlgebra.coeffLinearEquiv (TauCeti.ofDistribMulActionComapEquiv).

This is the bridge between the two forms a permutation module comes in. The unbundled form — an additive monoid carrying a DistribMulAction — is the form a G-module convention asks for, and the form in which a permutation lattice ℤ[X] = X →₀ ℤ is tensored with a ring along its canonical ℤ-module structure; the bundled Representation.ofMulAction is the form the representation-theory API is stated in.

Neither Finsupp.comapDistribMulAction nor TauCeti.comapSMulCommClass is a global instance: the first would conflict with the coefficientwise action, and the second is stated for it. A consumer installs both with attribute [local instance], the way Mathlib/Data/Finsupp/SMul.lean states its own lemmas about the action.

Main declarations

• TauCeti.comapSMulCommClass: pushing the support forward commutes with the coefficientwise scalars.
• TauCeti.ofDistribMulActionComapEquiv: the permutation module X →₀ R is the permutation representation R[X].

theorem TauCeti.comapSMulCommClass {G : Type u_2} [Monoid G] {X : Type u_3} [MulAction G X] {S : Type u_4} {M : Type u_5} [AddCommMonoid M] [DistribSMul S M] : SMulCommClass G S (X →₀ M)

Pushing the support forward commutes with the coefficientwise scalars, for any distributive scalar action on the coefficients. For X →₀ R over a commutative semiring R, this is what makes the permutation module, with the action of Finsupp.comapDistribMulAction, a representation of G over R. Like that action it is not a global instance; a consumer who wants Representation.ofDistribMulAction installs both with attribute [local instance].

noncomputable def TauCeti.ofDistribMulActionComapEquiv (R : Type u_1) (G : Type u_2) [Monoid G] (X : Type u_3) [MulAction G X] [CommSemiring R] : (Representation.ofDistribMulAction R G (X →₀ R)).Equiv (Representation.ofMulAction R G X)

The permutation module on a G-set is the permutation representation. The G-module X →₀ R, whose action pushes the support forward (Finsupp.comapDistribMulAction), is Representation.ofMulAction R G X read through the coefficients: this is the bridge between the unbundled DistribMulAction form of a permutation module and the bundled representation.

Equations

• TauCeti.ofDistribMulActionComapEquiv R G X = Representation.Equiv.mk (MonoidAlgebra.coeffLinearEquiv R).symm ⋯

@[simp]

theorem TauCeti.ofDistribMulActionComapEquiv_single {R : Type u_1} (G : Type u_2) [Monoid G] {X : Type u_3} [MulAction G X] [CommSemiring R] (x : X) (r : R) : (ofDistribMulActionComapEquiv R G X) (Finsupp.single x r) = MonoidAlgebra.single x r

TauCeti.ofDistribMulActionComapEquiv is the identification of coefficients.

@[simp]

theorem TauCeti.ofDistribMulActionComapEquiv_symm_single {R : Type u_1} (G : Type u_2) [Monoid G] {X : Type u_3} [MulAction G X] [CommSemiring R] (x : X) (r : R) : (ofDistribMulActionComapEquiv R G X).symm (MonoidAlgebra.single x r) = Finsupp.single x r

TauCeti.ofDistribMulActionComapEquiv reads a coefficient back off R[X].