Finite-dimensional representations as group-algebra modules

For a finite monoid G (typically a finite group) and a commutative ring k (typically a field), the usual equivalence between representations of G and modules over the monoid algebra k[G] restricts to an equivalence

FDRep k G ≌ FGModuleCat k[G].

The finiteness assertion in one direction uses that k[G] is a finite k-module; in the other, a finite representation is generated over k[G] by any finite set of k-module generators. When k is Noetherian, this restricted equivalence identifies the abelian exact structure on finite representations with the exact structure of finitely generated group-algebra modules, and is the bridge between categorical representation theory and G₀(k[G]).

Main definitions

• TauCeti.fdRepEquivalence: the equivalence between finite-dimensional representations and finitely generated group-algebra modules.
• TauCeti.isConflationExact_fdRepEquivalence_functor and TauCeti.isConflationExact_fdRepEquivalence_inverse: the equivalence preserves the chosen exact structures in both directions.

noncomputable def TauCeti.fdRepEquivalence (k G : Type u) [CommRing k] [Monoid G] [Finite G] : FDRep k G ≌ FGModuleCat (MonoidAlgebra k G)

Finite-dimensional representations are finitely generated group-algebra modules. This is the restriction of Rep.equivalenceModuleMonoidAlgebra to finite objects.

instance TauCeti.instAdditiveFDRepFGModuleCatMonoidAlgebraFunctorFdRepEquivalence (k G : Type u) [CommRing k] [Monoid G] [Finite G] : (fdRepEquivalence k G).functor.Additive

@[simp]

theorem TauCeti.fdRepEquivalence_functor_obj_obj (k G : Type u) [CommRing k] [Monoid G] [Finite G] (V : FDRep k G) : ((fdRepEquivalence k G).functor.obj V).obj = ↧(Representation.asModule V.ρ)

The forward functor of fdRepEquivalence sends a representation to its underlying group-algebra module.

theorem TauCeti.fdRepEquivalence_functor_comp_ι (k G : Type u) [CommRing k] [Monoid G] [Finite G] : (fdRepEquivalence k G).functor.comp (ModuleCat.isFG (MonoidAlgebra k G)).ι = (CategoryTheory.forget₂ (FDRep k G) (Rep k G)).comp Rep.toModuleMonoidAlgebra

Followed by the inclusion into all modules, the forward functor of fdRepEquivalence is Rep.toModuleMonoidAlgebra; in particular it sends an equivariant map to the same map, viewed as a linear map of group-algebra modules.

theorem TauCeti.instIsNoetherianRingMonoidAlgebra_tauCeti (k G : Type u) [CommRing k] [Monoid G] [Finite G] [IsNoetherianRing k] : IsNoetherianRing (MonoidAlgebra k G)

theorem TauCeti.isConflationExact_fdRepEquivalence_functor (k G : Type u) [CommRing k] [Monoid G] [Finite G] [IsNoetherianRing k] : (ExactStructure.abelian (FDRep k G)).IsConflationExact (finiteModulesExactStructure (MonoidAlgebra k G)) (fdRepEquivalence k G).functor

The forward direction of fdRepEquivalence carries short exact sequences of finite-dimensional representations to conflations of finitely generated group-algebra modules.

theorem TauCeti.isConflationExact_fdRepEquivalence_inverse (k G : Type u) [CommRing k] [Monoid G] [Finite G] [IsNoetherianRing k] : (finiteModulesExactStructure (MonoidAlgebra k G)).IsConflationExact (ExactStructure.abelian (FDRep k G)) (fdRepEquivalence k G).inverse

The inverse direction of fdRepEquivalence carries conflations of finitely generated group-algebra modules to short exact sequences of finite-dimensional representations.