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.

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

@[reducible, inline]

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

Equations

• FDRep k G = Action (FGModuleCat k) (MonCat.of G)

@[deprecated FDRep]

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

Alias of FDRep.

---

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

Equations

• FdRep = FDRep

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

Equations

• FDRep.instLargeCategory = inferInstance

noncomputable instance FDRep.instConcreteCategory {k : Type u} {G : Type u} [Field k] [Monoid G] : CategoryTheory.ConcreteCategory (FDRep k G)

Equations

• FDRep.instConcreteCategory = inferInstance

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

Equations

• FDRep.instPreadditive = inferInstance

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

Equations

• ⋯ = ⋯

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

Equations

• FDRep.instLinear = inferInstance

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

Equations

• FDRep.instCoeSortType = CategoryTheory.ConcreteCategory.hasCoeToSort (FDRep k G)

noncomputable instance FDRep.instAddCommGroupCoe {k : Type u} {G : Type u} [Field k] [Monoid G] (V : FDRep k G) : AddCommGroup (CoeSort.coe V)

Equations

• V.instAddCommGroupCoe = let_fun this := inferInstance; this

noncomputable instance FDRep.instModuleCoe {k : Type u} {G : Type u} [Field k] [Monoid G] (V : FDRep k G) : Module k (CoeSort.coe V)

Equations

• V.instModuleCoe = let_fun this := inferInstance; this

noncomputable instance FDRep.instFiniteDimensionalCoe {k : Type u} {G : Type u} [Field k] [Monoid G] (V : FDRep k G) : FiniteDimensional k (CoeSort.coe V)

Equations

• ⋯ = ⋯

noncomputable instance FDRep.instFiniteDimensionalHom {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.

Equations

• ⋯ = ⋯

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

Equations

• V.ρ = V.ρ

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

Equations

• FDRep.isoToLinearEquiv i = FGModuleCat.isoToLinearEquiv ((Action.forget (FGModuleCat k) (MonCat.of G)).mapIso i)

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) : W.ρ g = (FDRep.isoToLinearEquiv i).conj (V.ρ g)

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

Equations

• FDRep.of ρ = { V := FGModuleCat.of k V, ρ := ρ }

@[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 ρ).ρ = ρ

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

Equations

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

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

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

Equations

• ⋯ = ⋯

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

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

Equations

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

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

Equations

• FDRep.instRightRigidCategory = let_fun this := inferInstance; this

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 ρV.dual) W).V ≅ (FDRep.of (ρV.linHom W.ρ)).V

Auxiliary definition for FDRep.dualTensorIsoLinHom.

Equations

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

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 ρV.dual) W ≅ FDRep.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 : 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)