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 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.

TODO

• FdRep k G ≌ FullSubcategory (FiniteDimensional k)
• Upgrade the right rigid structure to a rigid structure (this just needs to be done for FGModuleCat).
• FdRep k G has all finite colimits.
• FdRep k G is abelian.
• FdRep k G ≌ FGModuleCat (MonoidAlgebra k G).

@[inline, reducible]

abbrev FdRep (k : Type u) (G : Type u) [Field k] [Monoid G] : Type (u + 1)

The category of finite dimensional k-linear representations of a monoid G.

instance FdRep.instLargeCategoryFdRep {k : Type u} {G : Type u} [Field k] [Monoid G] : CategoryTheory.LargeCategory (FdRep k G)

instance FdRep.instConcreteCategoryFdRepInstLargeCategoryFdRep {k : Type u} {G : Type u} [Field k] [Monoid G] : CategoryTheory.ConcreteCategory (FdRep k G)

instance FdRep.instPreadditiveFdRepInstLargeCategoryFdRep {k : Type u} {G : Type u} [Field k] [Monoid G] : CategoryTheory.Preadditive (FdRep k G)

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

instance FdRep.instLinearToSemiringToDivisionSemiringToSemifieldFdRepInstLargeCategoryFdRepInstPreadditiveFdRepInstLargeCategoryFdRep {k : Type u} {G : Type u} [Field k] [Monoid G] : CategoryTheory.Linear k (FdRep k G)

instance FdRep.instCoeSortFdRepType {k : Type u} {G : Type u} [Field k] [Monoid G] : CoeSort (FdRep k G) (Type u)

instance FdRep.instAddCommGroupCoeFdRepTypeInstCoeSortFdRepType {k : Type u} {G : Type u} [Field k] [Monoid G] (V : FdRep k G) : AddCommGroup (CoeSort.coe V)

instance FdRep.instModuleCoeFdRepTypeInstCoeSortFdRepTypeToSemiringToDivisionSemiringToSemifieldToAddCommMonoidInstAddCommGroupCoeFdRepTypeInstCoeSortFdRepType {k : Type u} {G : Type u} [Field k] [Monoid G] (V : FdRep k G) : Module k (CoeSort.coe V)

instance FdRep.instFiniteDimensionalCoeFdRepTypeInstCoeSortFdRepTypeToDivisionRingInstAddCommGroupCoeFdRepTypeInstCoeSortFdRepTypeInstModuleCoeFdRepTypeInstCoeSortFdRepTypeToSemiringToDivisionSemiringToSemifieldToAddCommMonoidInstAddCommGroupCoeFdRepTypeInstCoeSortFdRepType {k : Type u} {G : Type u} [Field k] [Monoid G] (V : FdRep k G) : FiniteDimensional k (CoeSort.coe V)

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

All hom spaces are finite dimensional.

def FdRep.ρ {k : Type u} {G : Type u} [Field k] [Monoid G] (V : FdRep k G) : G →* CoeSort.coe V →ₗ[k] CoeSort.coe V

The monoid homomorphism corresponding to the action of G onto V : FdRep k G.

def FdRep.isoToLinearEquiv {k : Type u} {G : Type u} [Field k] [Monoid G] {V : FdRep k G} {W : FdRep k G} (i : V ≅ W) : CoeSort.coe V ≃ₗ[k] CoeSort.coe W

The underlying LinearEquiv of an isomorphism of representations.

theorem FdRep.Iso.conj_ρ {k : Type u} {G : Type u} [Field k] [Monoid G] {V : FdRep k G} {W : FdRep k G} (i : V ≅ W) (g : G) : ↑(FdRep.ρ W) g = ↑(LinearEquiv.conj (FdRep.isoToLinearEquiv i)) (↑(FdRep.ρ V) g)

@[simp]

theorem FdRep.of_ρ {k : Type u} {G : Type u} [Field k] [Monoid G] {V : Type u} [AddCommGroup V] [Module k V] [FiniteDimensional k V] (ρ : Representation k G V) : (FdRep.of ρ).ρ = ρ

def FdRep.of {k : Type u} {G : Type u} [Field k] [Monoid G] {V : Type u} [AddCommGroup V] [Module k V] [FiniteDimensional k V] (ρ : Representation k G V) : FdRep k G

Lift an unbundled representation to FdRep.

instance FdRep.instHasForget₂FdRepRepToRingToDivisionRingInstLargeCategoryFdRepInstConcreteCategoryFdRepInstLargeCategoryFdRepInstCategoryActionModuleCatModuleCategoryOfInstConcreteCategoryActionInstCategoryActionModuleConcreteCategory {k : Type u} {G : Type u} [Field k] [Monoid G] : CategoryTheory.HasForget₂ (FdRep k G) (Rep k G)

theorem FdRep.forget₂_ρ {k : Type u} {G : Type u} [Field k] [Monoid G] (V : FdRep k G) : Rep.ρ ((CategoryTheory.forget₂ (FdRep k G) (Rep k G)).obj V) = FdRep.ρ V

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

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

def FdRep.forget₂HomLinearEquiv {k : Type u} {G : Type u} [Field k] [Monoid G] (X : FdRep k G) (Y : FdRep k G) : ((CategoryTheory.forget₂ (FdRep k G) (Rep k G)).obj X ⟶ (CategoryTheory.forget₂ (FdRep k G) (Rep k G)).obj Y) ≃ₗ[k] X ⟶ Y

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

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

noncomputable def FdRep.dualTensorIsoLinHomAux {k : Type u} {G : Type u} {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.MonoidalCategory.tensorObj (FdRep.of (Representation.dual ρV)) W).V ≅ (FdRep.of (Representation.linHom ρV (FdRep.ρ W))).V

Auxiliary definition for FdRep.dualTensorIsoLinHom.

noncomputable def FdRep.dualTensorIsoLinHom {k : Type u} {G : Type u} {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.MonoidalCategory.tensorObj (FdRep.of (Representation.dual ρV)) W ≅ FdRep.of (Representation.linHom ρV (FdRep.ρ 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.

@[simp]

theorem FdRep.dualTensorIsoLinHom_hom_hom {k : Type u} {G : Type u} {V : Type u} [Field k] [Group G] [AddCommGroup V] [Module k V] [FiniteDimensional k V] (ρV : Representation k G V) (W : FdRep k G) : (FdRep.dualTensorIsoLinHom ρV W).hom.hom = dualTensorHom k V (CoeSort.coe W)