# Documentation

Mathlib.RepresentationTheory.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 ≌ ModuleCat (MonoidAlgebra k G). We verify that Rep k G is a k-linear abelian symmetric monoidal category with all (co)limits.

@[inline, reducible]
abbrev Rep (k : Type u) (G : Type u) [Ring k] [] :
Type (u + 1)

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

Instances For
instance Rep.instCoeSortRepToRingType {k : Type u} {G : Type u} [] [] :
CoeSort (Rep k G) (Type u)
def Rep.ρ {k : Type u} {G : Type u} [] [] (V : Rep k G) :

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

Instances For
def Rep.of {k : Type u} {G : Type u} [] [] {V : Type u} [] [Module k V] (ρ : G →* V →ₗ[k] V) :
Rep k G

Lift an unbundled representation to Rep.

Instances For
@[simp]
theorem Rep.coe_of {k : Type u} {G : Type u} [] [] {V : Type u} [] [Module k V] (ρ : G →* V →ₗ[k] V) :
= V
@[simp]
theorem Rep.of_ρ {k : Type u} {G : Type u} [] [] {V : Type u} [] [Module k V] (ρ : G →* V →ₗ[k] V) :
Rep.ρ () = ρ
theorem Rep.Action_ρ_eq_ρ {k : Type u} {G : Type u} [] [] {A : Rep k G} :
A =
theorem Rep.of_ρ_apply {k : Type u} {G : Type u} [] [] {V : Type u} [] [Module k V] (ρ : ) (g : ↑()) :
↑(Rep.ρ ()) g = ρ g

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

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

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

Instances For
theorem Rep.trivial_def {k : Type u} {G : Type u} [] [] {V : Type u} [] [Module k V] (g : G) (v : V) :
↑(↑(Rep.ρ (Rep.trivial k G V)) g) v = v
theorem Rep.MonoidalCategory.braiding_hom_apply {k : Type u} {G : Type u} [] [] {A : Rep k G} {B : Rep k G} (x : ) (y : ) :
(β_ A B).hom.hom (x ⊗ₜ[k] y) = y ⊗ₜ[k] x
theorem Rep.MonoidalCategory.braiding_inv_apply {k : Type u} {G : Type u} [] [] {A : Rep k G} {B : Rep k G} (x : ) (y : ) :
(β_ A B).inv.hom (y ⊗ₜ[k] x) = x ⊗ₜ[k] y
noncomputable def Rep.linearization (k : Type u) (G : Type u) [] [] :

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

Instances For
@[simp]
theorem Rep.linearization_obj_ρ {k : Type u} {G : Type u} [] [] (X : Action (Type u) ()) (g : G) (x : X.V →₀ k) :
↑(↑(Rep.ρ (().toLaxMonoidalFunctor.toFunctor.obj X)) g) x = ↑(Finsupp.lmapDomain k k (X g)) x
theorem Rep.linearization_of {k : Type u} {G : Type u} [] [] (X : Action (Type u) ()) (g : G) (x : X.V) :
(↑(↑(Rep.ρ (().toLaxMonoidalFunctor.toFunctor.obj X)) g) fun₀ | x => 1) = fun₀ | X g x => 1
theorem Rep.linearization_single {k : Type u} {G : Type u} [] [] (X : Action (Type u) ()) (g : G) (x : X.V) (r : k) :
(↑(↑(Rep.ρ (().toLaxMonoidalFunctor.toFunctor.obj X)) g) fun₀ | x => r) = fun₀ | X g x => r
@[simp]
theorem Rep.linearization_map_hom {k : Type u} {G : Type u} [] [] {X : Action (Type u) ()} {Y : Action (Type u) ()} (f : X Y) :
(().toLaxMonoidalFunctor.toFunctor.map f).hom = Finsupp.lmapDomain k k f.hom
theorem Rep.linearization_map_hom_single {k : Type u} {G : Type u} [] [] {X : Action (Type u) ()} {Y : Action (Type u) ()} (f : X Y) (x : X.V) (r : k) :
((().toLaxMonoidalFunctor.toFunctor.map f).hom fun₀ | x => r) = fun₀ | => r
@[simp]
theorem Rep.linearization_μ_hom {k : Type u} {G : Type u} [] [] (X : Action (Type u) ()) (Y : Action (Type u) ()) :
(CategoryTheory.LaxMonoidalFunctor.μ ().toLaxMonoidalFunctor X Y).hom = ↑(finsuppTensorFinsupp' k X.V Y.V)
@[simp]
theorem Rep.linearization_μ_inv_hom {k : Type u} {G : Type u} [] [] (X : Action (Type u) ()) (Y : Action (Type u) ()) :
@[simp]
theorem Rep.linearization_ε_hom {k : Type u} {G : Type u} [] [] :
().toLaxMonoidalFunctor.hom =
@[simp]
theorem Rep.linearization_ε_inv_hom_apply {k : Type u} {G : Type u} [] [] (r : k) :
((CategoryTheory.inv ().toLaxMonoidalFunctor).hom fun₀ | PUnit.unit => r) = r
@[simp]
theorem Rep.linearizationTrivialIso_hom_hom_apply (k : Type u) (G : Type u) [] [] (X : Type u) :
∀ (a : (().toLaxMonoidalFunctor.toFunctor.obj { V := X, ρ := 1 }).V), ().hom.hom a = a
@[simp]
theorem Rep.linearizationTrivialIso_inv_hom_apply (k : Type u) (G : Type u) [] [] (X : Type u) :
∀ (a : (().toLaxMonoidalFunctor.toFunctor.obj { V := X, ρ := 1 }).V), ().inv.hom a = a
noncomputable def Rep.linearizationTrivialIso (k : Type u) (G : Type u) [] [] (X : Type u) :
().toLaxMonoidalFunctor.toFunctor.obj { V := X, ρ := 1 } Rep.trivial k G (X →₀ k)

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

Instances For
@[inline, reducible]
noncomputable abbrev Rep.ofMulAction (k : Type u) (G : Type u) [] [] (H : Type u) [] :
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.

Instances For
noncomputable def Rep.leftRegular (k : Type u) (G : Type u) [] [] :
Rep k G

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

Instances For
noncomputable def Rep.diagonal (k : Type u) (G : Type u) [] [] (n : ) :
Rep k G

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

Instances For
noncomputable def Rep.linearizationOfMulActionIso (k : Type u) (G : Type u) [] [] (H : Type u) [] :
().toLaxMonoidalFunctor.toFunctor.obj ()

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.

Instances For
@[simp]
theorem Rep.leftRegularHom_hom {k : Type u} {G : Type u} [] [] (A : Rep k G) (x : ) :
().hom = ↑(Finsupp.lift ((fun x => ) x) k G) fun g => ↑(↑() g) x
noncomputable def Rep.leftRegularHom {k : Type u} {G : Type u} [] [] (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).

Instances For
theorem Rep.leftRegularHom_apply {k : Type u} {G : Type u} [] [] {A : Rep k G} (x : ) :
(().hom fun₀ | 1 => 1) = x
@[simp]
theorem Rep.leftRegularHomEquiv_symm_apply {k : Type u} {G : Type u} [] [] (A : Rep k G) (x : ) :
@[simp]
theorem Rep.leftRegularHomEquiv_apply {k : Type u} {G : Type u} [] [] (A : Rep k G) (f : A) :
↑() f = f.hom fun₀ | 1 => 1
noncomputable def Rep.leftRegularHomEquiv {k : Type u} {G : Type u} [] [] (A : Rep k G) :
( A) ≃ₗ[k]

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

Instances For
theorem Rep.leftRegularHomEquiv_symm_single {k : Type u} {G : Type u} [] [] {A : Rep k G} (x : ) (g : G) :
(().hom fun₀ | g => 1) = ↑(↑() g) x
@[simp]
theorem Rep.ihom_map_hom {k : Type u} {G : Type u} [] [] (A : Rep k G) {X : Rep k G} {Y : Rep k G} (f : X Y) :
(().map f).hom = ModuleCat.ofHom (↑(LinearMap.llcomp k () X.V Y.V) f.hom)
@[simp]
theorem Rep.ihom_obj {k : Type u} {G : Type u} [] [] (A : Rep k G) (B : Rep k G) :
().obj B = Rep.of (Representation.linHom () ())
def Rep.ihom {k : Type u} {G : Type u} [] [] (A : 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⁻¹).

Instances For
@[simp]
theorem Rep.ihom_obj_ρ_apply {k : Type u} {G : Type u} [] [] {A : Rep k G} {B : Rep k G} (g : G) (x : ) :
↑(↑(Rep.ρ (().obj B)) g) x = LinearMap.comp (↑() g) (LinearMap.comp x (↑() g⁻¹))
def Rep.homEquiv {k : Type u} {G : Type u} [] [] (A : Rep k G) (B : Rep k G) (C : Rep k G) :
() (B ().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.

Instances For
theorem Rep.homEquiv_apply_hom {k : Type u} {G : Type u} [] [] {A : Rep k G} {B : Rep k G} {C : Rep k G} (f : ) :
(↑(Rep.homEquiv A B C) f).hom =

Porting note: if we generate this with @[simps] the linter complains some types in the LHS simplify.

theorem Rep.homEquiv_symm_apply_hom {k : Type u} {G : Type u} [] [] {A : Rep k G} {B : Rep k G} {C : Rep k G} (f : B ().obj C) :
((Rep.homEquiv A B C).symm f).hom = ↑(TensorProduct.uncurry k () () ()) (LinearMap.flip f.hom)

Porting note: if we generate this with @[simps] the linter complains some types in the LHS simplify.

@[simp]
theorem Rep.ihom_obj_ρ_def {k : Type u} {G : Type u} [] [] (A : Rep k G) (B : Rep k G) :
Rep.ρ (().obj B) = Rep.ρ (().obj B)
@[simp]
theorem Rep.homEquiv_def {k : Type u} {G : Type u} [] [] (A : Rep k G) (B : Rep k G) (C : Rep k G) :
@[simp]
theorem Rep.ihom_ev_app_hom {k : Type u} {G : Type u} [] [] (A : Rep k G) (B : Rep k G) :
(().app B).hom = ↑(TensorProduct.uncurry k () () ()) (LinearMap.flip LinearMap.id)
@[simp]
theorem Rep.ihom_coev_app_hom {k : Type u} {G : Type u} [] [] (A : Rep k G) (B : Rep k G) :
(().app B).hom = LinearMap.flip (TensorProduct.mk k () (().obj B).V)
def Rep.MonoidalClosed.linearHomEquiv {k : Type u} {G : Type u} [] [] (A : Rep k G) (B : Rep k G) (C : Rep k G) :
() ≃ₗ[k] B ().obj C

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

Instances For
def Rep.MonoidalClosed.linearHomEquivComm {k : Type u} {G : Type u} [] [] (A : Rep k G) (B : Rep k G) (C : Rep k G) :
() ≃ₗ[k] A ().obj C

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

Instances For
@[simp]
theorem Rep.MonoidalClosed.linearHomEquiv_hom {k : Type u} {G : Type u} [] [] {A : Rep k G} {B : Rep k G} {C : Rep k G} (f : ) :
(↑() f).hom =
@[simp]
theorem Rep.MonoidalClosed.linearHomEquivComm_hom {k : Type u} {G : Type u} [] [] {A : Rep k G} {B : Rep k G} {C : Rep k G} (f : ) :
(↑() f).hom = TensorProduct.curry f.hom
@[simp]
theorem Rep.MonoidalClosed.linearHomEquiv_symm_hom {k : Type u} {G : Type u} [] [] {A : Rep k G} {B : Rep k G} {C : Rep k G} (f : B ().obj C) :
(↑() f).hom = ↑(TensorProduct.uncurry k () () ()) (LinearMap.flip f.hom)
@[simp]
theorem Rep.MonoidalClosed.linearHomEquivComm_symm_hom {k : Type u} {G : Type u} [] [] {A : Rep k G} {B : Rep k G} {C : Rep k G} (f : A ().obj C) :
().hom = ↑(TensorProduct.uncurry k () () ()) f.hom
def Representation.repOfTprodIso {k : Type u} {G : Type u} [] [] {V : Type u} {W : Type u} [] [] [Module k V] [Module k W] (ρ : ) (τ : ) :

Tautological isomorphism to help Lean in typechecking.

Instances For
theorem Representation.repOfTprodIso_apply {k : Type u} {G : Type u} [] [] {V : Type u} {W : Type u} [] [] [Module k V] [Module k W] (ρ : ) (τ : ) (x : ) :
().hom.hom x = x
theorem Representation.repOfTprodIso_inv_apply {k : Type u} {G : Type u} [] [] {V : Type u} {W : Type u} [] [] [Module k V] [Module k W] (ρ : ) (τ : ) (x : ) :
().inv.hom x = x

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

theorem Rep.to_Module_monoidAlgebra_map_aux {k : Type u_1} {G : Type u_2} [] [] (V : Type u_3) (W : Type u_4) [] [] [Module k V] [Module k W] (ρ : G →* V →ₗ[k] V) (σ : G →* W →ₗ[k] W) (f : V →ₗ[k] W) (w : ∀ (g : G), LinearMap.comp f (ρ g) = LinearMap.comp (σ g) f) (r : ) (x : V) :
f (↑(↑(↑(MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) r) x) = ↑(↑(↑(MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) r) (f x)

Auxiliary lemma for toModuleMonoidAlgebra.

def Rep.toModuleMonoidAlgebraMap {k : Type u} {G : Type u} [] [] {V : Rep k G} {W : Rep k G} (f : V W) :

Auxiliary definition for toModuleMonoidAlgebra.

Instances For

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

Instances For

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

Instances For
theorem Rep.ofModuleMonoidAlgebra_obj_coe {k : Type u} {G : Type u} [] [] (M : ModuleCat ()) :
CoeSort.coe (Rep.ofModuleMonoidAlgebra.obj M) = RestrictScalars k () M
theorem Rep.ofModuleMonoidAlgebra_obj_ρ {k : Type u} {G : Type u} [] [] (M : ModuleCat ()) :
Rep.ρ (Rep.ofModuleMonoidAlgebra.obj M) =
def Rep.counitIsoAddEquiv {k : Type u} {G : Type u} [] [] {M : ModuleCat ()} :
↑((CategoryTheory.Functor.comp Rep.ofModuleMonoidAlgebra Rep.toModuleMonoidAlgebra).obj M) ≃+ M

Auxiliary definition for equivalenceModuleMonoidAlgebra.

Instances For
def Rep.unitIsoAddEquiv {k : Type u} {G : Type u} [] [] {V : Rep k G} :
≃+ CoeSort.coe ((CategoryTheory.Functor.comp Rep.toModuleMonoidAlgebra Rep.ofModuleMonoidAlgebra).obj V)

Auxiliary definition for equivalenceModuleMonoidAlgebra.

Instances For
def Rep.counitIso {k : Type u} {G : Type u} [] [] (M : ModuleCat ()) :
(CategoryTheory.Functor.comp Rep.ofModuleMonoidAlgebra Rep.toModuleMonoidAlgebra).obj M M

Auxiliary definition for equivalenceModuleMonoidAlgebra.

Instances For
theorem Rep.unit_iso_comm {k : Type u} {G : Type u} [] [] (V : Rep k G) (g : G) (x : ) :
Auxiliary definition for equivalenceModuleMonoidAlgebra.
The categorical equivalence Rep k G ≌ ModuleCat (MonoidAlgebra k G).