Isotypic modules and isotypic components

Main definitions

• IsIsotypicOfType R M S means that all simple submodules of the R-module M are isomorphic to S. Such a module M is isomorphic to a finsupp over S, see IsIsotypicOfType.linearEquiv_finsupp.

• IsIsotypic R M means that all simple submodules of the R-module M are isomorphic to each other.

• isotypicComponent R M S is the sum of all submodules of M isomorphic to S.

• isotypicComponents R M is the set of all nontrivial isotypic components of M (where S is taken to be simple submodules).

• Submodule.IsFullyInvariant N means that the submodule N of an R-module M is mapped into itself by all endomorphisms of M. The fullyInvariantSubmodules of M form a complete lattice, which is atomic if M is semisimple, in which case the atoms are the isotypic components of M. A fully invariant submodule of a semiring as a module over itself is simply a two-sided ideal, see isFullyInvariant_iff_isTwoSided.

• iSupIndep.ringEquiv, iSupIndep.algEquiv: if M is the direct sum of fully invariant submodules Nᵢ, then End R M is isomorphic to Πᵢ End R Nᵢ. This can be applied to the isotypic components of a semisimple module M, yielding IsSemisimpleModule.endAlgEquiv.

Keywords

isotypic component, fully invariant submodule

def IsIsotypicOfType (R : Type u_2) (M : Type u) (S : Type u_4) [Ring R] [AddCommGroup M] [AddCommGroup S] [Module R M] [Module R S] : Prop

An R-module M is isotypic of type S if all simple submodules of M are isomorphic to S. If M is semisimple, it is equivalent to requiring that all simple quotients of M are isomorphic to S.

def IsIsotypic (R : Type u_2) (M : Type u) [Ring R] [AddCommGroup M] [Module R M] : Prop

An R-module M is isotypic if all its simple submodules are isomorphic.

theorem IsIsotypicOfType.isIsotypic {R : Type u_2} {M : Type u} {S : Type u_4} [Ring R] [AddCommGroup M] [AddCommGroup S] [Module R M] [Module R S] (h : IsIsotypicOfType R M S) : IsIsotypic R M

theorem IsIsotypicOfType.of_subsingleton (R : Type u_2) (M : Type u) (S : Type u_4) [Ring R] [AddCommGroup M] [AddCommGroup S] [Module R M] [Module R S] [Subsingleton M] : IsIsotypicOfType R M S

theorem IsIsotypic.of_subsingleton (R : Type u_2) (M : Type u) [Ring R] [AddCommGroup M] [Module R M] [Subsingleton M] : IsIsotypic R M

theorem IsIsotypicOfType.of_isSimpleModule (R : Type u_2) (M : Type u) [Ring R] [AddCommGroup M] [Module R M] [IsSimpleModule R M] : IsIsotypicOfType R M M

theorem IsIsotypicOfType.of_linearEquiv_type {R : Type u_2} {M : Type u} {N : Type u_3} {S : Type u_4} [Ring R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup S] [Module R M] [Module R N] [Module R S] (h : IsIsotypicOfType R M S) (e : S ≃ₗ[R] N) : IsIsotypicOfType R M N

theorem IsIsotypicOfType.of_injective {R : Type u_2} {M : Type u} {N : Type u_3} {S : Type u_4} [Ring R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup S] [Module R M] [Module R N] [Module R S] (h : IsIsotypicOfType R N S) (f : M →ₗ[R] N) (inj : Function.Injective ⇑f) : IsIsotypicOfType R M S

theorem IsIsotypic.of_injective {R : Type u_2} {M : Type u} {N : Type u_3} [Ring R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (h : IsIsotypic R N) (f : M →ₗ[R] N) (inj : Function.Injective ⇑f) : IsIsotypic R M

theorem LinearEquiv.isIsotypicOfType_iff {R : Type u_2} {M : Type u} {N : Type u_3} {S : Type u_4} [Ring R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup S] [Module R M] [Module R N] [Module R S] (e : M ≃ₗ[R] N) : IsIsotypicOfType R M S ↔ IsIsotypicOfType R N S

theorem LinearEquiv.isIsotypicOfType_iff_type {R : Type u_2} {M : Type u} {N : Type u_3} {S : Type u_4} [Ring R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup S] [Module R M] [Module R N] [Module R S] (e : N ≃ₗ[R] S) : IsIsotypicOfType R M N ↔ IsIsotypicOfType R M S

theorem LinearEquiv.isIsotypic_iff {R : Type u_2} {M : Type u} {N : Type u_3} [Ring R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (e : M ≃ₗ[R] N) : IsIsotypic R M ↔ IsIsotypic R N

theorem isIsotypicOfType_submodule_iff {R : Type u_2} {M : Type u} {S : Type u_4} [Ring R] [AddCommGroup M] [AddCommGroup S] [Module R M] [Module R S] {N : Submodule R M} : IsIsotypicOfType R (↥N) S ↔ ∀ m ≤ N, ∀ [IsSimpleModule R ↥m], Nonempty (↥m ≃ₗ[R] S)

theorem isIsotypic_submodule_iff {R : Type u_2} {M : Type u} [Ring R] [AddCommGroup M] [Module R M] {N : Submodule R M} : IsIsotypic R ↥N ↔ ∀ m ≤ N, ∀ [IsSimpleModule R ↥m], IsIsotypicOfType R ↥N ↥m

theorem IsIsotypicOfType.linearEquiv_finsupp {R : Type u_2} {M : Type u} {S : Type u_4} [Ring R] [AddCommGroup M] [AddCommGroup S] [Module R M] [Module R S] [IsSemisimpleModule R M] (h : IsIsotypicOfType R M S) : ∃ (ι : Type u), Nonempty (M ≃ₗ[R] ι →₀ S)

theorem IsIsotypic.linearEquiv_finsupp {R : Type u_2} {M : Type u} [Ring R] [AddCommGroup M] [Module R M] [IsSemisimpleModule R M] [Nontrivial M] (h : IsIsotypic R M) : ∃ (ι : Type u) (_ : Nonempty ι) (S : Submodule R M), IsSimpleModule R ↥S ∧ Nonempty (M ≃ₗ[R] ι →₀ ↥S)

theorem IsIsotypicOfType.linearEquiv_fun {R : Type u_2} {M : Type u} {S : Type u_4} [Ring R] [AddCommGroup M] [AddCommGroup S] [Module R M] [Module R S] [IsSemisimpleModule R M] [Module.Finite R M] (h : IsIsotypicOfType R M S) : ∃ (n : ℕ), Nonempty (M ≃ₗ[R] Fin n → S)

theorem IsIsotypic.linearEquiv_fun {R : Type u_2} {M : Type u} [Ring R] [AddCommGroup M] [Module R M] [IsSemisimpleModule R M] [Module.Finite R M] [Nontrivial M] (h : IsIsotypic R M) : ∃ (n : ℕ) (_ : NeZero n) (S : Submodule R M), IsSimpleModule R ↥S ∧ Nonempty (M ≃ₗ[R] Fin n → ↥S)

theorem IsIsotypic.submodule_linearEquiv_fun {R : Type u_2} {M : Type u} [Ring R] [AddCommGroup M] [Module R M] [IsSemisimpleModule R M] {m : Submodule R M} [Module.Finite R ↥m] [Nontrivial ↥m] (h : IsIsotypic R ↥m) : ∃ (n : ℕ) (_ : NeZero n), ∃ S ≤ m, IsSimpleModule R ↥S ∧ Nonempty (↥m ≃ₗ[R] Fin n → ↥S)

def isotypicComponent (R : Type u_2) (M : Type u) (S : Type u_4) [Ring R] [AddCommGroup M] [AddCommGroup S] [Module R M] [Module R S] : Submodule R M

If S is a simple R-module, the S-isotypic component in an R-module M is the sum of all submodules of M isomorphic to S.

def isotypicComponents (R : Type u_2) (M : Type u) [Ring R] [AddCommGroup M] [Module R M] : Set (Submodule R M)

The set of all (nontrivial) isotypic components of a module.

theorem Submodule.le_isotypicComponent {R : Type u_2} {M : Type u} [Ring R] [AddCommGroup M] [Module R M] (m : Submodule R M) : m ≤ isotypicComponent R M ↥m

theorem bot_lt_isotypicComponent {R : Type u_2} {M : Type u} [Ring R] [AddCommGroup M] [Module R M] (S : Submodule R M) [IsSimpleModule R ↥S] : ⊥ < isotypicComponent R M ↥S

theorem bot_lt_isotypicComponents {R : Type u_2} {M : Type u} [Ring R] [AddCommGroup M] [Module R M] {m : Submodule R M} (h : m ∈ isotypicComponents R M) : ⊥ < m

instance instNontrivialSubtypeMemSubmoduleValSetIsotypicComponents {R : Type u_2} {M : Type u} [Ring R] [AddCommGroup M] [Module R M] (c : ↑(isotypicComponents R M)) : Nontrivial ↥↑c

instance instIsSemisimpleModuleSubtypeMemSubmoduleIsotypicComponent {R : Type u_2} {M : Type u} (S : Type u_4) [Ring R] [AddCommGroup M] [AddCommGroup S] [Module R M] [Module R S] [IsSemisimpleModule R S] : IsSemisimpleModule R ↥(isotypicComponent R M S)

instance instIsSemisimpleModuleSubtypeMemSubmoduleValSetIsotypicComponents {R : Type u_2} {M : Type u} [Ring R] [AddCommGroup M] [Module R M] (c : ↑(isotypicComponents R M)) : IsSemisimpleModule R ↥↑c

theorem LinearEquiv.isotypicComponent_eq {R : Type u_2} {M : Type u} {N : Type u_3} {S : Type u_4} [Ring R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup S] [Module R M] [Module R N] [Module R S] (e : N ≃ₗ[R] S) : isotypicComponent R M N = isotypicComponent R M S

theorem Submodule.le_linearEquiv_of_sSup_eq_top {R : Type u_2} {M : Type u} [Ring R] [AddCommGroup M] [Module R M] (N : Submodule R M) [IsSimpleModule R ↥N] (s : Set (Submodule R M)) [IsSemisimpleModule R M] (hs : sSup s = ⊤) : ∃ m ∈ s, ∃ S ≤ m, Nonempty (↥N ≃ₗ[R] ↥S)

theorem Submodule.linearEquiv_of_sSup_eq_top {R : Type u_2} {M : Type u} [Ring R] [AddCommGroup M] [Module R M] (N : Submodule R M) [IsSimpleModule R ↥N] (s : Set (Submodule R M)) [h : ∀ (m : ↑s), IsSimpleModule R ↥↑m] (hs : sSup s = ⊤) : ∃ S ∈ s, Nonempty (↥N ≃ₗ[R] ↥S)

theorem Submodule.le_linearEquiv_of_le_sSup {R : Type u_2} {M : Type u} [Ring R] [AddCommGroup M] [Module R M] (N : Submodule R M) [IsSimpleModule R ↥N] (s : Set (Submodule R M)) [hs : ∀ (m : ↑s), IsSemisimpleModule R ↥↑m] (hN : N ≤ sSup s) : ∃ m ∈ s, ∃ S ≤ m, Nonempty (↥N ≃ₗ[R] ↥S)

If a simple module is contained in a sum of semisimple modules, it must be isomorphic to a submodule of one of the summands.

theorem Submodule.linearEquiv_of_le_sSup {R : Type u_2} {M : Type u} [Ring R] [AddCommGroup M] [Module R M] (N : Submodule R M) [IsSimpleModule R ↥N] (s : Set (Submodule R M)) [simple : ∀ (m : ↑s), IsSimpleModule R ↥↑m] (hs : N ≤ sSup s) : ∃ S ∈ s, Nonempty (↥N ≃ₗ[R] ↥S)

theorem instIsSimpleModuleSubtypeMemSubmoduleValSetSetOfNonemptyLinearEquivId (R : Type u_2) (M : Type u) (S : Type u_4) [Ring R] [AddCommGroup M] [AddCommGroup S] [Module R M] [Module R S] [IsSimpleModule R S] (m : ↑{m : Submodule R M | Nonempty (↥m ≃ₗ[R] S)}) : IsSimpleModule R ↥↑m

theorem IsIsotypicOfType.isotypicComponent (R : Type u_2) (M : Type u) (S : Type u_4) [Ring R] [AddCommGroup M] [AddCommGroup S] [Module R M] [Module R S] [IsSimpleModule R S] : IsIsotypicOfType R (↥(isotypicComponent R M S)) S

theorem IsIsotypic.isotypicComponent (R : Type u_2) (M : Type u) (S : Type u_4) [Ring R] [AddCommGroup M] [AddCommGroup S] [Module R M] [Module R S] [IsSimpleModule R S] : IsIsotypic R ↥(isotypicComponent R M S)

theorem IsIsotypic.isotypicComponents {R : Type u_2} {M : Type u} [Ring R] [AddCommGroup M] [Module R M] {m : Submodule R M} (h : m ∈ isotypicComponents R M) : IsIsotypic R ↥m

theorem eq_isotypicComponent_of_le {R : Type u_2} {M : Type u} [Ring R] [AddCommGroup M] [Module R M] {S c : Submodule R M} (hc : c ∈ isotypicComponents R M) [IsSimpleModule R ↥S] (le : S ≤ c) : c = isotypicComponent R M ↥S

theorem sSupIndep_isotypicComponents (R : Type u_2) (M : Type u) [Ring R] [AddCommGroup M] [Module R M] : sSupIndep (isotypicComponents R M)

instance instFiniteElemSubmoduleIsotypicComponentsOfIsNoetherian (R : Type u_2) (M : Type u) [Ring R] [AddCommGroup M] [Module R M] [IsNoetherian R M] : Finite ↑(isotypicComponents R M)

theorem IsIsotypicOfType.of_isotypicComponent_eq_top {R : Type u_2} {M : Type u} {S : Type u_4} [Ring R] [AddCommGroup M] [AddCommGroup S] [Module R M] [Module R S] [IsSimpleModule R S] (h : isotypicComponent R M S = ⊤) : IsIsotypicOfType R M S

theorem Submodule.map_le_isotypicComponent {R : Type u_2} {M : Type u} {N : Type u_3} [Ring R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (S : Submodule R M) [IsSimpleModule R ↥S] (f : M →ₗ[R] N) : map f S ≤ isotypicComponent R N ↥S

theorem LinearMap.le_comap_isotypicComponent {R : Type u_2} {M : Type u} {N : Type u_3} (S : Type u_4) [Ring R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup S] [Module R M] [Module R N] [Module R S] [IsSimpleModule R S] (f : M →ₗ[R] N) : isotypicComponent R M S ≤ Submodule.comap f (isotypicComponent R N S)

def Submodule.IsFullyInvariant {R : Type u_5} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (N : Submodule R M) : Prop

A submodule N an R-module M is fully invariant if N is mapped into itself by all R-linear endomorphisms of M.

If M is semisimple, this is equivalent to N being a sum of isotypic components of M: see isFullyInvariant_iff_sSup_isotypicComponents.

theorem isFullyInvariant_iff_isTwoSided {R : Type u_5} [Semiring R] {I : Ideal R} : Submodule.IsFullyInvariant I ↔ I.IsTwoSided

def fullyInvariantSubmodule (R : Type u_5) (M : Type u_6) [Semiring R] [AddCommMonoid M] [Module R M] : CompleteSublattice (Submodule R M)

The fully invariant submodules of a module form a complete sublattice in the lattice of submodules.

theorem mem_fullyInvariantSubmodule_iff {R : Type u_5} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] {m : Submodule R M} : m ∈ fullyInvariantSubmodule R M ↔ m.IsFullyInvariant

noncomputable def iSupIndep.ringEquiv {R : Type u_2} {M : Type u} [Ring R] [AddCommGroup M] [Module R M] {ι : Type u_5} [DecidableEq ι] {N : ι → Submodule R M} (ind : iSupIndep N) (iSup_top : ⨆ (i : ι), N i = ⊤) (invar : ∀ (i : ι), (N i).IsFullyInvariant) : Module.End R M ≃+* ((i : ι) → Module.End R ↥(N i))

If an R-module M is the direct sum of fully invariant submodules Nᵢ, then End R M is isomorphic to Πᵢ End R Nᵢ as a ring.

noncomputable def iSupIndep.algEquiv (R₀ : Type u_1) {R : Type u_2} {M : Type u} [CommSemiring R₀] [Ring R] [Algebra R₀ R] [AddCommGroup M] [Module R M] {ι : Type u_5} [DecidableEq ι] {N : ι → Submodule R M} (ind : iSupIndep N) (iSup_top : ⨆ (i : ι), N i = ⊤) (invar : ∀ (i : ι), (N i).IsFullyInvariant) [Module R₀ M] [IsScalarTower R₀ R M] : Module.End R M ≃ₐ[R₀] (i : ι) → Module.End R ↥(N i)

If an R-module M is the direct sum of fully invariant submodules Nᵢ, then End R M is isomorphic to Πᵢ End R Nᵢ as an algebra.

theorem Submodule.IsFullyInvariant.isotypicComponent (R : Type u_2) (M : Type u) (S : Type u_4) [Ring R] [AddCommGroup M] [AddCommGroup S] [Module R M] [Module R S] [IsSimpleModule R S] : (isotypicComponent R M S).IsFullyInvariant

theorem Submodule.IsFullyInvariant.of_mem_isotypicComponents {R : Type u_2} {M : Type u} [Ring R] [AddCommGroup M] [Module R M] {m : Submodule R M} (h : m ∈ isotypicComponents R M) : m.IsFullyInvariant

def GaloisCoinsertion.setIsotypicComponents (R : Type u_2) (M : Type u) [Ring R] [AddCommGroup M] [Module R M] : GaloisCoinsertion (fun (s : Set ↑(isotypicComponents R M)) => ⨆ c ∈ s, ⟨↑c, ⋯⟩) fun (m : ↥(fullyInvariantSubmodule R M)) => {c : ↑(isotypicComponents R M) | ↑c ≤ ↑m}

The Galois coinsertion from sets of isotypic components to fully invariant submodules.

theorem le_isotypicComponent_iff {R : Type u_2} {M : Type u} {S : Type u_4} [Ring R] [AddCommGroup M] [AddCommGroup S] [Module R M] [Module R S] [IsSimpleModule R S] [IsSemisimpleModule R M] {m : Submodule R M} : m ≤ isotypicComponent R M S ↔ IsIsotypicOfType R (↥m) S

theorem isotypicComponent_eq_top_iff {R : Type u_2} {M : Type u} {S : Type u_4} [Ring R] [AddCommGroup M] [AddCommGroup S] [Module R M] [Module R S] [IsSimpleModule R S] [IsSemisimpleModule R M] : isotypicComponent R M S = ⊤ ↔ IsIsotypicOfType R M S

theorem isFullyInvariant_iff_le_imp_isotypicComponent_le {R : Type u_2} {M : Type u} [Ring R] [AddCommGroup M] [Module R M] [IsSemisimpleModule R M] {m : Submodule R M} : m.IsFullyInvariant ↔ ∀ S ≤ m, ∀ [IsSimpleModule R ↥S], isotypicComponent R M ↥S ≤ m

theorem eq_isotypicComponent_iff {R : Type u_2} {M : Type u} {S : Type u_4} [Ring R] [AddCommGroup M] [AddCommGroup S] [Module R M] [Module R S] [IsSimpleModule R S] [IsSemisimpleModule R M] {m : Submodule R M} (ne : m ≠ ⊥) : m = isotypicComponent R M S ↔ IsIsotypicOfType R (↥m) S ∧ m.IsFullyInvariant

theorem isIsotypic_iff_isFullyInvariant_imp_bot_or_top {R : Type u_2} {M : Type u} [Ring R] [AddCommGroup M] [Module R M] [IsSemisimpleModule R M] : IsIsotypic R M ↔ ∀ (N : Submodule R M), N.IsFullyInvariant → N = ⊥ ∨ N = ⊤

theorem mem_isotypicComponents_iff {R : Type u_2} {M : Type u} [Ring R] [AddCommGroup M] [Module R M] [IsSemisimpleModule R M] {m : Submodule R M} : m ∈ isotypicComponents R M ↔ IsIsotypic R ↥m ∧ m.IsFullyInvariant ∧ m ≠ ⊥

def OrderIso.setIsotypicComponents {R : Type u_2} {M : Type u} [Ring R] [AddCommGroup M] [Module R M] [IsSemisimpleModule R M] : Set ↑(isotypicComponents R M) ≃o ↥(fullyInvariantSubmodule R M)

Sets of isotypic components in a semisimple module are in order-preserving 1-1 correspondence with fully invariant submodules. Consequently, the fully invariant submodules form a complete atomic Boolean algebra.

@[simp]

theorem OrderIso.setIsotypicComponents_symm_apply {R : Type u_2} {M : Type u} [Ring R] [AddCommGroup M] [Module R M] [IsSemisimpleModule R M] (m : ↥(fullyInvariantSubmodule R M)) : (RelIso.symm setIsotypicComponents) m = {c : ↑(isotypicComponents R M) | ↑c ≤ ↑m}

@[simp]

theorem OrderIso.setIsotypicComponents_apply {R : Type u_2} {M : Type u} [Ring R] [AddCommGroup M] [Module R M] [IsSemisimpleModule R M] (s : Set ↑(isotypicComponents R M)) : setIsotypicComponents s = ⨆ c ∈ s, ⟨↑c, ⋯⟩

theorem isFullyInvariant_iff_sSup_isotypicComponents {R : Type u_2} {M : Type u} [Ring R] [AddCommGroup M] [Module R M] [IsSemisimpleModule R M] {m : Submodule R M} : m.IsFullyInvariant ↔ ∃ s ⊆ isotypicComponents R M, m = sSup s

theorem sSup_isotypicComponents (R : Type u_2) (M : Type u) [Ring R] [AddCommGroup M] [Module R M] [IsSemisimpleModule R M] : sSup (isotypicComponents R M) = ⊤

noncomputable def IsSemisimpleModule.endAlgEquiv (R₀ : Type u_1) (R : Type u_2) (M : Type u) [CommSemiring R₀] [Ring R] [Algebra R₀ R] [AddCommGroup M] [Module R M] [IsSemisimpleModule R M] [Module R₀ M] [IsScalarTower R₀ R M] [DecidableEq ↑(isotypicComponents R M)] : Module.End R M ≃ₐ[R₀] (c : ↑(isotypicComponents R M)) → Module.End R ↥↑c

The endomorphism algebra of a semisimple module is the direct product of the endomorphism algebras of its isotypic components.

noncomputable def IsSemisimpleModule.endRingEquiv (R : Type u_2) (M : Type u) [Ring R] [AddCommGroup M] [Module R M] [IsSemisimpleModule R M] [DecidableEq ↑(isotypicComponents R M)] : Module.End R M ≃+* ((c : ↑(isotypicComponents R M)) → Module.End R ↥↑c)

The endomorphism ring of a semisimple module is the direct product of the endomorphism rings of its isotypic components.