FDRep k G is the category of finite-dimensional k-linear representations of G.

If V : FDRep k G, there is a coercion that allows you to treat V as a type, and this type comes equipped with Module k V and FiniteDimensional k V instances. Also V.ρ gives the homomorphism G →* (V →ₗ[k] V).

Conversely, given a homomorphism ρ : G →* (V →ₗ[k] V), you can construct the bundled representation as Rep.of ρ.

We prove Schur's Lemma: the dimension of the Hom-space between two irreducible representation is 0 if they are not isomorphic, and 1 if they are. This is the content of finrank_hom_simple_simple

We verify that FDRep k G is a k-linear monoidal category, and rigid when G is a group.

FDRep k G has all finite limits.

Implementation notes

We define FDRep R G for any ring R and monoid G, as the category of finitely generated R-linear representations of G.

The main case of interest is when R = k is a field and G is a group, and this is reflected in the documentation.

TODO

• FdRep k G ≌ FullSubcategory (FiniteDimensional k)
• FdRep k G has all finite colimits.
• FdRep k G is abelian.
• FdRep k G ≌ FGModuleCat k[G].

@[reducible, inline]

noncomputable abbrev FDRep (R G : Type u) [Ring R] [Monoid G] : Type (u + 1)

The category of finitely generated R-linear representations of a monoid G.

Note that R can be any ring, but the main case of interest is when R = k is a field and G is a group.

Equations

• FDRep R G = Action (FGModuleCat R) G

noncomputable instance FDRep.instLargeCategory {R G : Type u} [CommRing R] [Monoid G] : CategoryTheory.LargeCategory (FDRep R G)

Equations

• FDRep.instLargeCategory = inferInstance

noncomputable instance FDRep.instConcreteCategoryHomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV {R G : Type u} [CommRing R] [Monoid G] : CategoryTheory.ConcreteCategory (FDRep R G) (Action.HomSubtype (FGModuleCat R) G)

Equations

• FDRep.instConcreteCategoryHomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV = inferInstance

noncomputable instance FDRep.instPreadditive {R G : Type u} [CommRing R] [Monoid G] : CategoryTheory.Preadditive (FDRep R G)

Equations

• FDRep.instPreadditive = inferInstance

instance FDRep.instHasFiniteLimits {k G : Type u} [Field k] [Monoid G] : CategoryTheory.Limits.HasFiniteLimits (FDRep k G)

noncomputable instance FDRep.instLinear {R G : Type u} [CommRing R] [Monoid G] : CategoryTheory.Linear R (FDRep R G)

Equations

• FDRep.instLinear = inferInstance

noncomputable instance FDRep.instCoeSortType {R G : Type u} [CommRing R] [Monoid G] : CoeSort (FDRep R G) (Type u)

Equations

• FDRep.instCoeSortType = { coe := fun (V : FDRep R G) => ↑V.V }

noncomputable instance FDRep.instAddCommGroupCarrierVFGModuleCat {R G : Type u} [CommRing R] [Monoid G] (V : FDRep R G) : AddCommGroup ↑V.V

Equations

• V.instAddCommGroupCarrierVFGModuleCat = id inferInstance

noncomputable instance FDRep.instModuleCarrierVFGModuleCat {R G : Type u} [CommRing R] [Monoid G] (V : FDRep R G) : Module R ↑V.V

Equations

• V.instModuleCarrierVFGModuleCat = id inferInstance

instance FDRep.instFiniteCarrierVFGModuleCat {R G : Type u} [CommRing R] [Monoid G] (V : FDRep R G) : Module.Finite R ↑V.V

instance FDRep.instFiniteDimensionalCarrierVFGModuleCat {k G : Type u} [Field k] [Monoid G] (V : FDRep k G) : FiniteDimensional k ↑V.V

instance FDRep.instFiniteDimensionalHom {k G : Type u} [Field k] [Monoid G] (V W : FDRep k G) : FiniteDimensional k (V ⟶ W)

All hom spaces are finite dimensional.

noncomputable def FDRep.ρ {R G : Type u} [CommRing R] [Monoid G] (V : FDRep R G) : G →* ↑V.V →ₗ[R] ↑V.V

The monoid homomorphism corresponding to the action of G onto V : FDRep R G.

Equations

• V.ρ = V.V.obj.endRingEquiv.toMonoidHom.comp (CategoryTheory.InducedCategory.endEquiv.toMonoidHom.comp V.ρ)

@[simp]

theorem FDRep.endRingEquiv_symm_comp_ρ {R G : Type u} [CommRing R] [Monoid G] (V : FDRep R G) : (↑V.V.obj.endRingEquiv.symm).comp V.ρ = CategoryTheory.InducedCategory.endEquiv.toMonoidHom.comp V.ρ

theorem FDRep.endRingEquiv_comp_ρ {R G : Type u} [CommRing R] [Monoid G] (V : FDRep R G) : (↑V.V.obj.endRingEquiv).comp (CategoryTheory.InducedCategory.endEquiv.toMonoidHom.comp V.ρ) = V.ρ

@[simp]

theorem FDRep.hom_hom_action_ρ {R G : Type u} [CommRing R] [Monoid G] (V : FDRep R G) (g : G) : ModuleCat.Hom.hom (V.ρ g).hom = V.ρ g

@[deprecated FDRep.hom_hom_action_ρ (since := "2025-12-18")]

theorem FDRep.hom_action_ρ {R G : Type u} [CommRing R] [Monoid G] (V : FDRep R G) (g : G) : ModuleCat.Hom.hom (V.ρ g).hom = V.ρ g

Alias of FDRep.hom_hom_action_ρ.

noncomputable def FDRep.isoToLinearEquiv {R G : Type u} [CommRing R] [Monoid G] {V W : FDRep R G} (i : V ≅ W) : ↑V.V ≃ₗ[R] ↑W.V

The underlying LinearEquiv of an isomorphism of representations.

Equations

• FDRep.isoToLinearEquiv i = FGModuleCat.isoToLinearEquiv ((Action.forget (FGModuleCat R) G).mapIso i)

theorem FDRep.Iso.conj_ρ {R G : Type u} [CommRing R] [Monoid G] {V W : FDRep R G} (i : V ≅ W) (g : G) : W.ρ g = (isoToLinearEquiv i).conj (V.ρ g)

@[reducible, inline]

noncomputable abbrev FDRep.of {R G : Type u} [CommRing R] [Monoid G] {V : Type u} [AddCommGroup V] [Module R V] [Module.Finite R V] (ρ : Representation R G V) : FDRep R G

Lift an unbundled representation to FDRep.

Equations

• FDRep.of ρ = { V := FGModuleCat.of R V, ρ := CategoryTheory.InducedCategory.endEquiv.symm.toMonoidHom.comp ((ModuleCat.of R V).endRingEquiv.symm.toMonoidHom.comp ρ) }

@[simp]

theorem FDRep.of_ρ {R G : Type u} [CommRing R] [Monoid G] {V : Type u} [AddCommGroup V] [Module R V] [Module.Finite R V] (ρ : Representation R G V) : (of ρ).ρ = CategoryTheory.InducedCategory.endEquiv.symm.toMonoidHom.comp ((ModuleCat.of R V).endRingEquiv.symm.toMonoidHom.comp ρ)

@[simp]

theorem FDRep.of_ρ' {R G : Type u} [CommRing R] [Monoid G] {V : Type u} [AddCommGroup V] [Module R V] [Module.Finite R V] (ρ : G →* V →ₗ[R] V) : (of ρ).ρ = ρ

This lemma is about FDRep.ρ, instead of Action.ρ for of_ρ.

noncomputable instance FDRep.instHasForget₂Rep {R G : Type u} [CommRing R] [Monoid G] : CategoryTheory.HasForget₂ (FDRep R G) (Rep R G)

Equations

• FDRep.instHasForget₂Rep = { forget₂ := (CategoryTheory.forget₂ (FGModuleCat R) (ModuleCat R)).mapAction G, forget_comp := ⋯ }

theorem FDRep.forget₂_ρ {R G : Type u} [CommRing R] [Monoid G] (V : FDRep R G) : ((CategoryTheory.forget₂ (FDRep R G) (Rep R G)).obj V).ρ = V.ρ

instance FDRep.instPreservesFiniteLimitsRepForget₂OfIsNoetherianRing {R G : Type u} [CommRing R] [Monoid G] [IsNoetherianRing R] : CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.forget₂ (FDRep R G) (Rep R G))

instance FDRep.instPreservesFiniteColimitsRepForget₂ {R G : Type u} [CommRing R] [Monoid G] : CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.forget₂ (FDRep R G) (Rep R G))

instance FDRep.instHasKernels {k G : Type u} [Field k] [Monoid G] : CategoryTheory.Limits.HasKernels (FDRep k G)

theorem FDRep.finrank_hom_simple_simple {k G : Type u} [Field k] [Monoid G] [IsAlgClosed k] (V W : FDRep k G) [CategoryTheory.Simple V] [CategoryTheory.Simple W] : Module.finrank k (V ⟶ W) = if Nonempty (V ≅ W) then 1 else 0

Schur's Lemma: the dimension of the Hom-space between two irreducible representation is 0 if they are not isomorphic, and 1 if they are.

noncomputable def FDRep.forget₂HomLinearEquiv {R G : Type u} [CommRing R] [Monoid G] (X Y : FDRep R G) : ((CategoryTheory.forget₂ (FDRep R G) (Rep R G)).obj X ⟶ (CategoryTheory.forget₂ (FDRep R G) (Rep R G)).obj Y) ≃ₗ[R] X ⟶ Y

The forgetful functor to Rep k G preserves hom-sets and their vector space structure.

Equations

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

instance FDRep.instFullRepForget₂ {R G : Type u} [CommRing R] [Monoid G] : (CategoryTheory.forget₂ (FDRep R G) (Rep R G)).Full

instance FDRep.instFaithfulRepForget₂ {R G : Type u} [CommRing R] [Monoid G] : (CategoryTheory.forget₂ (FDRep R G) (Rep R G)).Faithful

noncomputable instance FDRep.instRightRigidCategory {k G : Type u} [Field k] [Group G] : CategoryTheory.RightRigidCategory (FDRep k G)

Equations

• FDRep.instRightRigidCategory = id inferInstance

noncomputable def FDRep.dualTensorIsoLinHomAux {k G V : Type u} [Field k] [Group G] [AddCommGroup V] [Module k V] [FiniteDimensional k V] (ρV : Representation k G V) (W : FDRep k G) : (CategoryTheory.MonoidalCategoryStruct.tensorObj (of ρV.dual) W).V ≅ (of (ρV.linHom W.ρ)).V

Auxiliary definition for FDRep.dualTensorIsoLinHom.

Equations

• FDRep.dualTensorIsoLinHomAux ρV W = (dualTensorHomEquiv k V ↑W.V).toFGModuleCatIso

noncomputable def FDRep.dualTensorIsoLinHom {k G V : Type u} [Field k] [Group G] [AddCommGroup V] [Module k V] [FiniteDimensional k V] (ρV : Representation k G V) (W : FDRep k G) : CategoryTheory.MonoidalCategoryStruct.tensorObj (of ρV.dual) W ≅ of (ρV.linHom W.ρ)

When V and W are finite-dimensional representations of a group G, the isomorphism dualTensorHomEquiv k V W of vector spaces induces an isomorphism of representations.

Equations

• FDRep.dualTensorIsoLinHom ρV W = Action.mkIso (FDRep.dualTensorIsoLinHomAux ρV W) ⋯

@[simp]

theorem FDRep.dualTensorIsoLinHom_hom_hom {k G V : Type u} [Field k] [Group G] [AddCommGroup V] [Module k V] [FiniteDimensional k V] (ρV : Representation k G V) (W : FDRep k G) : (dualTensorIsoLinHom ρV W).hom.hom = CategoryTheory.ConcreteCategory.ofHom (dualTensorHom k V ↑W.V)