Intertwining maps out of, and the character of, the left ideal of a quasi-idempotent

Let σ be a representation of a monoid G on V over a commutative semiring k, and let a be an element of the monoid algebra k[G] that is quasi-idempotent: a * a = κ • a for a unit κ of k. The left ideal k[G] a is a representation of G by left multiplication, and this file identifies the intertwining maps out of it:

Hom_G(k[G] a, V) ≃ₗ[k] a V, by f ↦ f a,

where a V is the image of a acting on V through σ.

This identifies the intertwiner space with a subspace of V itself, the image of a. In a split semisimple setting, when k[G] a is irreducible, this intertwiner space is its multiplicity space in V. The identification is natural in V (Representation.spanSingletonHomEquivRange_comp), so any operator on V commuting with G acts compatibly on both sides.

Allowing a scalar κ rather than asking for an idempotent is what the applications need: the Young symmetrizer c_t satisfies c_t * c_t = κ • c_t with κ = n! / dim (k[Sₙ] c_t), and it is c_t itself, not its normalization, whose image cuts out the Weyl module.

Both directions are elementary. The monoid-algebra linear map corresponding to an intertwining map commutes with the whole of k[G], so its value on an element r a of the ideal is r applied to its value at a, which therefore determines it; and that value lies in a V because a = κ⁻¹ a a. Conversely a vector a v of a V defines the intertwining map x ↦ κ⁻¹ x (a v), which sends a to κ⁻¹ a a v = a v.

For a finite group over a field the character of k[G] a is read off from the coefficients of a (Representation.mul_char_ofModule'_span_singleton):

κ * χ(g) = ∑ σ, a_{σ⁻¹ g⁻¹ σ}.

Right multiplication by a maps k[G] into the ideal and acts on it as κ, so composing it with left multiplication by g gives an endomorphism of k[G] whose trace is κ * χ(g) (TauCeti.LinearMap.trace_mul_eq_mul_trace_restrict_range); the right-hand side is the same trace computed in the basis of group elements.

Main definitions

• Representation.spanSingletonHomEquivRange: the dictionary Hom_G(k[G] a, V) ≃ₗ[k] a V, evaluation at the generator a.

Main results

• Representation.coe_spanSingletonHomEquivRange_apply: the dictionary evaluates at the generator.
• Representation.spanSingletonHomEquivRange_symm_apply_smul_generator: its inverse sends a vector of a V to the intertwining map taking r a to r applied to that vector.
• Representation.spanSingletonHomEquivRange_comp: naturality in the target.
• Representation.mul_char_ofModule'_span_singleton: the character of k[G] a, multiplied by κ, is a sum of coefficients of a over the conjugates of g⁻¹.

References

• I. Assem, D. Simson, A. Skowroński, Elements of the Representation Theory of Associative Algebras, Vol. 1, Section I.4, for the idempotent case Hom_A(Ae, M) ≅ eM.
• W. Fulton and J. Harris, Representation Theory: A First Course (1991), Lecture 6, where the quasi-idempotent Young symmetrizers are the case that matters.

noncomputable def Representation.spanSingletonHomEquivRange {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) {a : MonoidAlgebra k G} {κ : k} (hκ : IsUnit κ) (ha : a * a = κ • a) : (ofModule' ↥(Ideal.span {a})).IntertwiningMap σ ≃ₗ[k] ↥(LinearMap.range (σ.asAlgebraHom a))

Intertwining maps out of the left ideal of a quasi-idempotent. If a * a = κ • a with κ a unit, evaluation at the generator identifies the intertwining maps from k[G] a to V with the image of a acting on V.

@[simp]

theorem Representation.coe_spanSingletonHomEquivRange_apply {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) {a : MonoidAlgebra k G} {κ : k} (hκ : IsUnit κ) (ha : a * a = κ • a) (f : (ofModule' ↥(Ideal.span {a})).IntertwiningMap σ) : ↑((σ.spanSingletonHomEquivRange hκ ha) f) = f (TauCeti.spanSingletonGenerator a)

The dictionary evaluates an intertwining map at the generator a.

theorem Representation.spanSingletonHomEquivRange_symm_apply_smul_generator {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) {a : MonoidAlgebra k G} {κ : k} (hκ : IsUnit κ) (ha : a * a = κ • a) (w : ↥(LinearMap.range (σ.asAlgebraHom a))) (r : MonoidAlgebra k G) : ((σ.spanSingletonHomEquivRange hκ ha).symm w) (r • TauCeti.spanSingletonGenerator a) = (σ.asAlgebraHom r) ↑w

The intertwining map attached to a vector w of a V sends r a to r w.

@[simp]

theorem Representation.spanSingletonHomEquivRange_symm_apply_generator {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) {a : MonoidAlgebra k G} {κ : k} (hκ : IsUnit κ) (ha : a * a = κ • a) (w : ↥(LinearMap.range (σ.asAlgebraHom a))) : ((σ.spanSingletonHomEquivRange hκ ha).symm w) (TauCeti.spanSingletonGenerator a) = ↑w

The intertwining map attached to a vector w of a V sends the generator a to w.

theorem Representation.spanSingletonHomEquivRange_comp {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) {a : MonoidAlgebra k G} {κ : k} {W : Type u_4} [AddCommMonoid W] [Module k W] {τ : Representation k G W} (hκ : IsUnit κ) (ha : a * a = κ • a) (T : σ.IntertwiningMap τ) (f : (ofModule' ↥(Ideal.span {a})).IntertwiningMap σ) : ↑((τ.spanSingletonHomEquivRange hκ ha) (T.comp f)) = T ↑((σ.spanSingletonHomEquivRange hκ ha) f)

Naturality in the target. Composing with an intertwining map T : V → W corresponds, on the images of a, to applying T.

The character of the left ideal

theorem Representation.mul_char_ofModule'_span_singleton {k : Type u_4} {G : Type u_5} [Field k] [Group G] [Fintype G] {a : MonoidAlgebra k G} {κ : k} (ha : a * a = κ • a) (g : G) : κ * (ofModule' ↥(Ideal.span {a})).character g = ∑ σ : G, a.coeff (σ⁻¹ * g⁻¹ * σ)

The character of the left ideal of a quasi-idempotent. If a * a = κ • a, then κ times the character of k[G] a at g is ∑ σ, a_{σ⁻¹ g⁻¹ σ}, the sum of the coefficients of a over the conjugates of g⁻¹, each counted once for every element of G conjugating g⁻¹ to it.