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 construct the categorical equivalence Rep k G ≌ Module (monoid_algebra k G). 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
@[reducible]
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} [comm_ring k] [monoid G] :
has_coe_to_sort (Rep k G) (Type u)
Equations
source
@[protected, instance]
def Rep.add_comm_group {k G : Type u} [comm_ring k] [monoid G] (V : Rep k G) :
add_comm_group ↥V
Equations
source
@[protected, instance]
def Rep.module {k G : Type u} [comm_ring k] [monoid G] (V : Rep k G) :
module k ↥V
Equations
source
def Rep.ρ {k G : Type u} [comm_ring k] [monoid G] (V : Rep k G) :
representation k G ↥V

Specialize the existing Action.ρ, changing the type to representation k G V.

Equations
source
def Rep.of {k G : Type u} [comm_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
source
@[simp]
theorem Rep.coe_of {k G : Type u} [comm_ring k] [monoid G] {V : Type u} [add_comm_group V] [module k V] (ρ : G →* V →ₗ[k] V) :
↥(Rep.of ρ) = V
source
@[simp]
theorem Rep.of_ρ {k G : Type u} [comm_ring k] [monoid G] {V : Type u} [add_comm_group V] [module k V] (ρ : G →* V →ₗ[k] V) :
(Rep.of ρ).ρ = ρ

The categorical equivalence Rep k G ≌ Module.{u} (monoid_algebra k G). #

source
theorem Rep.to_Module_monoid_algebra_map_aux {k : Type u_1} {G : Type u_2} [comm_ring k] [monoid G] (V : Type u_3) (W : Type u_4) [add_comm_group V] [add_comm_group W] [module k V] [module k W] (ρ : G →* V →ₗ[k] V) (σ : G →* W →ₗ[k] W) (f : V →ₗ[k] W) (w : ∀ (g : G), f.comp (⇑ρ g) = (⇑σ g).comp f) (r : monoid_algebra k G) (x : V) :
⇑f (⇑(⇑(⇑(monoid_algebra.lift k G (V →ₗ[k] V)) ρ) r) x) = ⇑(⇑(⇑(monoid_algebra.lift k G (W →ₗ[k] W)) σ) r) (⇑f x)

Auxilliary lemma for to_Module_monoid_algebra.

source
def Rep.to_Module_monoid_algebra_map {k G : Type u} [comm_ring k] [monoid G] {V W : Rep k G} (f : V ⟶ W) :
Module.of (monoid_algebra k G) V.ρ.as_module ⟶ Module.of (monoid_algebra k G) W.ρ.as_module

Auxilliary definition for to_Module_monoid_algebra.

Equations
source
noncomputable def Rep.to_Module_monoid_algebra {k G : Type u} [comm_ring k] [monoid G] :
Rep k G ⥤ Module (monoid_algebra k G)

Functorially convert a representation of G into a module over monoid_algebra k G.

Equations
source
noncomputable def Rep.of_Module_monoid_algebra {k G : Type u} [comm_ring k] [monoid G] :
Module (monoid_algebra k G) ⥤ Rep k G

Functorially convert a module over monoid_algebra k G into a representation of G.

Equations
source
theorem Rep.of_Module_monoid_algebra_obj_coe {k G : Type u} [comm_ring k] [monoid G] (M : Module (monoid_algebra k G)) :
↥(Rep.of_Module_monoid_algebra.obj M) = restrict_scalars k (monoid_algebra k G) ↥M
source
theorem Rep.of_Module_monoid_algebra_obj_ρ {k G : Type u} [comm_ring k] [monoid G] (M : Module (monoid_algebra k G)) :
(Rep.of_Module_monoid_algebra.obj M).ρ = representation.of_module k G ↥M
source
noncomputable def Rep.counit_iso_add_equiv {k G : Type u} [comm_ring k] [monoid G] {M : Module (monoid_algebra k G)} :
↥((Rep.of_Module_monoid_algebra ⋙ Rep.to_Module_monoid_algebra).obj M) ≃+ ↥M

Auxilliary definition for equivalence_Module_monoid_algebra.

Equations
source
noncomputable def Rep.unit_iso_add_equiv {k G : Type u} [comm_ring k] [monoid G] {V : Rep k G} :
↥V ≃+ ↥((Rep.to_Module_monoid_algebra ⋙ Rep.of_Module_monoid_algebra).obj V)

Auxilliary definition for equivalence_Module_monoid_algebra.

Equations
source
noncomputable def Rep.counit_iso {k G : Type u} [comm_ring k] [monoid G] (M : Module (monoid_algebra k G)) :
(Rep.of_Module_monoid_algebra ⋙ Rep.to_Module_monoid_algebra).obj M ≅ M

Auxilliary definition for equivalence_Module_monoid_algebra.

Equations
source
theorem Rep.unit_iso_comm {k G : Type u} [comm_ring k] [monoid G] (V : Rep k G) (g : G) (x : ↥V) :
⇑Rep.unit_iso_add_equiv ((⇑(V.ρ) g).to_fun x) = (⇑((Rep.of_Module_monoid_algebra.obj (Rep.to_Module_monoid_algebra.obj V)).ρ) g).to_fun (⇑Rep.unit_iso_add_equiv x)
source
noncomputable def Rep.unit_iso {k G : Type u} [comm_ring k] [monoid G] (V : Rep k G) :
V ≅ (Rep.to_Module_monoid_algebra ⋙ Rep.of_Module_monoid_algebra).obj V

Auxilliary definition for equivalence_Module_monoid_algebra.

Equations
source
noncomputable def Rep.equivalence_Module_monoid_algebra {k G : Type u} [comm_ring k] [monoid G] :
Rep k G ≌ Module (monoid_algebra k G)

The categorical equivalence Rep k G ≌ Module (monoid_algebra k G).

Equations