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.

@[protected, instance]

def Rep.has_colimits (k G : Type u) [ring k] [monoid G] :

category_theory.limits.has_colimits (Rep k G)

@[protected, instance]

def Rep.preadditive (k G : Type u) [ring k] [monoid G] :

category_theory.preadditive (Rep k G)

@[protected, instance]

noncomputable def Rep.abelian (k G : Type u) [ring k] [monoid G] :

category_theory.abelian (Rep k G)

@[protected, instance]

def Rep.large_category (k G : Type u) [ring k] [monoid G] :

category_theory.large_category (Rep k G)

@[protected, instance]

def Rep.has_limits (k G : Type u) [ring k] [monoid G] :

category_theory.limits.has_limits (Rep k G)

@[reducible]

def Rep (k G : Type u) [ring k] [monoid G] :

Type (u+1)

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

@[protected, instance]

def Rep.concrete_category (k G : Type u) [ring k] [monoid G] :

category_theory.concrete_category (Rep k G)

@[protected, instance]

def Rep.category_theory.linear (k G : Type u) [comm_ring k] [monoid G] :

category_theory.linear k (Rep k G)

Equations

Rep.category_theory.linear k G = Action.category_theory.linear

@[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

Rep.has_coe_to_sort = category_theory.concrete_category.has_coe_to_sort (Rep k G)

@[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

V.add_comm_group = id ((category_theory.forget₂ (Rep k G) (Module k)).obj V).is_add_comm_group

@[protected, instance]

def Rep.module {k G : Type u} [comm_ring k] [monoid G] (V : Rep k G) :

Equations

V.module = id ((category_theory.forget₂ (Rep k G) (Module k)).obj V).is_module

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

V.ρ = V.ρ

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

Rep.of ρ = {V := Module.of k V _inst_4, ρ := ρ}

@[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

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

noncomputable def Rep.linearization (k G : Type u) [comm_ring k] [monoid G] :

category_theory.monoidal_functor (Action (Type u) (Mon.of G)) (Rep k G)

The monoidal functor sending a type H with a G-action to the induced k-linear G-representation on k[H].

Equations

Rep.linearization k G = (Module.monoidal_free k).map_Action (Mon.of G)

@[simp]

theorem Rep.linearization_obj_ρ {k G : Type u} [comm_ring k] [monoid G] (X : Action (Type u) (Mon.of G)) (g : G) (x : X.V →₀ k) :

⇑(⇑(((Rep.linearization k G).to_lax_monoidal_functor.to_functor.obj X).ρ) g) x = ⇑(finsupp.lmap_domain k k (⇑(X.ρ) g)) x

@[simp]

theorem Rep.linearization_of {k G : Type u} [comm_ring k] [monoid G] (X : Action (Type u) (Mon.of G)) (g : G) (x : X.V) :

⇑(⇑(((Rep.linearization k G).to_lax_monoidal_functor.to_functor.obj X).ρ) g) (finsupp.single x 1) = finsupp.single (⇑(X.ρ) g x) 1

@[simp]

theorem Rep.linearization_map_hom {k G : Type u} [comm_ring k] [monoid G] (X Y : Action (Type u) (Mon.of G)) (f : X ⟶ Y) :

((Rep.linearization k G).to_lax_monoidal_functor.to_functor.map f).hom = finsupp.lmap_domain k k f.hom

theorem Rep.linearization_map_hom_of {k G : Type u} [comm_ring k] [monoid G] (X Y : Action (Type u) (Mon.of G)) (f : X ⟶ Y) (x : X.V) :

⇑(((Rep.linearization k G).to_lax_monoidal_functor.to_functor.map f).hom) (finsupp.single x 1) = finsupp.single (f.hom x) 1

@[reducible]

noncomputable def Rep.of_mul_action (k G : Type u) [comm_ring k] [monoid G] (H : Type u) [mul_action G H] :

Rep k G

Given a G-action on H, this is k[H] bundled with the natural representation G →* End(k[H]) as a term of type Rep k G.

noncomputable def Rep.linearization_of_mul_action_iso (k G : Type u) [comm_ring k] [monoid G] (n : ℕ) :

(Rep.linearization k G).to_lax_monoidal_functor.to_functor.obj (Action.of_mul_action G (fin n → G)) ≅ Rep.of_mul_action k G (fin n → G)

The linearization of a type H with a G-action is definitionally isomorphic to the k-linear G-representation on k[H] induced by the G-action on H.

Equations

Rep.linearization_of_mul_action_iso k G n = category_theory.iso.refl ((Rep.linearization k G).to_lax_monoidal_functor.to_functor.obj (Action.of_mul_action G (fin n → G)))

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

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.

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

Rep.to_Module_monoid_algebra_map f = {to_fun := f.hom.to_fun, map_add' := _, map_smul' := _}

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

Rep.to_Module_monoid_algebra = {obj := λ (V : Rep k G), Module.of (monoid_algebra k G) V.ρ.as_module, map := λ (V W : Rep k G) (f : V ⟶ W), Rep.to_Module_monoid_algebra_map f, map_id' := _, map_comp' := _}

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

Rep.of_Module_monoid_algebra = {obj := λ (M : Module (monoid_algebra k G)), Rep.of (representation.of_module k G ↥M), map := λ (M N : Module (monoid_algebra k G)) (f : M ⟶ N), {hom := {to_fun := f.to_fun, map_add' := _, map_smul' := _}, comm' := _}, map_id' := _, map_comp' := _}

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

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

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

Rep.counit_iso_add_equiv = id ((representation.of_module k G ↥M).as_module_equiv.trans (restrict_scalars.add_equiv k (monoid_algebra k G) ↥M))

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

Rep.unit_iso_add_equiv = id (V.ρ.as_module_equiv.symm.trans (restrict_scalars.add_equiv k (monoid_algebra k G) V.ρ.as_module).symm)

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

Rep.counit_iso M = {to_fun := Rep.counit_iso_add_equiv.to_fun, map_add' := _, map_smul' := _, inv_fun := Rep.counit_iso_add_equiv.inv_fun, left_inv := _, right_inv := _}.to_Module_iso'

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)

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

V.unit_iso = Action.mk_iso {to_fun := Rep.unit_iso_add_equiv.to_fun, map_add' := _, map_smul' := _, inv_fun := Rep.unit_iso_add_equiv.inv_fun, left_inv := _, right_inv := _}.to_Module_iso' _

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

Rep.equivalence_Module_monoid_algebra = {functor := Rep.to_Module_monoid_algebra _inst_2, inverse := Rep.of_Module_monoid_algebra _inst_2, unit_iso := category_theory.nat_iso.of_components (λ (V : Rep k G), V.unit_iso) Rep.equivalence_Module_monoid_algebra._proof_1, counit_iso := category_theory.nat_iso.of_components (λ (M : Module (monoid_algebra k G)), Rep.counit_iso M) Rep.equivalence_Module_monoid_algebra._proof_2, functor_unit_iso_comp' := _}