Comparing the isomorphism classes of simple objects with the module-level classes

A classification of representations is a bijection onto isomorphism classes, and the same group can be classified in two languages: over the isomorphism classes of simple objects of FDRep k G, which is TauCeti.SimpleFDRepClasses in TauCeti.RepresentationTheory.Simple.Basic, and over the isomorphism classes of simple k[G]-modules, which over a semisimple group algebra is TauCeti.SimpleSubmoduleClasses k[G] k[G]. Two bijections onto two targets are not yet one theorem read twice; what makes them one is a comparison of the targets.

TauCeti.SimpleFDRepClasses.toSimpleSubmoduleClasses is that comparison: it sends a simple object to the isomorphism class of the k[G]-module it carries. It is well defined because isomorphic objects carry isomorphic modules, by TauCeti.nonempty_fdRepIso_iff followed by TauCeti.Representation.nonempty_equiv_iff, and injective because that chain of equivalences runs backwards just as well. See TauCeti.coe_simpleFDRepClassesEquivSimpleModuleClasses for the symmetric group, where the comparison identifies the two classifications by the partitions of n.

Main results

• TauCeti.SimpleFDRepClasses.toSimpleSubmoduleClasses: over a semisimple group algebra, the isomorphism class of the k[G]-module a simple object carries.
• TauCeti.SimpleFDRepClasses.toSimpleSubmoduleClasses_injective: distinct classes of simple objects carry distinct classes of modules, so the comparison identifies the categorical classification with a part of the module-level one.

noncomputable def TauCeti.SimpleFDRepClasses.toSimpleSubmoduleClasses {k : Type u} {G : Type v} [Field k] [Monoid G] [IsSemisimpleRing (MonoidAlgebra k G)] : SimpleFDRepClasses k G → SimpleSubmoduleClasses (MonoidAlgebra k G) (MonoidAlgebra k G)

The isomorphism class of the k[G]-module a simple object of FDRep k G carries. Over a semisimple group algebra this compares the categorical classification with the module-level one of TauCeti.SimpleSubmoduleClasses.

Equations

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

@[simp]

theorem TauCeti.SimpleFDRepClasses.toSimpleSubmoduleClasses_mk {k : Type u} {G : Type v} [Field k] [Monoid G] [IsSemisimpleRing (MonoidAlgebra k G)] (X : FDRep k G) [CategoryTheory.Simple X] : (mk X).toSimpleSubmoduleClasses = simpleModuleClass (MonoidAlgebra k G) (Representation.asModule X.ρ)

theorem TauCeti.SimpleFDRepClasses.toSimpleSubmoduleClasses_injective {k : Type u} {G : Type v} [Field k] [Monoid G] [IsSemisimpleRing (MonoidAlgebra k G)] : Function.Injective toSimpleSubmoduleClasses

The comparison is injective: two simple objects of FDRep k G carrying isomorphic k[G]-modules are isomorphic, so the fibres of the comparison are single classes. This is the well-definedness argument run backwards.