mathlib3 documentation

representation_theory.fdRep

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 finite_dimensional 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 #

@[protected, instance]
@[protected, instance]
@[reducible]
def fdRep (k G : Type u) [field k] [monoid G] :
Type (u+1)

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

@[protected, instance]
@[protected, instance]
@[protected, instance]
def fdRep.add_comm_group {k G : Type u} [field k] [monoid G] (V : fdRep k G) :
Equations
@[protected, instance]
def fdRep.module {k G : Type u} [field k] [monoid G] (V : fdRep k G) :
Equations
@[protected, instance]
def fdRep.finite_dimensional {k G : Type u} [field k] [monoid G] (V : fdRep k G) :
@[protected, instance]
def fdRep.quiver.hom.finite_dimensional {k G : Type u} [field k] [monoid G] (V W : fdRep k G) :

All hom spaces are finite dimensional.

def fdRep.ρ {k G : Type u} [field k] [monoid G] (V : fdRep k G) :

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

Equations
def fdRep.iso_to_linear_equiv {k G : Type u} [field k] [monoid G] {V W : fdRep k G} (i : V W) :

The underlying linear_equiv of an isomorphism of representations.

Equations
theorem fdRep.iso.conj_ρ {k G : Type u} [field k] [monoid G] {V W : fdRep k G} (i : V W) (g : G) :
@[simp]
theorem fdRep.of_ρ {k G : Type u} [field k] [monoid G] {V : Type u} [add_comm_group V] [module k V] [finite_dimensional k V] (ρ : representation k G V) :
(fdRep.of ρ).ρ = ρ
def fdRep.of {k G : Type u} [field k] [monoid G] {V : Type u} [add_comm_group V] [module k V] [finite_dimensional k V] (ρ : representation k G V) :
fdRep k G

Lift an unbundled representation to fdRep.

Equations
theorem fdRep.forget₂_ρ {k G : Type u} [field k] [monoid G] (V : fdRep k G) :
def fdRep.forget₂_hom_linear_equiv {k G : Type u} [field k] [monoid G] (X Y : fdRep k G) :

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

Equations
noncomputable def fdRep.dual_tensor_iso_lin_hom_aux {k G V : Type u} [field k] [group G] [add_comm_group V] [module k V] [finite_dimensional k V] (ρV : representation k G V) (W : fdRep k G) :
(fdRep.of ρV.dual W).V (fdRep.of (ρV.lin_hom W.ρ)).V

Auxiliary definition for fdRep.dual_tensor_iso_lin_hom.

Equations
noncomputable def fdRep.dual_tensor_iso_lin_hom {k G V : Type u} [field k] [group G] [add_comm_group V] [module k V] [finite_dimensional k V] (ρV : representation k G V) (W : fdRep k G) :

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

Equations