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 ρ).ρ = ρ
source
@[simp]
theorem Rep.Action_ρ_eq_ρ {k G : Type u} [comm_ring k] [monoid G] {A : Rep k G} :
A.ρ = A.ρ
source
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.

source
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
source
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
source
@[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
source
@[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
source
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
source
@[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
source
@[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
source
@[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
source
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) :
⇑(((Rep.linearization k G).to_lax_monoidal_functor.to_functor.map f).hom) (finsupp.single x r) = finsupp.single (f.hom x) r
source
@[simp]
theorem Rep.linearization_μ_hom {k G : Type u} [comm_ring k] [monoid G] (X Y : Action (Type u) (Mon.of G)) :
((Rep.linearization k G).to_lax_monoidal_functor.μ X Y).hom = (finsupp_tensor_finsupp' k X.V Y.V).to_linear_map
source
@[simp]
theorem Rep.linearization_μ_inv_hom {k G : Type u} [comm_ring k] [monoid G] (X Y : Action (Type u) (Mon.of G)) :
(category_theory.inv ((Rep.linearization k G).to_lax_monoidal_functor.μ X Y)).hom = (finsupp_tensor_finsupp' k X.V Y.V).symm.to_linear_map
source
@[simp]
theorem Rep.linearization_ε_hom {k G : Type u} [comm_ring k] [monoid G] :
(Rep.linearization k G).to_lax_monoidal_functor.ε.hom = finsupp.lsingle punit.star
source
@[simp]
theorem Rep.linearization_ε_inv_hom_apply {k G : Type u} [comm_ring k] [monoid G] (r : k) :
⇑((category_theory.inv (Rep.linearization k G).to_lax_monoidal_functor.ε).hom) (finsupp.single punit.star r) = r
source
@[simp]
theorem Rep.linearization_trivial_iso_inv_hom_apply (k G : Type u) [comm_ring k] [monoid G] (X : Type u) (a : ↥(((Rep.linearization k G).to_lax_monoidal_functor.to_functor.obj {V := X, ρ := 1}).V)) :
⇑((Rep.linearization_trivial_iso k G X).inv.hom) a = a
source
noncomputable def Rep.linearization_trivial_iso (k G : Type u) [comm_ring k] [monoid G] (X : Type u) :
(Rep.linearization k G).to_lax_monoidal_functor.to_functor.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].

Equations
source
@[simp]
theorem Rep.linearization_trivial_iso_hom_hom_apply (k G : Type u) [comm_ring k] [monoid G] (X : Type u) (a : ↥(((Rep.linearization k G).to_lax_monoidal_functor.to_functor.obj {V := X, ρ := 1}).V)) :
⇑((Rep.linearization_trivial_iso k G X).hom.hom) a = a
source
@[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.

source
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
source
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
source
noncomputable def Rep.linearization_of_mul_action_iso (k G : Type u) [comm_ring k] [monoid G] (H : Type u) [mul_action G H] :
(Rep.linearization k G).to_lax_monoidal_functor.to_functor.obj (Action.of_mul_action G H) ≅ Rep.of_mul_action k G H

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

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

Equations
source
@[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)
source
theorem Rep.left_regular_hom_apply {k G : Type u} [comm_ring k] [monoid G] {A : Rep k G} (x : ↥A) :
⇑((A.left_regular_hom x).hom) (finsupp.single 1 1) = x
source
noncomputable def Rep.left_regular_hom_equiv {k G : Type u} [comm_ring k] [monoid G] (A : Rep k G) :
(Rep.of_mul_action k G G ⟶ A) ≃ₗ[k] ↥A

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

Equations
source
@[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) :
⇑(A.left_regular_hom_equiv) f = ⇑(f.hom) (finsupp.single 1 1)
source
@[simp]
theorem Rep.left_regular_hom_equiv_symm_apply {k G : Type u} [comm_ring k] [monoid G] (A : Rep k G) (x : ↥A) :
⇑(A.left_regular_hom_equiv.symm) x = A.left_regular_hom x
source
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) :
⇑((⇑(A.left_regular_hom_equiv.symm) x).hom) (finsupp.single g 1) = ⇑(⇑(A.ρ) g) x
source
@[protected, instance]
noncomputable def Rep.category_theory.monoidal_closed {k G : Type u} [comm_ring k] [group G] :
category_theory.monoidal_closed (Rep k G)
Equations
source
theorem Rep.ihom_obj_ρ_def {k G : Type u} [comm_ring k] [group G] (A B : Rep k G) :
((category_theory.ihom A).obj B).ρ = (Action.functor_category_equivalence.inverse.obj ((Action.functor_category_equivalence.functor.obj A).closed_ihom.obj (Action.functor_category_equivalence.functor.obj B))).ρ

Explicit description of the 'internal Hom' iHom(A, B) of two representations A, B: this is F⁻¹(iHom(F(A), F(B))), where F is an equivalence Rep k G ≌ (single_obj G ⥤ Module k). Just used to prove Rep.ihom_obj_ρ.

source
@[simp]
theorem Rep.ihom_obj_ρ {k G : Type u} [comm_ring k] [group G] (A B : Rep k G) :
((category_theory.ihom A).obj B).ρ = A.ρ.lin_hom B.ρ

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

source
@[simp]
theorem Rep.ihom_map_hom {k G : Type u} [comm_ring k] [group G] (A : Rep k G) {B C : Rep k G} (f : B ⟶ C) :
((category_theory.ihom A).map f).hom = ⇑(linear_map.llcomp k ↥A ↥B ↥C) f.hom
source
theorem Rep.ihom_coev_app_def {k G : Type u} [comm_ring k] [group G] (A B : Rep k G) :
(category_theory.ihom.coev A).app B = Action.functor_category_equivalence.unit_iso.hom.app B ≫ Action.functor_category_equivalence.inverse.map ((Action.functor_category_equivalence.functor.obj A).closed_unit.app ((Action.functor_category_monoidal_equivalence (Module k) (Mon.of G)).to_lax_monoidal_functor.to_functor.obj B) ≫ (Action.functor_category_equivalence.functor.obj A).closed_ihom.map ((Action.functor_category_monoidal_equivalence (Module k) (Mon.of G)).to_lax_monoidal_functor.μ A B))

Unfolds the unit in the adjunction A ⊗ - ⊣ iHom(A, -); just used to prove Rep.ihom_coev_app_hom.

source
@[simp]
theorem Rep.ihom_coev_app_hom {k G : Type u} [comm_ring k] [group G] (A B : Rep k G) :
((category_theory.ihom.coev A).app B).hom = (tensor_product.mk k ↥(opposite.unop (opposite.op (opposite.unop (((category_theory.prod_functor_to_functor_prod (category_theory.single_obj ↥(Mon.of G)) (Module k)ᵒᵖ (Module k)).obj (category_theory.groupoid.inv_functor (category_theory.single_obj ↥(Mon.of G)) ⋙ ((Action.functor_category_monoidal_equivalence (Module k) (Mon.of G)).to_lax_monoidal_functor.to_functor.obj A).op, (category_theory.is_left_adjoint.right (Action.functor_category_monoidal_equivalence (Module k) (Mon.of G)).to_lax_monoidal_functor.to_functor.inv).obj ((category_theory.monoidal_category.tensor_left A).obj B))).obj punit.star).fst))) ↥(((𝟭 (Rep k G)).obj B).V)).flip

Describes the unit in the adjunction A ⊗ - ⊣ iHom(A, -); given another k-linear G-representation B, the k-linear map underlying the resulting map B ⟶ iHom(A, A ⊗ B) is given by flipping the arguments in the natural k-bilinear map A →ₗ[k] B →ₗ[k] A ⊗ B.

source
@[simp]
theorem Rep.monoidal_closed_curry_hom {k G : Type u} [comm_ring k] [group G] {A B C : Rep k G} (f : A ⊗ B ⟶ C) :
(category_theory.monoidal_closed.curry f).hom = (tensor_product.curry f.hom).flip

Given a k-linear G-representation A, the adjunction A ⊗ - ⊣ iHom(A, -) defines a bijection Hom(A ⊗ B, C) ≃ Hom(B, iHom(A, C)) for all B, C. Given f : A ⊗ B ⟶ C, this lemma describes the k-linear map underlying f's image under the bijection. It is given by currying the k-linear map underlying f, giving a map A →ₗ[k] B →ₗ[k] C, then flipping the arguments.

source
@[simp]
theorem Rep.monoidal_closed_uncurry_hom {k G : Type u} [comm_ring k] [group G] {A B C : Rep k G} (f : B ⟶ (category_theory.ihom A).obj C) :
(category_theory.monoidal_closed.uncurry f).hom = ⇑(tensor_product.uncurry k ↥(opposite.unop (opposite.op (opposite.unop (((category_theory.prod_functor_to_functor_prod (category_theory.single_obj ↥(Mon.of G)) (Module k)ᵒᵖ (Module k)).obj (category_theory.groupoid.inv_functor (category_theory.single_obj ↥(Mon.of G)) ⋙ ((Action.functor_category_monoidal_equivalence (Module k) (Mon.of G)).to_lax_monoidal_functor.to_functor.obj A).op, (category_theory.is_left_adjoint.right (Action.functor_category_monoidal_equivalence (Module k) (Mon.of G)).to_lax_monoidal_functor.to_functor.inv).obj C)).obj punit.star).fst))) ↥(B.V) ↥((((category_theory.prod_functor_to_functor_prod (category_theory.single_obj ↥(Mon.of G)) (Module k)ᵒᵖ (Module k)).obj (category_theory.groupoid.inv_functor (category_theory.single_obj ↥(Mon.of G)) ⋙ ((Action.functor_category_monoidal_equivalence (Module k) (Mon.of G)).to_lax_monoidal_functor.to_functor.obj A).op, (category_theory.is_left_adjoint.right (Action.functor_category_monoidal_equivalence (Module k) (Mon.of G)).to_lax_monoidal_functor.to_functor.inv).obj C)).obj punit.star).snd)) (linear_map.flip f.hom)

Given a k-linear G-representation A, the adjunction A ⊗ - ⊣ iHom(A, -) defines a bijection Hom(A ⊗ B, C) ≃ Hom(B, iHom(A, C)) for all B, C. Given f : B ⟶ iHom(A, C), this lemma describes the k-linear map underlying f's image under the bijection. It is given by flipping the arguments of the k-linear map underlying f, giving a map A →ₗ[k] B →ₗ[k] C, then uncurrying.

source
@[simp]
theorem Rep.ihom_ev_app_hom {k G : Type u} [comm_ring k] [group G] {A B : Rep k G} :
((category_theory.ihom.ev A).app B).hom = ⇑(tensor_product.uncurry k ↥(((Action.functor_category_equivalence (Module k) (Mon.of G)).symm.inverse.obj A).obj punit.star) (↥(((Action.functor_category_equivalence (Module k) (Mon.of G)).symm.inverse.obj A).obj punit.star) →ₗ[k] ↥((((category_theory.prod_functor_to_functor_prod (category_theory.single_obj ↥(Mon.of G)) (Module k)ᵒᵖ (Module k)).obj (category_theory.groupoid.inv_functor (category_theory.single_obj ↥(Mon.of G)) ⋙ ((Action.functor_category_monoidal_equivalence (Module k) (Mon.of G)).to_lax_monoidal_functor.to_functor.obj A).op, (category_theory.is_left_adjoint.right (Action.functor_category_monoidal_equivalence (Module k) (Mon.of G)).to_lax_monoidal_functor.to_functor.inv).obj B)).obj punit.star).snd)) ↥((((category_theory.prod_functor_to_functor_prod (category_theory.single_obj ↥(Mon.of G)) (Module k)ᵒᵖ (Module k)).obj (category_theory.groupoid.inv_functor (category_theory.single_obj ↥(Mon.of G)) ⋙ ((Action.functor_category_monoidal_equivalence (Module k) (Mon.of G)).to_lax_monoidal_functor.to_functor.obj A).op, (category_theory.is_left_adjoint.right (Action.functor_category_monoidal_equivalence (Module k) (Mon.of G)).to_lax_monoidal_functor.to_functor.inv).obj B)).obj punit.star).snd)) linear_map.id.flip

Describes the counit in the adjunction A ⊗ - ⊣ iHom(A, -); given another k-linear G-representation B, the k-linear map underlying the resulting morphism A ⊗ iHom(A, B) ⟶ B is given by uncurrying the map A →ₗ[k] (A →ₗ[k] B) →ₗ[k] B defined by flipping the arguments in the identity map on Homₖ(A, B).

source
noncomputable def Rep.monoidal_closed.linear_hom_equiv {k G : Type u} [comm_ring k] [group G] (A B C : Rep k G) :
(A ⊗ B ⟶ C) ≃ₗ[k] B ⟶ (category_theory.ihom A).obj C

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

Equations
source
noncomputable def Rep.monoidal_closed.linear_hom_equiv_comm {k G : Type u} [comm_ring k] [group G] (A B C : Rep k G) :
(A ⊗ B ⟶ C) ≃ₗ[k] A ⟶ (category_theory.ihom B).obj C

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

Equations
source
theorem Rep.monoidal_closed.linear_hom_equiv_hom {k G : Type u} [comm_ring k] [group G] {A B C : Rep k G} (f : A ⊗ B ⟶ C) :
(⇑(Rep.monoidal_closed.linear_hom_equiv A B C) f).hom = (tensor_product.curry f.hom).flip
source
theorem Rep.monoidal_closed.linear_hom_equiv_comm_hom {k G : Type u} [comm_ring k] [group G] {A B C : Rep k G} (f : A ⊗ B ⟶ C) :
(⇑(Rep.monoidal_closed.linear_hom_equiv_comm A B C) f).hom = tensor_product.curry f.hom
source
theorem Rep.monoidal_closed.linear_hom_equiv_symm_hom {k G : Type u} [comm_ring k] [group G] {A B C : Rep k G} (f : B ⟶ (category_theory.ihom A).obj C) :
(⇑((Rep.monoidal_closed.linear_hom_equiv A B C).symm) f).hom = ⇑(tensor_product.uncurry k ↥A ↥B ↥C) (linear_map.flip f.hom)
source
theorem Rep.monoidal_closed.linear_hom_equiv_comm_symm_hom {k G : Type u} [comm_ring k] [group G] {A B C : Rep k G} (f : A ⟶ (category_theory.ihom B).obj C) :
(⇑((Rep.monoidal_closed.linear_hom_equiv_comm A B C).symm) f).hom = ⇑(tensor_product.uncurry k ↥A ↥B ↥C) f.hom
source
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) :
Rep.of (ρ.tprod τ) ≅ Rep.of ρ ⊗ Rep.of τ

Tautological isomorphism to help Lean in typechecking.

Equations
source
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) :
⇑((ρ.Rep_of_tprod_iso τ).hom.hom) x = x
source
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) :
⇑((ρ.Rep_of_tprod_iso τ).inv.hom) x = x

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