Isotypic components of the regular module as an invariant of abstract simple modules

Mathlib's isotypicComponent R N S is the sum of all submodules of N isomorphic to S, and isotypicComponents R N is the set of its nontrivial values as S ranges over the simple submodules of N. For N = R the latter is a set of left ideals, and it is what indexes the Artin-Wedderburn decomposition of a semisimple ring. Calling those indices the isomorphism classes of simple R-modules is a theorem, not a rename: an abstract simple module carries no relation to R beyond its action.

Mathlib supplies the input, IsSemisimpleRing.exists_linearEquiv_ideal_of_isSimpleModule: every simple module over a semisimple ring is isomorphic to a left ideal, necessarily a minimal one. This file turns that realization into the statement that M ↦ isotypicComponent R R M, which Mathlib already defines for an abstract M, is a complete isomorphism invariant of simple modules whose values are exactly isotypicComponents R R.

Main results

• TauCeti.le_isotypicComponent_iff_nonempty_linearEquiv: a simple submodule lies in the S-isotypic component exactly when it is a copy of the simple module S. The isotypic component therefore sees no simple module other than S; this holds in any ambient module, with no hypothesis on the ring.
• TauCeti.isotypicComponent_eq_iff: the block ⇆ simple-module dictionary. Two simple modules over a semisimple ring cut out the same isotypic component of R if and only if they are isomorphic — the injectivity half.
• TauCeti.isotypicComponent_mem_isotypicComponents: the isotypic component cut out by an abstract simple module is one of the isotypic components of the regular module, so the map above is well defined into isotypicComponents R R. Surjectivity needs no lemma: by definition every element of isotypicComponents R R is isotypicComponent R R I for a simple left ideal I.
• TauCeti.simpleSubmoduleClassesEquiv: the bijection. The isomorphism classes of simple submodules of M, as the quotient type TauCeti.SimpleSubmoduleClasses R M, correspond to the isotypic components of M, the class of N going to the N-isotypic component. This needs no hypothesis on the ring; for M = R it is the bijection with the Artin-Wedderburn blocks.
• TauCeti.simpleModuleClass: over a semisimple ring, the class in SimpleSubmoduleClasses R R of the simple left ideals realizing an abstract simple module. Its fibres are the isomorphism classes (TauCeti.simpleModuleClass_eq_iff) and it hits every class (TauCeti.simpleModuleClass_coe), so SimpleSubmoduleClasses R R is a universe-safe type of isomorphism classes of simple R-modules.
• TauCeti.finite_of_pairwise_not_linearEquiv: a semisimple ring has only finitely many isomorphism classes of simple modules.

Implementation notes

Isomorphism classes of abstract simple modules cannot be a type: they range over every universe. They are therefore handled in two ways here. The relational lemmas TauCeti.isotypicComponent_eq_iff and TauCeti.isotypicComponent_mem_isotypicComponents state injectivity and well-definedness of M ↦ isotypicComponent R R M without naming a type of classes at all. The bundled bijection instead uses TauCeti.SimpleSubmoduleClasses R R, the classes of simple left ideals, which is a type in Type u; over a semisimple ring TauCeti.simpleModuleClass identifies it with the classes of abstract simple modules. It is used through TauCeti.SimpleSubmoduleClasses.mk, TauCeti.SimpleSubmoduleClasses.mk_eq_mk_iff and the eliminators TauCeti.SimpleSubmoduleClasses.lift (into Sort, with its defining equation TauCeti.SimpleSubmoduleClasses.lift_mk) and TauCeti.SimpleSubmoduleClasses.ind (into Prop), which is a complete API: nothing downstream has to know it is a quotient.

Each proof over a semisimple ring realizes the abstract module as a left ideal and transports along that realization; nothing here redoes the isotypic theory.

This implements the isomorphism-class bijection of Layer 1.5 of the semisimple algebras roadmap. See T. Y. Lam, A First Course in Noncommutative Rings, GTM 131, §3, and C. W. Curtis and I. Reiner, Representation Theory of Finite Groups and Associative Algebras, §25.

theorem TauCeti.le_isotypicComponent_iff_nonempty_linearEquiv {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {S : Type w} [AddCommGroup S] [Module R S] [IsSimpleModule R S] (N : Submodule R M) [IsSimpleModule R ↥N] : N ≤ isotypicComponent R M S ↔ Nonempty (S ≃ₗ[R] ↥N)

A simple submodule lies in the S-isotypic component of M exactly when it is a copy of the simple module S. Unlike Mathlib's Submodule.le_isotypicComponent, the module S cutting out the component is an arbitrary simple R-module rather than a submodule of M.

def TauCeti.SimpleSubmoduleClasses (R : Type u) [Ring R] (M : Type v) [AddCommGroup M] [Module R M] : Type v

The isomorphism classes of simple submodules of M. Unlike the isomorphism classes of abstract simple modules, which range over every universe, this is a type; over a semisimple ring the two agree for M = R, by TauCeti.simpleModuleClass.

That this is a quotient of the simple submodules by linear isomorphism is an implementation detail: build a class with TauCeti.SimpleSubmoduleClasses.mk, compare classes with TauCeti.SimpleSubmoduleClasses.mk_eq_mk_iff, and eliminate with TauCeti.SimpleSubmoduleClasses.lift into Sort or TauCeti.SimpleSubmoduleClasses.ind into Prop. The bodies stay unexposed: the defining equations TauCeti.SimpleSubmoduleClasses.lift_mk and TauCeti.coe_simpleSubmoduleClassesEquiv_mk are stated as ordinary theorems, so nothing downstream depends on the quotient by definitional unfolding.

Equations

• TauCeti.SimpleSubmoduleClasses R M = Quot fun (N N' : { N : Submodule R M // IsSimpleModule R ↥N }) => Nonempty (↥↑N ≃ₗ[R] ↥↑N')

def TauCeti.SimpleSubmoduleClasses.mk {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] (N : Submodule R M) [IsSimpleModule R ↥N] : SimpleSubmoduleClasses R M

The isomorphism class of a simple submodule of M.

Equations

• TauCeti.SimpleSubmoduleClasses.mk N = Quot.mk (fun (N N' : { N : Submodule R M // IsSimpleModule R ↥N }) => Nonempty (↥↑N ≃ₗ[R] ↥↑N')) ⟨N, inst✝⟩

theorem TauCeti.SimpleSubmoduleClasses.mk_eq_mk_iff {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {N N' : Submodule R M} [IsSimpleModule R ↥N] [IsSimpleModule R ↥N'] : mk N = mk N' ↔ Nonempty (↥N ≃ₗ[R] ↥N')

theorem TauCeti.SimpleSubmoduleClasses.ind {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {motive : SimpleSubmoduleClasses R M → Prop} (mk : ∀ (N : Submodule R M) (x : IsSimpleModule R ↥N), motive (mk N)) (c : SimpleSubmoduleClasses R M) : motive c

Every isomorphism class is the class of a simple submodule: the eliminator into Prop.

def TauCeti.SimpleSubmoduleClasses.lift {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {α : Sort u_1} (f : (N : Submodule R M) → [IsSimpleModule R ↥N] → α) (hf : ∀ (N N' : Submodule R M) [inst : IsSimpleModule R ↥N] [inst_1 : IsSimpleModule R ↥N'], Nonempty (↥N ≃ₗ[R] ↥N') → f N = f N') (c : SimpleSubmoduleClasses R M) : α

The eliminator into Sort. To define data on the isomorphism classes of simple submodules of M it suffices to give a value on each simple submodule and to check that isomorphic simple submodules get the same value; the value on a class is then read off by TauCeti.SimpleSubmoduleClasses.lift_mk.

Equations

• TauCeti.SimpleSubmoduleClasses.lift f hf c = Quot.lift (fun (N : { N : Submodule R M // IsSimpleModule R ↥N }) => f ↑N) ⋯ c

@[simp]

theorem TauCeti.SimpleSubmoduleClasses.lift_mk {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {α : Sort u_1} {f : (N : Submodule R M) → [IsSimpleModule R ↥N] → α} {hf : ∀ (N N' : Submodule R M) [inst : IsSimpleModule R ↥N] [inst_1 : IsSimpleModule R ↥N'], Nonempty (↥N ≃ₗ[R] ↥N') → f N = f N'} (N : Submodule R M) [IsSimpleModule R ↥N] : lift f hf (mk N) = f N

The defining equation of TauCeti.SimpleSubmoduleClasses.lift.

noncomputable def TauCeti.simpleSubmoduleClassesEquiv (R : Type u) [Ring R] (M : Type v) [AddCommGroup M] [Module R M] : SimpleSubmoduleClasses R M ≃ ↑(isotypicComponents R M)

Isomorphism classes of simple submodules biject with isotypic components. The class of a simple submodule N of M corresponds to the N-isotypic component of M.

Injectivity is TauCeti.le_isotypicComponent_iff_nonempty_linearEquiv: a simple submodule of an isotypic component is a copy of the module cutting it out. Surjectivity is the definition of isotypicComponents.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.coe_simpleSubmoduleClassesEquiv_mk {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] (N : Submodule R M) [IsSimpleModule R ↥N] : ↑((simpleSubmoduleClassesEquiv R M) (SimpleSubmoduleClasses.mk N)) = isotypicComponent R M ↥N

theorem TauCeti.isotypicComponent_mem_isotypicComponents (R : Type u) [Ring R] (M : Type v) [AddCommGroup M] [Module R M] [IsSemisimpleRing R] [IsSimpleModule R M] : isotypicComponent R R M ∈ isotypicComponents R R

Over a semisimple ring, the isotypic component of the regular module cut out by an abstract simple module really is one of the isotypic components of R, which are indexed by the simple left ideals.

theorem TauCeti.isotypicComponent_eq_iff {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsSemisimpleRing R] {N : Type w} [AddCommGroup N] [Module R N] [IsSimpleModule R M] [IsSimpleModule R N] : isotypicComponent R R M = isotypicComponent R R N ↔ Nonempty (M ≃ₗ[R] N)

The isotypic component of the regular module is a complete isomorphism invariant of a simple module. Over a semisimple ring, two simple modules cut out the same isotypic component of R if and only if they are isomorphic.

Together with TauCeti.isotypicComponent_mem_isotypicComponents and the fact that every element of isotypicComponents R R is by definition an isotypic component of a simple left ideal, this is the bijection between isomorphism classes of simple R-modules and the isotypic components of R; the latter index the blocks of an Artin-Wedderburn decomposition.

noncomputable def TauCeti.simpleModuleClass (R : Type u) [Ring R] (M : Type v) [AddCommGroup M] [Module R M] [IsSemisimpleRing R] [IsSimpleModule R M] : SimpleSubmoduleClasses R R

Over a semisimple ring, the isomorphism class of the simple left ideals realizing an abstract simple module M; see TauCeti.simpleModuleClass_eq_mk_iff.

Equations

• TauCeti.simpleModuleClass R M = (TauCeti.simpleSubmoduleClassesEquiv R R).symm ⟨isotypicComponent R R M, ⋯⟩

@[simp]

theorem TauCeti.coe_simpleSubmoduleClassesEquiv_simpleModuleClass {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsSemisimpleRing R] [IsSimpleModule R M] : ↑((simpleSubmoduleClassesEquiv R R) (simpleModuleClass R M)) = isotypicComponent R R M

theorem TauCeti.simpleModuleClass_eq_mk_iff {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsSemisimpleRing R] [IsSimpleModule R M] (I : Submodule R R) [IsSimpleModule R ↥I] : simpleModuleClass R M = SimpleSubmoduleClasses.mk I ↔ Nonempty (M ≃ₗ[R] ↥I)

The class of an abstract simple module is the class of a simple left ideal exactly when the two are isomorphic, which is what makes TauCeti.simpleModuleClass a realization of M.

theorem TauCeti.simpleModuleClass_coe {R : Type u} [Ring R] [IsSemisimpleRing R] (I : Submodule R R) [IsSimpleModule R ↥I] : simpleModuleClass R ↥I = SimpleSubmoduleClasses.mk I

Every isomorphism class of simple left ideals is the class of an abstract simple module, namely of the ideal itself: TauCeti.simpleModuleClass is surjective.

theorem TauCeti.simpleModuleClass_eq_iff {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsSemisimpleRing R] {N : Type w} [AddCommGroup N] [Module R N] [IsSimpleModule R M] [IsSimpleModule R N] : simpleModuleClass R M = simpleModuleClass R N ↔ Nonempty (M ≃ₗ[R] N)

The dictionary as a map to a type of classes. Over a semisimple ring, two simple modules have the same class of realizing left ideals if and only if they are isomorphic.

With TauCeti.simpleModuleClass_coe this says that SimpleSubmoduleClasses R R, which TauCeti.simpleSubmoduleClassesEquiv identifies with the isotypic components of R, is a type of isomorphism classes of simple R-modules.

theorem TauCeti.finite_of_pairwise_not_linearEquiv {R : Type u} [Ring R] [IsSemisimpleRing R] {ι : Type u_1} (S : ι → Type v) [(i : ι) → AddCommGroup (S i)] [(i : ι) → Module R (S i)] [∀ (i : ι), IsSimpleModule R (S i)] (h : ∀ (i j : ι), Nonempty (S i ≃ₗ[R] S j) → i = j) : Finite ι

A semisimple ring has only finitely many isomorphism classes of simple modules: a family of pairwise non-isomorphic simple R-modules is indexed by a finite type, because isotypicComponent R R embeds it into the finite set isotypicComponents R R.