An isotypic component is its type tensored with its multiplicity space

Let A be an algebra over a field k and let S be a simple A-module. For any A-module M the multiplicity space of S in M is the hom space S →ₗ[A] M. Its dimension deserves the name: when k is algebraically closed, S is finite-dimensional and M is a finite product of simple modules, that dimension is the number of factors of M isomorphic to S (TauCeti.finrank_linearMap_eq_natCard_of_linearEquiv_pi). Evaluation

TauCeti.isotypicEval : S ⊗[k] (S →ₗ[A] M) →ₗ[A] M, s ⊗ f ↦ f s,

is A-linear for the action on the left factor alone, and has the S-isotypic component of M as its range (TauCeti.range_isotypicEval). This file proves that it is injective, so that

S ⊗[k] (S →ₗ[A] M) ≃ₗ[A] isotypicComponent A M S.

Injectivity asks that S be simple and finite-dimensional over an algebraically closed k, and nothing at all of M.

This is the uncounted form of the isotypic decomposition. A counted form is already available — TauCeti.nonempty_linearEquiv_isotypicComponent writes the component as S ^ m with m = finrank k (S →ₗ[A] M) — but it asks M itself to be finite-dimensional over k, and it produces only an unspecified isomorphism, so it destroys any structure the multiplicity space carries. The tensor form asks nothing of M and keeps that structure: every A-linear map out of M acts on the second factor and on nothing else (TauCeti.isotypicEval_comp), which is exactly what a double-centralizer decomposition consumes.

Summing over components gives the uncounted form of the whole decomposition of a semisimple module. For pairwise non-isomorphic simple modules S j that represent every simple submodule of a semisimple M, evaluation is an isomorphism ⨁ⱼ S j ⊗[k] (S j →ₗ[A] M) ≃ₗ[A] M. Injectivity combines injectivity on each summand with the independence of the isotypic components (TauCeti.iSupIndep_isotypicComponent). Again nothing is asked of M beyond semisimplicity; in particular infinitely many S j may occur, with infinite-dimensional multiplicity spaces.

Main definitions

• TauCeti.isotypicComponentTensorEquiv: the isotypic component is S tensored with its multiplicity space, S ⊗[k] (S →ₗ[A] M) ≃ₗ[A] isotypicComponent A M S.
• TauCeti.isotypicTensorEquiv: the same for a module that is its own isotypic component, S ⊗[k] (S →ₗ[A] M) ≃ₗ[A] M.
• TauCeti.directSumIsotypicEval: the sum of the evaluation maps of a family of modules S j.
• TauCeti.directSumIsotypicTensorEquiv: the isotypic decomposition of a semisimple module, ⨁ⱼ S j ⊗[k] (S j →ₗ[A] M) ≃ₗ[A] M.

Main results

• TauCeti.isotypicEval_injective: evaluation is injective, for S simple and finite-dimensional over an algebraically closed k, with no finiteness asked of the target.
• TauCeti.isotypicComponentTensorEquiv_map_coe and TauCeti.isotypicTensorEquiv_map: naturality in the target — an A-linear map M →ₗ[A] N acts on the multiplicity space and on nothing else, read on the equivalences.
• TauCeti.isotypicTensorEquiv_symm_apply_map: the same read on the inverse — the form that, taking N = M, transports the commutant of A onto the multiplicity space.
• TauCeti.range_directSumIsotypicEval: the range of the summed evaluation is the sum of the isotypic components; TauCeti.directSumIsotypicEval_surjective and TauCeti.directSumIsotypicEval_injective give the two halves of the decomposition.
• TauCeti.directSumIsotypicEval_comp, TauCeti.directSumIsotypicTensorEquiv_map and TauCeti.directSumIsotypicTensorEquiv_symm_apply_map: naturality of the decomposition in the target, so that A-linear maps act on the multiplicity spaces alone.

References

• C. W. Curtis and I. Reiner, Representation Theory of Finite Groups and Associative Algebras, §25.
• J.-P. Serre, Linear Representations of Finite Groups, §2.6.

Injectivity of evaluation

theorem TauCeti.isotypicEval_injective (k : Type u_1) {A : Type u_2} {S : Type u_3} {M : Type u_4} [Field k] [Ring A] [Algebra k A] [AddCommGroup S] [Module k S] [Module A S] [IsScalarTower k A S] [AddCommGroup M] [Module k M] [Module A M] [IsScalarTower k A M] [IsSimpleModule A S] [IsAlgClosed k] [FiniteDimensional k S] : Function.Injective ⇑(isotypicEval k)

Evaluation is injective. Only S is asked to be simple and finite-dimensional over the algebraically closed field k; the target M is arbitrary.

The tensor decomposition

noncomputable def TauCeti.isotypicComponentTensorEquiv (k : Type u_1) {A : Type u_2} {S : Type u_3} {M : Type u_4} [Field k] [Ring A] [Algebra k A] [AddCommGroup S] [Module k S] [Module A S] [IsScalarTower k A S] [AddCommGroup M] [Module k M] [Module A M] [IsScalarTower k A M] [IsSimpleModule A S] [IsAlgClosed k] [FiniteDimensional k S] : TensorProduct k S (S →ₗ[A] M) ≃ₗ[A] ↥(isotypicComponent A M S)

An isotypic component is its type tensored with its multiplicity space. Evaluation s ⊗ f ↦ f s is an isomorphism of A-modules from S ⊗[k] (S →ₗ[A] M) onto the S-isotypic component of M. The A-action is on the left factor only, so the multiplicity space carries whatever commutes with A.

@[simp]

theorem TauCeti.isotypicComponentTensorEquiv_apply_coe (k : Type u_1) {A : Type u_2} {S : Type u_3} {M : Type u_4} [Field k] [Ring A] [Algebra k A] [AddCommGroup S] [Module k S] [Module A S] [IsScalarTower k A S] [AddCommGroup M] [Module k M] [Module A M] [IsScalarTower k A M] [IsSimpleModule A S] [IsAlgClosed k] [FiniteDimensional k S] (x : TensorProduct k S (S →ₗ[A] M)) : ↑((isotypicComponentTensorEquiv k) x) = (isotypicEval k) x

theorem TauCeti.isotypicComponentTensorEquiv_map_coe (k : Type u_1) {A : Type u_2} {S : Type u_3} {M : Type u_4} {N : Type u_5} [Field k] [Ring A] [Algebra k A] [AddCommGroup S] [Module k S] [Module A S] [IsScalarTower k A S] [AddCommGroup M] [Module k M] [Module A M] [IsScalarTower k A M] [AddCommGroup N] [Module k N] [Module A N] [IsScalarTower k A N] [IsSimpleModule A S] [IsAlgClosed k] [FiniteDimensional k S] (g : M →ₗ[A] N) (x : TensorProduct k S (S →ₗ[A] M)) : ↑((isotypicComponentTensorEquiv k) ((TensorProduct.AlgebraTensorModule.map LinearMap.id (LinearMap.compRight k g)) x)) = g ↑((isotypicComponentTensorEquiv k) x)

The component decomposition is natural in the target. An A-linear map g : M →ₗ[A] N carries the S-isotypic component of M into that of N, and through the equivalences it is the map g induces on multiplicity spaces: it acts on the second factor and on nothing else.

noncomputable def TauCeti.isotypicTensorEquiv (k : Type u_1) {A : Type u_2} {S : Type u_3} {M : Type u_4} [Field k] [Ring A] [Algebra k A] [AddCommGroup S] [Module k S] [Module A S] [IsScalarTower k A S] [AddCommGroup M] [Module k M] [Module A M] [IsScalarTower k A M] [IsSimpleModule A S] [IsAlgClosed k] [FiniteDimensional k S] (h : isotypicComponent A M S = ⊤) : TensorProduct k S (S →ₗ[A] M) ≃ₗ[A] M

A module that is its own S-isotypic component is S tensored with its multiplicity space. For a semisimple M the hypothesis is IsIsotypicOfType A M S, through isotypicComponent_eq_top_iff.

@[simp]

theorem TauCeti.isotypicTensorEquiv_apply (k : Type u_1) {A : Type u_2} {S : Type u_3} {M : Type u_4} [Field k] [Ring A] [Algebra k A] [AddCommGroup S] [Module k S] [Module A S] [IsScalarTower k A S] [AddCommGroup M] [Module k M] [Module A M] [IsScalarTower k A M] [IsSimpleModule A S] [IsAlgClosed k] [FiniteDimensional k S] (h : isotypicComponent A M S = ⊤) (x : TensorProduct k S (S →ₗ[A] M)) : (isotypicTensorEquiv k h) x = (isotypicEval k) x

theorem TauCeti.isotypicTensorEquiv_map (k : Type u_1) {A : Type u_2} {S : Type u_3} {M : Type u_4} {N : Type u_5} [Field k] [Ring A] [Algebra k A] [AddCommGroup S] [Module k S] [Module A S] [IsScalarTower k A S] [AddCommGroup M] [Module k M] [Module A M] [IsScalarTower k A M] [AddCommGroup N] [Module k N] [Module A N] [IsScalarTower k A N] [IsSimpleModule A S] [IsAlgClosed k] [FiniteDimensional k S] (hM : isotypicComponent A M S = ⊤) (hN : isotypicComponent A N S = ⊤) (g : M →ₗ[A] N) (x : TensorProduct k S (S →ₗ[A] M)) : (isotypicTensorEquiv k hN) ((TensorProduct.AlgebraTensorModule.map LinearMap.id (LinearMap.compRight k g)) x) = g ((isotypicTensorEquiv k hM) x)

The tensor decomposition is natural in the target. For M and N both their own S-isotypic components, an A-linear map g : M →ₗ[A] N acts on the multiplicity space alone: this is TauCeti.isotypicEval_comp read through the equivalences.

@[simp]

theorem TauCeti.isotypicTensorEquiv_symm_apply_map (k : Type u_1) {A : Type u_2} {S : Type u_3} {M : Type u_4} {N : Type u_5} [Field k] [Ring A] [Algebra k A] [AddCommGroup S] [Module k S] [Module A S] [IsScalarTower k A S] [AddCommGroup M] [Module k M] [Module A M] [IsScalarTower k A M] [AddCommGroup N] [Module k N] [Module A N] [IsScalarTower k A N] [IsSimpleModule A S] [IsAlgClosed k] [FiniteDimensional k S] (hM : isotypicComponent A M S = ⊤) (hN : isotypicComponent A N S = ⊤) (g : M →ₗ[A] N) (y : M) : (isotypicTensorEquiv k hN).symm (g y) = (TensorProduct.AlgebraTensorModule.map LinearMap.id (LinearMap.compRight k g)) ((isotypicTensorEquiv k hM).symm y)

Transporting a map to the multiplicity space. Reading TauCeti.isotypicTensorEquiv_map backwards: the inverse equivalences carry an A-linear map g : M →ₗ[A] N to 1 ⊗ (g ∘ ·). For N = M this says that under the decomposition the commutant of A in Module.End k M acts on the multiplicity space and trivially on S.

The isotypic decomposition of a semisimple module

noncomputable def TauCeti.directSumIsotypicEval (k : Type u_1) (A : Type u_2) [CommSemiring k] [Semiring A] [Algebra k A] {κ : Type u_3} [DecidableEq κ] (S : κ → Type u_4) [(j : κ) → AddCommMonoid (S j)] [(j : κ) → Module k (S j)] [(j : κ) → Module A (S j)] [∀ (j : κ), IsScalarTower k A (S j)] (M : Type u_5) [AddCommMonoid M] [Module k M] [Module A M] [IsScalarTower k A M] : (Π₀ (j : κ), TensorProduct k (S j) (S j →ₗ[A] M)) →ₗ[A] M

The sum over a family of modules S j of the evaluation maps S j ⊗[k] (S j →ₗ[A] M) →ₗ[A] M, s ⊗ f ↦ f s. This construction works over semirings and needs no additive inverses.

@[simp]

theorem TauCeti.directSumIsotypicEval_single (k : Type u_1) (A : Type u_2) [CommSemiring k] [Semiring A] [Algebra k A] {κ : Type u_3} [DecidableEq κ] (S : κ → Type u_4) [(j : κ) → AddCommMonoid (S j)] [(j : κ) → Module k (S j)] [(j : κ) → Module A (S j)] [∀ (j : κ), IsScalarTower k A (S j)] (M : Type u_5) [AddCommMonoid M] [Module k M] [Module A M] [IsScalarTower k A M] (j : κ) (x : TensorProduct k (S j) (S j →ₗ[A] M)) : (directSumIsotypicEval k A S M) (DFinsupp.single j x) = (isotypicEval k) x

On the j-th summand, directSumIsotypicEval is the evaluation map of S j.

theorem TauCeti.directSumIsotypicEval_comp (k : Type u_1) {A : Type u_2} [CommSemiring k] [Semiring A] [Algebra k A] {κ : Type u_3} [DecidableEq κ] (S : κ → Type u_4) [(j : κ) → AddCommMonoid (S j)] [(j : κ) → Module k (S j)] [(j : κ) → Module A (S j)] [∀ (j : κ), IsScalarTower k A (S j)] {M : Type u_5} [AddCommMonoid M] [Module k M] [Module A M] [IsScalarTower k A M] {N : Type u_6} [AddCommMonoid N] [Module k N] [Module A N] [IsScalarTower k A N] (g : M →ₗ[A] N) : g ∘ₗ directSumIsotypicEval k A S M = directSumIsotypicEval k A S N ∘ₗ DFinsupp.mapRange.linearMap fun (j : κ) => TensorProduct.AlgebraTensorModule.map LinearMap.id (LinearMap.compRight k g)

Naturality of the summed evaluation in the target. An A-linear map g : M →ₗ[A] N acts on each summand through its multiplicity space alone; the factors S j are untouched.

theorem TauCeti.directSumIsotypicEval_map_apply (k : Type u_1) {A : Type u_2} [CommSemiring k] [Semiring A] [Algebra k A] {κ : Type u_3} [DecidableEq κ] (S : κ → Type u_4) [(j : κ) → AddCommMonoid (S j)] [(j : κ) → Module k (S j)] [(j : κ) → Module A (S j)] [∀ (j : κ), IsScalarTower k A (S j)] {M : Type u_5} [AddCommMonoid M] [Module k M] [Module A M] [IsScalarTower k A M] {N : Type u_6} [AddCommMonoid N] [Module k N] [Module A N] [IsScalarTower k A N] (g : M →ₗ[A] N) (x : Π₀ (j : κ), TensorProduct k (S j) (S j →ₗ[A] M)) : (directSumIsotypicEval k A S N) ((DFinsupp.mapRange.linearMap fun (j : κ) => TensorProduct.AlgebraTensorModule.map LinearMap.id (LinearMap.compRight k g)) x) = g ((directSumIsotypicEval k A S M) x)

The value form of TauCeti.directSumIsotypicEval_comp.

theorem TauCeti.range_directSumIsotypicEval (k : Type u_1) (A : Type u_2) [CommSemiring k] [Ring A] [Algebra k A] {κ : Type u_3} [DecidableEq κ] (S : κ → Type u_4) [(j : κ) → AddCommGroup (S j)] [(j : κ) → Module k (S j)] [(j : κ) → Module A (S j)] [∀ (j : κ), IsScalarTower k A (S j)] [∀ (j : κ), IsSimpleModule A (S j)] (M : Type u_5) [AddCommGroup M] [Module k M] [Module A M] [IsScalarTower k A M] : (directSumIsotypicEval k A S M).range = ⨆ (j : κ), isotypicComponent A M (S j)

The range of directSumIsotypicEval is the sum of the isotypic components of the S j.

theorem TauCeti.directSumIsotypicEval_surjective (k : Type u_1) {A : Type u_2} [CommSemiring k] [Ring A] [Algebra k A] {κ : Type u_3} [DecidableEq κ] (S : κ → Type u_4) [(j : κ) → AddCommGroup (S j)] [(j : κ) → Module k (S j)] [(j : κ) → Module A (S j)] [∀ (j : κ), IsScalarTower k A (S j)] {M : Type u_5} [AddCommGroup M] [Module k M] [Module A M] [IsScalarTower k A M] [IsSemisimpleModule A M] (hcover : ∀ (m : Submodule A M), IsSimpleModule A ↥m → ∃ (j : κ), Nonempty (S j ≃ₗ[A] ↥m)) : Function.Surjective ⇑(directSumIsotypicEval k A S M)

Evaluation is onto a semisimple module M as soon as each simple submodule of M is isomorphic to one of the S j. The remaining S j need not be simple.

theorem TauCeti.directSumIsotypicEval_injective (k : Type u_1) {A : Type u_2} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] {κ : Type u_3} [DecidableEq κ] (S : κ → Type u_4) [(j : κ) → AddCommGroup (S j)] [(j : κ) → Module k (S j)] [(j : κ) → Module A (S j)] [∀ (j : κ), IsScalarTower k A (S j)] [∀ (j : κ), IsSimpleModule A (S j)] [∀ (j : κ), FiniteDimensional k (S j)] {M : Type u_5} [AddCommGroup M] [Module k M] [Module A M] [IsScalarTower k A M] (hS : ∀ (i j : κ), Nonempty (S i ≃ₗ[A] S j) → i = j) : Function.Injective ⇑(directSumIsotypicEval k A S M)

For pairwise non-isomorphic simple modules S j, finite-dimensional over the algebraically closed field k, evaluation ⨁ⱼ S j ⊗[k] (S j →ₗ[A] M) → M is injective. No finiteness is asked of M.

noncomputable def TauCeti.directSumIsotypicTensorEquiv (k : Type u_1) {A : Type u_2} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] {κ : Type u_3} [DecidableEq κ] (S : κ → Type u_4) [(j : κ) → AddCommGroup (S j)] [(j : κ) → Module k (S j)] [(j : κ) → Module A (S j)] [∀ (j : κ), IsScalarTower k A (S j)] [∀ (j : κ), IsSimpleModule A (S j)] [∀ (j : κ), FiniteDimensional k (S j)] {M : Type u_5} [AddCommGroup M] [Module k M] [Module A M] [IsScalarTower k A M] [IsSemisimpleModule A M] (hS : ∀ (i j : κ), Nonempty (S i ≃ₗ[A] S j) → i = j) (hcover : ∀ (m : Submodule A M), IsSimpleModule A ↥m → ∃ (j : κ), Nonempty (S j ≃ₗ[A] ↥m)) : (Π₀ (j : κ), TensorProduct k (S j) (S j →ₗ[A] M)) ≃ₗ[A] M

The isotypic decomposition of a semisimple module. Let S j be pairwise non-isomorphic simple modules, finite-dimensional over the algebraically closed field k, such that every simple submodule of the semisimple module M is isomorphic to one of them. Then evaluation s ⊗ f ↦ f s is an isomorphism ⨁ⱼ S j ⊗[k] (S j →ₗ[A] M) ≃ M of A-modules.

@[simp]

theorem TauCeti.directSumIsotypicTensorEquiv_apply (k : Type u_1) {A : Type u_2} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] {κ : Type u_3} [DecidableEq κ] (S : κ → Type u_4) [(j : κ) → AddCommGroup (S j)] [(j : κ) → Module k (S j)] [(j : κ) → Module A (S j)] [∀ (j : κ), IsScalarTower k A (S j)] [∀ (j : κ), IsSimpleModule A (S j)] [∀ (j : κ), FiniteDimensional k (S j)] {M : Type u_5} [AddCommGroup M] [Module k M] [Module A M] [IsScalarTower k A M] [IsSemisimpleModule A M] (hS : ∀ (i j : κ), Nonempty (S i ≃ₗ[A] S j) → i = j) (hcover : ∀ (m : Submodule A M), IsSimpleModule A ↥m → ∃ (j : κ), Nonempty (S j ≃ₗ[A] ↥m)) (x : Π₀ (j : κ), TensorProduct k (S j) (S j →ₗ[A] M)) : (directSumIsotypicTensorEquiv k S hS hcover) x = (directSumIsotypicEval k A S M) x

directSumIsotypicTensorEquiv is the summed evaluation map.

theorem TauCeti.directSumIsotypicTensorEquiv_map (k : Type u_1) {A : Type u_2} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] {κ : Type u_3} [DecidableEq κ] (S : κ → Type u_4) [(j : κ) → AddCommGroup (S j)] [(j : κ) → Module k (S j)] [(j : κ) → Module A (S j)] [∀ (j : κ), IsScalarTower k A (S j)] [∀ (j : κ), IsSimpleModule A (S j)] [∀ (j : κ), FiniteDimensional k (S j)] {M : Type u_5} [AddCommGroup M] [Module k M] [Module A M] [IsScalarTower k A M] {N : Type u_6} [AddCommGroup N] [Module k N] [Module A N] [IsScalarTower k A N] [IsSemisimpleModule A M] [IsSemisimpleModule A N] (hS : ∀ (i j : κ), Nonempty (S i ≃ₗ[A] S j) → i = j) (hcoverM : ∀ (m : Submodule A M), IsSimpleModule A ↥m → ∃ (j : κ), Nonempty (S j ≃ₗ[A] ↥m)) (hcoverN : ∀ (m : Submodule A N), IsSimpleModule A ↥m → ∃ (j : κ), Nonempty (S j ≃ₗ[A] ↥m)) (g : M →ₗ[A] N) (x : Π₀ (j : κ), TensorProduct k (S j) (S j →ₗ[A] M)) : (directSumIsotypicTensorEquiv k S hS hcoverN) ((DFinsupp.mapRange.linearMap fun (j : κ) => TensorProduct.AlgebraTensorModule.map LinearMap.id (LinearMap.compRight k g)) x) = g ((directSumIsotypicTensorEquiv k S hS hcoverM) x)

The isotypic decomposition is natural in the target. An A-linear map g : M →ₗ[A] N between semisimple modules acts on each multiplicity space S j →ₗ[A] M by postcomposition, and on nothing else: this is TauCeti.directSumIsotypicEval_comp read through the equivalences.

@[simp]

theorem TauCeti.directSumIsotypicTensorEquiv_symm_apply_map (k : Type u_1) {A : Type u_2} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] {κ : Type u_3} [DecidableEq κ] (S : κ → Type u_4) [(j : κ) → AddCommGroup (S j)] [(j : κ) → Module k (S j)] [(j : κ) → Module A (S j)] [∀ (j : κ), IsScalarTower k A (S j)] [∀ (j : κ), IsSimpleModule A (S j)] [∀ (j : κ), FiniteDimensional k (S j)] {M : Type u_5} [AddCommGroup M] [Module k M] [Module A M] [IsScalarTower k A M] {N : Type u_6} [AddCommGroup N] [Module k N] [Module A N] [IsScalarTower k A N] [IsSemisimpleModule A M] [IsSemisimpleModule A N] (hS : ∀ (i j : κ), Nonempty (S i ≃ₗ[A] S j) → i = j) (hcoverM : ∀ (m : Submodule A M), IsSimpleModule A ↥m → ∃ (j : κ), Nonempty (S j ≃ₗ[A] ↥m)) (hcoverN : ∀ (m : Submodule A N), IsSimpleModule A ↥m → ∃ (j : κ), Nonempty (S j ≃ₗ[A] ↥m)) (g : M →ₗ[A] N) (y : M) : (directSumIsotypicTensorEquiv k S hS hcoverN).symm (g y) = (DFinsupp.mapRange.linearMap fun (j : κ) => TensorProduct.AlgebraTensorModule.map LinearMap.id (LinearMap.compRight k g)) ((directSumIsotypicTensorEquiv k S hS hcoverM).symm y)

Transporting a map to the multiplicity spaces. Reading TauCeti.directSumIsotypicTensorEquiv_map backwards: the inverse equivalences carry an A-linear map g : M →ₗ[A] N to 1 ⊗ (g ∘ ·) on every summand. For N = M this says that under the decomposition the commutant of A acts on the multiplicity spaces and trivially on the S j.