mathlib documentation

representation_theory.Rep

Rep k G is the category of k-linear representations of G. #

If V : Rep k G, there is a coercion that allows you to treat V as a type, and this type comes equipped with a module k V instance. 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 Rep k G is a k-linear abelian symmetric monoidal category with all (co)limits.

source
@[protected, instance]
def Rep.has_colimits (k G : Type u) [ring k] [monoid G] :
category_theory.limits.has_colimits (Rep k G)
source
@[protected, instance]
def Rep.preadditive (k G : Type u) [ring k] [monoid G] :
category_theory.preadditive (Rep k G)
source
@[protected, instance]
noncomputable def Rep.abelian (k G : Type u) [ring k] [monoid G] :
category_theory.abelian (Rep k G)
source
@[protected, instance]
def Rep.large_category (k G : Type u) [ring k] [monoid G] :
category_theory.large_category (Rep k G)
source
@[protected, instance]
def Rep.has_limits (k G : Type u) [ring k] [monoid G] :
category_theory.limits.has_limits (Rep k G)
source
def Rep (k G : Type u) [ring k] [monoid G] :
Type (u+1)

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

source
@[protected, instance]
def Rep.concrete_category (k G : Type u) [ring k] [monoid G] :
category_theory.concrete_category (Rep k G)
source
@[protected, instance]
def Rep.category_theory.linear (k G : Type u) [comm_ring k] [monoid G] :
category_theory.linear k (Rep k G)
Equations
source
@[protected, instance]
def Rep.has_coe_to_sort {k G : Type u} [ring k] [monoid G] :
has_coe_to_sort (Rep k G) (Type u)
Equations
source
@[protected, instance]
def Rep.add_comm_monoid {k G : Type u} [ring k] [monoid G] (V : Rep k G) :
add_comm_monoid ↥V
Equations
source
@[protected, instance]
def Rep.module {k G : Type u} [ring k] [monoid G] (V : Rep k G) :
module k ↥V
Equations
source
@[simp]
theorem Rep.of_ρ {k G : Type u} [ring k] [monoid G] {V : Type u} [add_comm_group V] [module k V] (ρ : G →* V →ₗ[k] V) :
(Rep.of ρ).ρ = ρ
source
def Rep.of {k G : Type u} [ring k] [monoid G] {V : Type u} [add_comm_group V] [module k V] (ρ : G →* V →ₗ[k] V) :
Rep k G

Lift an unbundled representation to Rep.

Equations