mathlib3 documentation

representation_theory.Rep

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

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

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]
@[protected, instance]
@[protected, instance]
noncomputable def Rep.abelian (k G : Type u) [ring k] [monoid G] :
@[protected, instance]
@[protected, instance]
@[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]
@[protected, instance]
def Rep.add_comm_group {k G : Type u} [comm_ring k] [monoid G] (V : Rep k G) :
Equations
@[protected, instance]
def Rep.module {k G : Type u} [comm_ring k] [monoid G] (V : Rep k G) :
Equations
def Rep.ρ {k G : Type u} [comm_ring k] [monoid G] (V : Rep k G) :

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

Equations
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
@[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 ρ).ρ = ρ
theorem Rep.Action_ρ_eq_ρ {k G : Type u} [comm_ring k] [monoid G] {A : Rep k G} :
A.ρ = A.ρ
theorem Rep.of_ρ_apply {k G : Type u} [comm_ring k] [monoid G] {V : Type u} [add_comm_group V] [module k V] (ρ : representation k G V) (g : (Mon.of G)) :
((Rep.of ρ).ρ) g = ρ g

Allows us to apply lemmas about the underlying ρ, which would take an element g : G rather than g : Mon.of G as an argument.

@[simp]
theorem Rep.ρ_inv_self_apply {k : Type u} [comm_ring k] {G : Type u} [group G] (A : Rep k G) (g : G) (x : A) :
((A.ρ) g⁻¹) (((A.ρ) g) x) = x
@[simp]
theorem Rep.ρ_self_inv_apply {k : Type u} [comm_ring k] {G : Type u} [group G] {A : Rep k G} (g : G) (x : A) :
((A.ρ) g) (((A.ρ) g⁻¹) x) = x
theorem Rep.hom_comm_apply {k G : Type u} [comm_ring k] [monoid G] {A B : Rep k G} (f : A B) (g : G) (x : A) :
(f.hom) (((A.ρ) g) x) = ((B.ρ) g) ((f.hom) x)
def Rep.trivial (k G : Type u) [comm_ring k] [monoid G] (V : Type u) [add_comm_group V] [module k V] :
Rep k G

The trivial k-linear G-representation on a k-module V.

Equations
theorem Rep.trivial_def {k G : Type u} [comm_ring k] [monoid G] {V : Type u} [add_comm_group V] [module k V] (g : G) (v : V) :
(((Rep.trivial k G V).ρ) g) v = v
@[simp]
theorem Rep.monoidal_category.braiding_hom_apply {k G : Type u} [comm_ring k] [monoid G] {A B : Rep k G} (x : A) (y : B) :
((β_ A B).hom.hom) (x ⊗ₜ[k] y) = y ⊗ₜ[k] x
@[simp]
theorem Rep.monoidal_category.braiding_inv_apply {k G : Type u} [comm_ring k] [monoid G] {A B : Rep k G} (x : A) (y : B) :
((β_ A B).inv.hom) (y ⊗ₜ[k] x) = x ⊗ₜ[k] y
noncomputable def Rep.linearization (k G : Type u) [comm_ring k] [monoid G] :

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

Equations
@[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) :
@[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) :
theorem Rep.linearization_map_hom_single {k G : Type u} [comm_ring k] [monoid G] {X Y : Action (Type u) (Mon.of G)} (f : X Y) (x : X.V) (r : k) :
noncomputable def Rep.linearization_trivial_iso (k G : Type u) [comm_ring k] [monoid G] (X : Type u) :

The linearization of a type X on which G acts trivially is the trivial G-representation on k[X].

Equations
@[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.left_regular (k G : Type u) [comm_ring k] [monoid G] :
Rep k G

The k-linear G-representation on k[G], induced by left multiplication.

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

The k-linear G-representation on k[Gⁿ], induced by left multiplication.

Equations

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
noncomputable def Rep.left_regular_hom {k G : Type u} [comm_ring k] [monoid G] (A : Rep k G) (x : A) :

Given an element x : A, there is a natural morphism of representations k[G] ⟶ A sending g ↦ A.ρ(g)(x).

Equations
@[simp]
theorem Rep.left_regular_hom_hom {k G : Type u} [comm_ring k] [monoid G] (A : Rep k G) (x : A) :
(A.left_regular_hom x).hom = (finsupp.lift A k G) (λ (g : G), ((A.ρ) g) x)
theorem Rep.left_regular_hom_apply {k G : Type u} [comm_ring k] [monoid G] {A : Rep k G} (x : A) :
noncomputable def Rep.left_regular_hom_equiv {k G : Type u} [comm_ring k] [monoid G] (A : Rep k G) :

Given a k-linear G-representation A, there is a k-linear isomorphism between representation morphisms Hom(k[G], A) and A.

Equations
@[simp]
theorem Rep.left_regular_hom_equiv_apply {k G : Type u} [comm_ring k] [monoid G] (A : Rep k G) (f : Rep.of_mul_action k G G A) :
@[simp]
theorem Rep.left_regular_hom_equiv_symm_single {k G : Type u} [comm_ring k] [monoid G] {A : Rep k G} (x : A) (g : G) :
@[protected]
def Rep.ihom {k G : Type u} [comm_ring k] [group G] (A : Rep k G) :
Rep k G Rep k G

Given a k-linear G-representation (A, ρ₁), this is the 'internal Hom' functor sending (B, ρ₂) to the representation Homₖ(A, B) that maps g : G and f : A →ₗ[k] B to (ρ₂ g) ∘ₗ f ∘ₗ (ρ₁ g⁻¹).

Equations
@[simp]
theorem Rep.ihom_obj {k G : Type u} [comm_ring k] [group G] (A B : Rep k G) :
@[simp]
theorem Rep.ihom_map_hom {k G : Type u} [comm_ring k] [group G] (A X Y : Rep k G) (f : X Y) :
@[protected, simp]
theorem Rep.ihom_obj_ρ_apply {k G : Type u} [comm_ring k] [group G] {A B : Rep k G} (g : G) (x : A →ₗ[k] B) :
(((A.ihom.obj B).ρ) g) x = ((B.ρ) g).comp (x.comp ((A.ρ) g⁻¹))
@[protected]
def Rep.hom_equiv {k G : Type u} [comm_ring k] [group G] (A B C : Rep k G) :
(A B C) (B A.ihom.obj C)

Given a k-linear G-representation A, this is the Hom-set bijection in the adjunction A ⊗ - ⊣ ihom(A, -). It sends f : A ⊗ B ⟶ C to a Rep k G morphism defined by currying the k-linear map underlying f, giving a map A →ₗ[k] B →ₗ[k] C, then flipping the arguments.

Equations
@[simp]
theorem Rep.hom_equiv_apply_hom {k G : Type u} [comm_ring k] [group G] (A B C : Rep k G) (f : A B C) :
@[simp]
theorem Rep.hom_equiv_symm_apply_hom {k G : Type u} [comm_ring k] [group G] (A B C : Rep k G) (f : B A.ihom.obj C) :
@[simp]
theorem Rep.ihom_obj_ρ_def {k G : Type u} [comm_ring k] [group G] (A B : Rep k G) :
@[simp]
theorem Rep.hom_equiv_def {k G : Type u} [comm_ring k] [group G] (A B C : Rep k G) :
@[simp]
theorem Rep.ihom_coev_app_hom {k G : Type u} [comm_ring k] [group G] (A B : Rep k G) :
def Rep.monoidal_closed.linear_hom_equiv {k G : Type u} [comm_ring k] [group G] (A B C : Rep k G) :

There is a k-linear isomorphism between the sets of representation morphismsHom(A ⊗ B, C) and Hom(B, Homₖ(A, C)).

Equations
def Rep.monoidal_closed.linear_hom_equiv_comm {k G : Type u} [comm_ring k] [group G] (A B C : Rep k G) :

There is a k-linear isomorphism between the sets of representation morphismsHom(A ⊗ B, C) and Hom(A, Homₖ(B, C)).

Equations
def representation.Rep_of_tprod_iso {k G : Type u} [comm_ring k] [monoid G] {V W : Type u} [add_comm_group V] [add_comm_group W] [module k V] [module k W] (ρ : representation k G V) (τ : representation k G W) :

Tautological isomorphism to help Lean in typechecking.

Equations
theorem representation.Rep_of_tprod_iso_apply {k G : Type u} [comm_ring k] [monoid G] {V W : Type u} [add_comm_group V] [add_comm_group W] [module k V] [module k W] (ρ : representation k G V) (τ : representation k G W) (x : tensor_product k V W) :
theorem representation.Rep_of_tprod_iso_inv_apply {k G : Type u} [comm_ring k] [monoid G] {V W : Type u} [add_comm_group V] [add_comm_group W] [module k V] [module k W] (ρ : representation k G V) (τ : representation k G W) (x : tensor_product k V W) :

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.

Auxilliary definition for to_Module_monoid_algebra.

Equations
noncomputable def Rep.to_Module_monoid_algebra {k G : Type u} [comm_ring k] [monoid G] :

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

Equations
noncomputable def Rep.of_Module_monoid_algebra {k G : Type u} [comm_ring k] [monoid G] :

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

Equations

Auxilliary definition for equivalence_Module_monoid_algebra.

Equations

Auxilliary definition for equivalence_Module_monoid_algebra.

Equations

Auxilliary definition for equivalence_Module_monoid_algebra.

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

Auxilliary definition for equivalence_Module_monoid_algebra.

Equations
noncomputable def Rep.equivalence_Module_monoid_algebra {k G : Type u} [comm_ring k] [monoid G] :

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

Equations