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] [Monoid G] : Type (u + 1)

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

instance instLinearToSemiringToCommSemiringRepToRingInstCategoryActionModuleCatModuleCategoryOfInstPreadditiveActionInstCategoryActionInstPreadditiveModuleCatModuleCategory (k : Type u) (G : Type u) [CommRing k] [Monoid G] : CategoryTheory.Linear k (Rep k G)

instance Rep.instCoeSortRepToRingType {k : Type u} {G : Type u} [CommRing k] [Monoid G] : CoeSort (Rep k G) (Type u)

instance Rep.instAddCommGroupCoeRepToRingTypeInstCoeSortRepToRingType {k : Type u} {G : Type u} [CommRing k] [Monoid G] (V : Rep k G) : AddCommGroup (CoeSort.coe V)

instance Rep.instModuleCoeRepToRingTypeInstCoeSortRepToRingTypeToSemiringToCommSemiringToAddCommMonoidInstAddCommGroupCoeRepToRingTypeInstCoeSortRepToRingType {k : Type u} {G : Type u} [CommRing k] [Monoid G] (V : Rep k G) : Module k (CoeSort.coe V)

def Rep.ρ {k : Type u} {G : Type u} [CommRing k] [Monoid G] (V : Rep k G) : Representation k G (CoeSort.coe V)

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

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

Lift an unbundled representation to Rep.

@[simp]

theorem Rep.coe_of {k : Type u} {G : Type u} [CommRing k] [Monoid G] {V : Type u} [AddCommGroup V] [Module k V] (ρ : G →* V →ₗ[k] V) : CoeSort.coe (Rep.of ρ) = V

@[simp]

theorem Rep.of_ρ {k : Type u} {G : Type u} [CommRing k] [Monoid G] {V : Type u} [AddCommGroup V] [Module k V] (ρ : G →* V →ₗ[k] V) : Rep.ρ (Rep.of ρ) = ρ

theorem Rep.Action_ρ_eq_ρ {k : Type u} {G : Type u} [CommRing k] [Monoid G] {A : Rep k G} : A.ρ = Rep.ρ A

theorem Rep.of_ρ_apply {k : Type u} {G : Type u} [CommRing k] [Monoid G] {V : Type u} [AddCommGroup V] [Module k V] (ρ : Representation k G V) (g : ↑(MonCat.of G)) : ↑(Rep.ρ (Rep.of ρ)) 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} [CommRing k] {G : Type u} [Group G] (A : Rep k G) (g : G) (x : CoeSort.coe A) : ↑(↑(Rep.ρ A) g⁻¹) (↑(↑(Rep.ρ A) g) x) = x

@[simp]

theorem Rep.ρ_self_inv_apply {k : Type u} [CommRing k] {G : Type u} [Group G] {A : Rep k G} (g : G) (x : CoeSort.coe A) : ↑(↑(Rep.ρ A) g) (↑(↑(Rep.ρ A) g⁻¹) x) = x

theorem Rep.hom_comm_apply {k : Type u} {G : Type u} [CommRing k] [Monoid G] {A : Rep k G} {B : Rep k G} (f : A ⟶ B) (g : G) (x : CoeSort.coe A) : ↑f.hom (↑(↑(Rep.ρ A) g) x) = ↑(↑(Rep.ρ B) g) (↑f.hom x)

def Rep.trivial (k : Type u) (G : Type u) [CommRing k] [Monoid G] (V : Type u) [AddCommGroup V] [Module k V] : Rep k G

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

theorem Rep.trivial_def {k : Type u} {G : Type u} [CommRing k] [Monoid G] {V : Type u} [AddCommGroup V] [Module k V] (g : G) (v : V) : ↑(↑(Rep.ρ (Rep.trivial k G V)) g) v = v

noncomputable instance Rep.instPreservesLimitsRepToRingInstCategoryActionModuleCatModuleCategoryOfForget₂InstConcreteCategoryActionInstCategoryActionModuleConcreteCategoryHasForgetToV {k : Type u} {G : Type u} [CommRing k] [Monoid G] : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget₂ (Rep k G) (ModuleCat k))

noncomputable instance Rep.instPreservesColimitsRepToRingInstCategoryActionModuleCatModuleCategoryOfForget₂InstConcreteCategoryActionInstCategoryActionModuleConcreteCategoryHasForgetToV {k : Type u} {G : Type u} [CommRing k] [Monoid G] : CategoryTheory.Limits.PreservesColimits (CategoryTheory.forget₂ (Rep k G) (ModuleCat k))

theorem Rep.MonoidalCategory.braiding_hom_apply {k : Type u} {G : Type u} [CommRing k] [Monoid G] {A : Rep k G} {B : Rep k G} (x : CoeSort.coe A) (y : CoeSort.coe B) : ↑(β_ A B).hom.hom (x ⊗ₜ[k] y) = y ⊗ₜ[k] x

theorem Rep.MonoidalCategory.braiding_inv_apply {k : Type u} {G : Type u} [CommRing k] [Monoid G] {A : Rep k G} {B : Rep k G} (x : CoeSort.coe A) (y : CoeSort.coe B) : ↑(β_ A B).inv.hom (y ⊗ₜ[k] x) = x ⊗ₜ[k] y

noncomputable def Rep.linearization (k : Type u) (G : Type u) [CommRing k] [Monoid G] : CategoryTheory.MonoidalFunctor (Action (Type u) (MonCat.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].

@[simp]

theorem Rep.linearization_obj_ρ {k : Type u} {G : Type u} [CommRing k] [Monoid G] (X : Action (Type u) (MonCat.of G)) (g : G) (x : X.V →₀ k) : ↑(↑(Rep.ρ ((Rep.linearization k G).toLaxMonoidalFunctor.toFunctor.obj X)) g) x = ↑(Finsupp.lmapDomain k k (↑X.ρ g)) x

theorem Rep.linearization_of {k : Type u} {G : Type u} [CommRing k] [Monoid G] (X : Action (Type u) (MonCat.of G)) (g : G) (x : X.V) : (↑(↑(Rep.ρ ((Rep.linearization k G).toLaxMonoidalFunctor.toFunctor.obj X)) g) fun₀ | x => 1) = fun₀ | ↑X.ρ g x => 1

theorem Rep.linearization_single {k : Type u} {G : Type u} [CommRing k] [Monoid G] (X : Action (Type u) (MonCat.of G)) (g : G) (x : X.V) (r : k) : (↑(↑(Rep.ρ ((Rep.linearization k G).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} [CommRing k] [Monoid G] {X : Action (Type u) (MonCat.of G)} {Y : Action (Type u) (MonCat.of G)} (f : X ⟶ Y) : ((Rep.linearization k G).toLaxMonoidalFunctor.toFunctor.map f).hom = Finsupp.lmapDomain k k f.hom

theorem Rep.linearization_map_hom_single {k : Type u} {G : Type u} [CommRing k] [Monoid G] {X : Action (Type u) (MonCat.of G)} {Y : Action (Type u) (MonCat.of G)} (f : X ⟶ Y) (x : X.V) (r : k) : (↑((Rep.linearization k G).toLaxMonoidalFunctor.toFunctor.map f).hom fun₀ | x => r) = fun₀ | Action.Hom.hom (Type u) CategoryTheory.types (MonCat.of G) X Y f x => r

@[simp]

theorem Rep.linearization_μ_hom {k : Type u} {G : Type u} [CommRing k] [Monoid G] (X : Action (Type u) (MonCat.of G)) (Y : Action (Type u) (MonCat.of G)) : (CategoryTheory.LaxMonoidalFunctor.μ (Rep.linearization k G).toLaxMonoidalFunctor X Y).hom = ↑(finsuppTensorFinsupp' k X.V Y.V)

@[simp]

theorem Rep.linearization_μ_inv_hom {k : Type u} {G : Type u} [CommRing k] [Monoid G] (X : Action (Type u) (MonCat.of G)) (Y : Action (Type u) (MonCat.of G)) : (CategoryTheory.inv (CategoryTheory.LaxMonoidalFunctor.μ (Rep.linearization k G).toLaxMonoidalFunctor X Y)).hom = ↑(LinearEquiv.symm (finsuppTensorFinsupp' k X.V Y.V))

@[simp]

theorem Rep.linearization_ε_hom {k : Type u} {G : Type u} [CommRing k] [Monoid G] : (Rep.linearization k G).toLaxMonoidalFunctor.ε.hom = Finsupp.lsingle PUnit.unit

@[simp]

theorem Rep.linearization_ε_inv_hom_apply {k : Type u} {G : Type u} [CommRing k] [Monoid G] (r : k) : (↑(CategoryTheory.inv (Rep.linearization k G).toLaxMonoidalFunctor.ε).hom fun₀ | PUnit.unit => r) = r

@[simp]

theorem Rep.linearizationTrivialIso_hom_hom_apply (k : Type u) (G : Type u) [CommRing k] [Monoid G] (X : Type u) : ∀ (a : ↑((Rep.linearization k G).toLaxMonoidalFunctor.toFunctor.obj { V := X, ρ := 1 }).V), ↑(Rep.linearizationTrivialIso k G X).hom.hom a = a

@[simp]

theorem Rep.linearizationTrivialIso_inv_hom_apply (k : Type u) (G : Type u) [CommRing k] [Monoid G] (X : Type u) : ∀ (a : ↑((Rep.linearization k G).toLaxMonoidalFunctor.toFunctor.obj { V := X, ρ := 1 }).V), ↑(Rep.linearizationTrivialIso k G X).inv.hom a = a

noncomputable def Rep.linearizationTrivialIso (k : Type u) (G : Type u) [CommRing k] [Monoid G] (X : Type u) : (Rep.linearization k G).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].

@[inline, reducible]

noncomputable abbrev Rep.ofMulAction (k : Type u) (G : Type u) [CommRing k] [Monoid G] (H : Type u) [MulAction 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.leftRegular (k : Type u) (G : Type u) [CommRing k] [Monoid G] : Rep k G

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

noncomputable def Rep.diagonal (k : Type u) (G : Type u) [CommRing k] [Monoid G] (n : ℕ) : Rep k G

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

noncomputable def Rep.linearizationOfMulActionIso (k : Type u) (G : Type u) [CommRing k] [Monoid G] (H : Type u) [MulAction G H] : (Rep.linearization k G).toLaxMonoidalFunctor.toFunctor.obj (Action.ofMulAction G H) ≅ Rep.ofMulAction 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.

@[simp]

theorem Rep.leftRegularHom_hom {k : Type u} {G : Type u} [CommRing k] [Monoid G] (A : Rep k G) (x : CoeSort.coe A) : (Rep.leftRegularHom A x).hom = ↑(Finsupp.lift ((fun x => CoeSort.coe A) x) k G) fun g => ↑(↑(Rep.ρ A) g) x

noncomputable def Rep.leftRegularHom {k : Type u} {G : Type u} [CommRing k] [Monoid G] (A : Rep k G) (x : CoeSort.coe A) : Rep.ofMulAction k G G ⟶ A

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

theorem Rep.leftRegularHom_apply {k : Type u} {G : Type u} [CommRing k] [Monoid G] {A : Rep k G} (x : CoeSort.coe A) : (↑(Rep.leftRegularHom A x).hom fun₀ | 1 => 1) = x

@[simp]

theorem Rep.leftRegularHomEquiv_symm_apply {k : Type u} {G : Type u} [CommRing k] [Monoid G] (A : Rep k G) (x : CoeSort.coe A) : ↑(LinearEquiv.symm (Rep.leftRegularHomEquiv A)) x = Rep.leftRegularHom A x

@[simp]

theorem Rep.leftRegularHomEquiv_apply {k : Type u} {G : Type u} [CommRing k] [Monoid G] (A : Rep k G) (f : Rep.ofMulAction k G G ⟶ A) : ↑(Rep.leftRegularHomEquiv A) f = ↑f.hom fun₀ | 1 => 1

noncomputable def Rep.leftRegularHomEquiv {k : Type u} {G : Type u} [CommRing k] [Monoid G] (A : Rep k G) : (Rep.ofMulAction k G G ⟶ A) ≃ₗ[k] CoeSort.coe A

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

theorem Rep.leftRegularHomEquiv_symm_single {k : Type u} {G : Type u} [CommRing k] [Monoid G] {A : Rep k G} (x : CoeSort.coe A) (g : G) : (↑(↑(LinearEquiv.symm (Rep.leftRegularHomEquiv A)) x).hom fun₀ | g => 1) = ↑(↑(Rep.ρ A) g) x

@[simp]

theorem Rep.ihom_map_hom {k : Type u} {G : Type u} [CommRing k] [Group G] (A : Rep k G) {X : Rep k G} {Y : Rep k G} (f : X ⟶ Y) : ((Rep.ihom A).map f).hom = ModuleCat.ofHom (↑(LinearMap.llcomp k (CoeSort.coe A) ↑X.V ↑Y.V) f.hom)

@[simp]

theorem Rep.ihom_obj {k : Type u} {G : Type u} [CommRing k] [Group G] (A : Rep k G) (B : Rep k G) : (Rep.ihom A).obj B = Rep.of (Representation.linHom (Rep.ρ A) (Rep.ρ B))

def Rep.ihom {k : Type u} {G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.Functor (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⁻¹).

@[simp]

theorem Rep.ihom_obj_ρ_apply {k : Type u} {G : Type u} [CommRing k] [Group G] {A : Rep k G} {B : Rep k G} (g : G) (x : CoeSort.coe A →ₗ[k] CoeSort.coe B) : ↑(↑(Rep.ρ ((Rep.ihom A).obj B)) g) x = LinearMap.comp (↑(Rep.ρ B) g) (LinearMap.comp x (↑(Rep.ρ A) g⁻¹))

def Rep.homEquiv {k : Type u} {G : Type u} [CommRing k] [Group G] (A : Rep k G) (B : Rep k G) (C : Rep k G) : (CategoryTheory.MonoidalCategory.tensorObj A B ⟶ C) ≃ (B ⟶ (Rep.ihom A).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.

theorem Rep.homEquiv_apply_hom {k : Type u} {G : Type u} [CommRing k] [Group G] {A : Rep k G} {B : Rep k G} {C : Rep k G} (f : CategoryTheory.MonoidalCategory.tensorObj A B ⟶ C) : (↑(Rep.homEquiv A B C) f).hom = LinearMap.flip (TensorProduct.curry 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} [CommRing k] [Group G] {A : Rep k G} {B : Rep k G} {C : Rep k G} (f : B ⟶ (Rep.ihom A).obj C) : (↑(Rep.homEquiv A B C).symm f).hom = ↑(TensorProduct.uncurry k (CoeSort.coe A) (CoeSort.coe B) (CoeSort.coe C)) (LinearMap.flip f.hom)

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

instance Rep.instMonoidalClosedRepToRingToMonoidToDivInvMonoidInstCategoryActionModuleCatModuleCategoryOfInstMonoidalCategoryActionInstCategoryActionMonoidalCategory {k : Type u} {G : Type u} [CommRing k] [Group G] : CategoryTheory.MonoidalClosed (Rep k G)

@[simp]

theorem Rep.ihom_obj_ρ_def {k : Type u} {G : Type u} [CommRing k] [Group G] (A : Rep k G) (B : Rep k G) : Rep.ρ ((CategoryTheory.ihom A).obj B) = Rep.ρ ((Rep.ihom A).obj B)

@[simp]

theorem Rep.homEquiv_def {k : Type u} {G : Type u} [CommRing k] [Group G] (A : Rep k G) (B : Rep k G) (C : Rep k G) : CategoryTheory.Adjunction.homEquiv (CategoryTheory.ihom.adjunction A) B C = Rep.homEquiv A B C

@[simp]

theorem Rep.ihom_ev_app_hom {k : Type u} {G : Type u} [CommRing k] [Group G] (A : Rep k G) (B : Rep k G) : ((CategoryTheory.ihom.ev A).app B).hom = ↑(TensorProduct.uncurry k (CoeSort.coe A) (CoeSort.coe A →ₗ[k] CoeSort.coe B) (CoeSort.coe B)) (LinearMap.flip LinearMap.id)

@[simp]

theorem Rep.ihom_coev_app_hom {k : Type u} {G : Type u} [CommRing k] [Group G] (A : Rep k G) (B : Rep k G) : ((CategoryTheory.ihom.coev A).app B).hom = LinearMap.flip (TensorProduct.mk k (CoeSort.coe A) ↑((CategoryTheory.Functor.id (Rep k G)).obj B).V)

def Rep.MonoidalClosed.linearHomEquiv {k : Type u} {G : Type u} [CommRing k] [Group G] (A : Rep k G) (B : Rep k G) (C : Rep k G) : (CategoryTheory.MonoidalCategory.tensorObj A B ⟶ C) ≃ₗ[k] B ⟶ (CategoryTheory.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)).

def Rep.MonoidalClosed.linearHomEquivComm {k : Type u} {G : Type u} [CommRing k] [Group G] (A : Rep k G) (B : Rep k G) (C : Rep k G) : (CategoryTheory.MonoidalCategory.tensorObj A B ⟶ C) ≃ₗ[k] A ⟶ (CategoryTheory.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)).

@[simp]

theorem Rep.MonoidalClosed.linearHomEquiv_hom {k : Type u} {G : Type u} [CommRing k] [Group G] {A : Rep k G} {B : Rep k G} {C : Rep k G} (f : CategoryTheory.MonoidalCategory.tensorObj A B ⟶ C) : (↑(Rep.MonoidalClosed.linearHomEquiv A B C) f).hom = LinearMap.flip (TensorProduct.curry f.hom)

@[simp]

theorem Rep.MonoidalClosed.linearHomEquivComm_hom {k : Type u} {G : Type u} [CommRing k] [Group G] {A : Rep k G} {B : Rep k G} {C : Rep k G} (f : CategoryTheory.MonoidalCategory.tensorObj A B ⟶ C) : (↑(Rep.MonoidalClosed.linearHomEquivComm A B C) f).hom = TensorProduct.curry f.hom

@[simp]

theorem Rep.MonoidalClosed.linearHomEquiv_symm_hom {k : Type u} {G : Type u} [CommRing k] [Group G] {A : Rep k G} {B : Rep k G} {C : Rep k G} (f : B ⟶ (CategoryTheory.ihom A).obj C) : (↑(LinearEquiv.symm (Rep.MonoidalClosed.linearHomEquiv A B C)) f).hom = ↑(TensorProduct.uncurry k (CoeSort.coe A) (CoeSort.coe B) (CoeSort.coe C)) (LinearMap.flip f.hom)

@[simp]

theorem Rep.MonoidalClosed.linearHomEquivComm_symm_hom {k : Type u} {G : Type u} [CommRing k] [Group G] {A : Rep k G} {B : Rep k G} {C : Rep k G} (f : A ⟶ (CategoryTheory.ihom B).obj C) : (↑(LinearEquiv.symm (Rep.MonoidalClosed.linearHomEquivComm A B C)) f).hom = ↑(TensorProduct.uncurry k (CoeSort.coe A) (CoeSort.coe B) (CoeSort.coe C)) f.hom

def Representation.repOfTprodIso {k : Type u} {G : Type u} [CommRing k] [Monoid G] {V : Type u} {W : Type u} [AddCommGroup V] [AddCommGroup W] [Module k V] [Module k W] (ρ : Representation k G V) (τ : Representation k G W) : Rep.of (Representation.tprod ρ τ) ≅ CategoryTheory.MonoidalCategory.tensorObj (Rep.of ρ) (Rep.of τ)

Tautological isomorphism to help Lean in typechecking.

theorem Representation.repOfTprodIso_apply {k : Type u} {G : Type u} [CommRing k] [Monoid G] {V : Type u} {W : Type u} [AddCommGroup V] [AddCommGroup W] [Module k V] [Module k W] (ρ : Representation k G V) (τ : Representation k G W) (x : TensorProduct k V W) : ↑(Representation.repOfTprodIso ρ τ).hom.hom x = x

theorem Representation.repOfTprodIso_inv_apply {k : Type u} {G : Type u} [CommRing k] [Monoid G] {V : Type u} {W : Type u} [AddCommGroup V] [AddCommGroup W] [Module k V] [Module k W] (ρ : Representation k G V) (τ : Representation k G W) (x : TensorProduct k V W) : ↑(Representation.repOfTprodIso ρ τ).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} [CommRing k] [Monoid G] (V : Type u_3) (W : Type u_4) [AddCommGroup V] [AddCommGroup W] [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 : MonoidAlgebra k G) (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} [CommRing k] [Monoid G] {V : Rep k G} {W : Rep k G} (f : V ⟶ W) : ModuleCat.of (MonoidAlgebra k G) (Representation.asModule (Rep.ρ V)) ⟶ ModuleCat.of (MonoidAlgebra k G) (Representation.asModule (Rep.ρ W))

Auxiliary definition for toModuleMonoidAlgebra.

def Rep.toModuleMonoidAlgebra {k : Type u} {G : Type u} [CommRing k] [Monoid G] : CategoryTheory.Functor (Rep k G) (ModuleCat (MonoidAlgebra k G))

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

def Rep.ofModuleMonoidAlgebra {k : Type u} {G : Type u} [CommRing k] [Monoid G] : CategoryTheory.Functor (ModuleCat (MonoidAlgebra k G)) (Rep k G)

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

theorem Rep.ofModuleMonoidAlgebra_obj_coe {k : Type u} {G : Type u} [CommRing k] [Monoid G] (M : ModuleCat (MonoidAlgebra k G)) : CoeSort.coe (Rep.ofModuleMonoidAlgebra.obj M) = RestrictScalars k (MonoidAlgebra k G) ↑M

theorem Rep.ofModuleMonoidAlgebra_obj_ρ {k : Type u} {G : Type u} [CommRing k] [Monoid G] (M : ModuleCat (MonoidAlgebra k G)) : Rep.ρ (Rep.ofModuleMonoidAlgebra.obj M) = Representation.ofModule ↑M

def Rep.counitIsoAddEquiv {k : Type u} {G : Type u} [CommRing k] [Monoid G] {M : ModuleCat (MonoidAlgebra k G)} : ↑((CategoryTheory.Functor.comp Rep.ofModuleMonoidAlgebra Rep.toModuleMonoidAlgebra).obj M) ≃+ ↑M

Auxiliary definition for equivalenceModuleMonoidAlgebra.

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

Auxiliary definition for equivalenceModuleMonoidAlgebra.

def Rep.counitIso {k : Type u} {G : Type u} [CommRing k] [Monoid G] (M : ModuleCat (MonoidAlgebra k G)) : (CategoryTheory.Functor.comp Rep.ofModuleMonoidAlgebra Rep.toModuleMonoidAlgebra).obj M ≅ M

Auxiliary definition for equivalenceModuleMonoidAlgebra.

theorem Rep.unit_iso_comm {k : Type u} {G : Type u} [CommRing k] [Monoid G] (V : Rep k G) (g : G) (x : CoeSort.coe V) : ↑Rep.unitIsoAddEquiv (AddHom.toFun (↑(Rep.ρ V) g).toAddHom x) = AddHom.toFun (↑(Rep.ρ (Rep.ofModuleMonoidAlgebra.obj (Rep.toModuleMonoidAlgebra.obj V))) g).toAddHom (↑Rep.unitIsoAddEquiv x)

def Rep.unitIso {k : Type u} {G : Type u} [CommRing k] [Monoid G] (V : Rep k G) : V ≅ (CategoryTheory.Functor.comp Rep.toModuleMonoidAlgebra Rep.ofModuleMonoidAlgebra).obj V

Auxiliary definition for equivalenceModuleMonoidAlgebra.

def Rep.equivalenceModuleMonoidAlgebra {k : Type u} {G : Type u} [CommRing k] [Monoid G] : Rep k G ≌ ModuleCat (MonoidAlgebra k G)

The categorical equivalence Rep k G ≌ ModuleCat (MonoidAlgebra k G).