The monoid-algebra action of a representation

General facts about Representation.asAlgebraHom, the extension of a representation ρ of a monoid G to the monoid algebra k[G].

The first is the description of the image of a monoid-algebra lift: since k[G] is spanned by G, its image is, as a submodule, the span of the image of the defining monoid homomorphism (MonoidAlgebra.toSubmodule_range_lift). For a representation this identifies both the submodule and the subalgebra generated by its image. This is what turns a statement about a monoid action into a statement about the subalgebra of endomorphisms it generates, as a double-centralizer theorem needs.

The second is a vanishing criterion. An element a of the monoid algebra k[G] acting through a representation ρ kills a vector v when three conditions meet: doubling is injective on V, some g fixes v, and right multiplication by g negates a. The last two make ρ.asAlgebraHom a v its own negative, and injective doubling turns being its own negative into vanishing.

That is the mechanism behind the column-antisymmetrizer vanishing arguments of TauCeti/RepresentationTheory/Symmetric/, which are its consumers: the antisymmetrizer of a set of indices absorbs each permutation of those indices up to its sign, so against a vector fixed by an odd such permutation the two conditions hold and the action is zero.

Nothing here is specific to symmetric groups or to ℚ. G is a monoid, and the module and the scalars are arbitrary; nothing is asked of 2 in k at all: the hypothesis is that doubling is injective on V, taken as an explicit assumption rather than read off the scalars. So this covers torsion-free modules over ℤ, where 2 is not a unit, and equally modules over a ring with zero divisors whose additive group has no 2-torsion.

Main results

• MonoidAlgebra.toSubmodule_range_lift: the image of a monoid-algebra lift is the span of the image of its defining monoid homomorphism.
• Representation.range_asAlgebraHom_eq_adjoin: the image of a representation's monoid-algebra action is the algebra generated by the representation.
• Representation.mem_centralizer_range_asAlgebraHom_iff: centralizing the monoid-algebra image is equivalent to commuting with every element of the monoid action.
• Representation.commute_asAlgebraHom_of_forall_commute: commuting with the monoid action propagates to the action of the monoid algebra.
• Representation.asAlgebraHom_eq_zero_of_mul_single_eq_neg: with doubling injective on V, an algebra element negated by right multiplication by an element fixing v annihilates v.

theorem MonoidAlgebra.toSubmodule_range_lift {k : Type u_1} {G : Type u_2} {A : Type u_3} [CommSemiring k] [Monoid G] [Semiring A] [Algebra k A] (F : G →* A) : Subalgebra.toSubmodule ((lift k A G) F).range = Submodule.span k (Set.range ⇑F)

The image of a monoid-algebra lift is the span of the image of the monoid homomorphism. The monoid algebra k[G] is spanned by the elements of G, so an element of its image is a finite k-combination of the elements F g, and conversely every F g lies in the image.

theorem Representation.toSubmodule_range_asAlgebraHom {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) : Subalgebra.toSubmodule ρ.asAlgebraHom.range = Submodule.span k (Set.range ⇑ρ)

The image of a representation's monoid-algebra action is the span of the representation.

theorem Representation.range_asAlgebraHom_eq_adjoin {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) : ρ.asAlgebraHom.range = Algebra.adjoin k (Set.range ⇑ρ)

The image of a representation's monoid-algebra action is the algebra generated by the representation.

theorem Representation.commute_asAlgebraHom_of_forall_commute {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) {x : Module.End k V} (h : ∀ (g : G), Commute x (ρ g)) (a : MonoidAlgebra k G) : Commute x (ρ.asAlgebraHom a)

If an endomorphism commutes with every operator in a representation, then it commutes with the action of every element of the monoid algebra.

theorem Representation.mem_centralizer_range_asAlgebraHom_iff {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) {x : Module.End k V} : x ∈ Subalgebra.centralizer k (Set.range ⇑ρ.asAlgebraHom) ↔ ∀ (g : G), Commute x (ρ g)

An endomorphism centralizes the image of a representation's monoid-algebra action exactly when it commutes with every operator in the representation.

theorem Representation.asAlgebraHom_eq_zero_of_mul_single_eq_neg {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommRing k] [Monoid G] [AddCommGroup V] [Module k V] (h2inj : Function.Injective fun (w : V) => 2 • w) (ρ : Representation k G V) {a : MonoidAlgebra k G} {g : G} {v : V} (hfix : (ρ g) v = v) (hneg : a * MonoidAlgebra.single g 1 = -a) : (ρ.asAlgebraHom a) v = 0

An algebra element absorbed by a fixing element, up to sign, annihilates the vector. If doubling is injective on V, g fixes v, and right multiplication by single g 1 negates a, then a acts as zero on v.