Isotypic modules and isotypic components

def IsIsotypicOfType (R : Type u_1) (M : Type u) (S : Type u_3) [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.

Equations

• IsIsotypicOfType R M S = ∀ (m : Submodule R M) [IsSimpleModule R ↥m], Nonempty (↥m ≃ₗ[R] S)

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

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

Equations

• IsIsotypic R M = ∀ (m : Submodule R M) [IsSimpleModule R ↥m], IsIsotypicOfType R M ↥m

theorem IsIsotypicOfType.isIsotypic {R : Type u_1} {M : Type u} {S : Type u_3} [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_1) (M : Type u) (S : Type u_3) [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_1) (M : Type u) [Ring R] [AddCommGroup M] [Module R M] [Subsingleton M] : IsIsotypic R M

theorem IsIsotypicOfType.of_isSimpleModule (R : Type u_1) (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_1} {M : Type u} {N : Type u_2} {S : Type u_3} [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_1} {M : Type u} {N : Type u_2} {S : Type u_3} [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_1} {M : Type u} {N : Type u_2} [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_1} {M : Type u} {N : Type u_2} {S : Type u_3} [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_1} {M : Type u} {N : Type u_2} {S : Type u_3} [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_1} {M : Type u} {N : Type u_2} [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_1} {M : Type u} {S : Type u_3} [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_1} {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_1} {M : Type u} {S : Type u_3} [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_1} {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_1} {M : Type u} {S : Type u_3} [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_1} {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)

def Submodule.IsFullyInvariant {R : Type u_1} {M : Type u} [Ring R] [AddCommGroup 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.

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

Equations

• N.IsFullyInvariant = ∀ (f : Module.End R M), N ≤ Submodule.comap f N

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

def isotypicComponent (R : Type u_1) (M : Type u) (S : Type u_3) [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.

Equations

• isotypicComponent R M S = sSup {m : Submodule R M | Nonempty (↥m ≃ₗ[R] S)}

theorem Submodule.le_isotypicComponent (R : Type u_1) (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_1) (M : Type u) [Ring R] [AddCommGroup M] [Module R M] (S : Submodule R M) [IsSimpleModule R ↥S] : ⊥ < isotypicComponent R M ↥S

instance instIsSemisimpleModuleSubtypeMemSubmoduleIsotypicComponent (R : Type u_1) (M : Type u) (S : Type u_3) [Ring R] [AddCommGroup M] [AddCommGroup S] [Module R M] [Module R S] [IsSemisimpleModule R S] : IsSemisimpleModule R ↥(isotypicComponent R M S)

theorem Submodule.le_linearEquiv_of_sSup_eq_top {R : Type u_1} {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_1} {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_1} {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_1} {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_1) (M : Type u) (S : Type u_3) [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_1) (M : Type u) (S : Type u_3) [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_1) (M : Type u) (S : Type u_3) [Ring R] [AddCommGroup M] [AddCommGroup S] [Module R M] [Module R S] [IsSimpleModule R S] : IsIsotypic R ↥(isotypicComponent R M S)

theorem IsIsotypicOfType.of_isotypicComponent_eq_top {R : Type u_1} {M : Type u} {S : Type u_3} [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 isotypicComponent_eq_top_iff {R : Type u_1} {M : Type u} {S : Type u_3} [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_isotypicComponent (R : Type u_1) (M : Type u) (S : Type u_3) [Ring R] [AddCommGroup M] [AddCommGroup S] [Module R M] [Module R S] [IsSimpleModule R S] : (isotypicComponent R M S).IsFullyInvariant

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