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.

@[reducible, inline]
noncomputable 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.

Equations
Instances For
    noncomputable instance instLinearRep (k : Type u) (G : Type u) [CommRing k] [Monoid G] :
    Equations
    noncomputable instance Rep.instCoeSortType {k : Type u} {G : Type u} [CommRing k] [Monoid G] :
    CoeSort (Rep k G) (Type u)
    Equations
    noncomputable instance Rep.instAddCommGroupCoe {k : Type u} {G : Type u} [CommRing k] [Monoid G] (V : Rep k G) :
    Equations
    • V.instAddCommGroupCoe = let_fun this := inferInstance; this
    noncomputable instance Rep.instModuleCoe {k : Type u} {G : Type u} [CommRing k] [Monoid G] (V : Rep k G) :
    Equations
    • V.instModuleCoe = let_fun this := inferInstance; this
    noncomputable def Rep.ρ {k : Type u} {G : Type u} [CommRing k] [Monoid G] (V : Rep k G) :

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

    Equations
    • V = V
    Instances For
      noncomputable 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.

      Equations
      Instances For
        @[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) :
        @[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.of ρ) = ρ
        theorem Rep.Action_ρ_eq_ρ {k : Type u} {G : Type u} [CommRing k] [Monoid G] {A : Rep k G} :
        A = 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.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) :
        (A g⁻¹) ((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) :
        (A g) ((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 ((A g) x) = (B g) (f.hom x)
        noncomputable 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.

        Equations
        Instances For
          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.trivial k G V) g) v = v
          @[reducible, inline]
          noncomputable abbrev Rep.IsTrivial {k : Type u} {G : Type u} [CommRing k] [Monoid G] (A : Rep k G) :

          A predicate for representations that fix every element.

          Equations
          • A.IsTrivial = A.IsTrivial
          Instances For
            noncomputable instance Rep.instIsTrivialTrivial {k : Type u} {G : Type u} [CommRing k] [Monoid G] {V : Type u} [AddCommGroup V] [Module k V] :
            (Rep.trivial k G V).IsTrivial
            Equations
            • =
            noncomputable instance Rep.instIsTrivialOfOfIsTrivial {k : Type u} {G : Type u} [CommRing k] [Monoid G] {V : Type u} [AddCommGroup V] [Module k V] (ρ : Representation k G V) [ρ.IsTrivial] :
            (Rep.of ρ).IsTrivial
            Equations
            • =
            Equations
            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] :

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

            Equations
            Instances For
              @[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.linearization k G).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.linearization k G).obj X) g) (Finsupp.single x 1) = Finsupp.single (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.linearization k G).obj X) g) (Finsupp.single x r) = Finsupp.single (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).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).map f).hom (Finsupp.single x r) = Finsupp.single (f.hom 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)) :
              ((Rep.linearization k G) 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 ((Rep.linearization k G) X Y)).hom = (finsuppTensorFinsupp' k X.V Y.V).symm
              noncomputable def Rep.linearizationTrivialIso (k : Type u) (G : Type u) [CommRing k] [Monoid G] (X : Type u) :
              (Rep.linearization k G).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
              Instances For
                @[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).obj { V := X, ρ := 1 }).V) :
                (Rep.linearizationTrivialIso k G X).inv.hom a = a
                @[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).obj { V := X, ρ := 1 }).V) :
                (Rep.linearizationTrivialIso k G X).hom.hom a = a
                @[reducible, inline]
                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.

                Equations
                Instances For
                  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.

                  Equations
                  Instances For
                    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.

                    Equations
                    Instances For
                      noncomputable def Rep.linearizationOfMulActionIso (k : Type u) (G : Type u) [CommRing k] [Monoid G] (H : Type u) [MulAction 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
                      Instances For
                        noncomputable def Rep.ofDistribMulAction (k : Type u) (G : Type u) (A : Type u) [CommRing k] [Monoid G] [AddCommGroup A] [Module k A] [DistribMulAction G A] [SMulCommClass G k A] :
                        Rep k G

                        Turns a k-module A with a compatible DistribMulAction of a monoid G into a k-linear G-representation on A.

                        Equations
                        Instances For
                          @[simp]
                          theorem Rep.ofDistribMulAction_ρ_apply_apply (k : Type u) (G : Type u) (A : Type u) [CommRing k] [Monoid G] [AddCommGroup A] [Module k A] [DistribMulAction G A] [SMulCommClass G k A] (g : G) (a : A) :
                          ((Rep.ofDistribMulAction k G A) g) a = g a
                          noncomputable def Rep.ofAlgebraAut (R : Type) (S : Type) [CommRing R] [CommRing S] [Algebra R S] :

                          Given an R-algebra S, the -linear representation associated to the natural action of S ≃ₐ[R] S on S.

                          Equations
                          Instances For
                            noncomputable def Rep.ofMulDistribMulAction (M : Type) (G : Type) [Monoid M] [CommGroup G] [MulDistribMulAction M G] :

                            Turns a CommGroup G with a MulDistribMulAction of a monoid M into a -linear M-representation on Additive G.

                            Equations
                            Instances For
                              @[simp]
                              theorem Rep.ofMulDistribMulAction_ρ_apply_apply (M : Type) (G : Type) [Monoid M] [CommGroup G] [MulDistribMulAction M G] (g : M) (a : Additive G) :
                              ((Rep.ofMulDistribMulAction M G) g) a = Additive.ofMul (g Additive.toMul a)
                              noncomputable def Rep.ofAlgebraAutOnUnits (R : Type) (S : Type) [CommRing R] [CommRing S] [Algebra R S] :

                              Given an R-algebra S, the -linear representation associated to the natural action of S ≃ₐ[R] S on .

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

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

                                Equations
                                • A.leftRegularHom x = { hom := (Finsupp.lift (A.V) k G) fun (g : G) => (A g) x, comm := }
                                Instances For
                                  @[simp]
                                  theorem Rep.leftRegularHom_hom {k : Type u} {G : Type u} [CommRing k] [Monoid G] (A : Rep k G) (x : CoeSort.coe A) :
                                  (A.leftRegularHom x).hom = (Finsupp.lift (A.V) k G) fun (g : 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) :
                                  (A.leftRegularHom x).hom (Finsupp.single 1 1) = x
                                  noncomputable def Rep.leftRegularHomEquiv {k : Type u} {G : Type u} [CommRing 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
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    @[simp]
                                    theorem Rep.leftRegularHomEquiv_symm_apply {k : Type u} {G : Type u} [CommRing k] [Monoid G] (A : Rep k G) (x : CoeSort.coe A) :
                                    A.leftRegularHomEquiv.symm x = A.leftRegularHom 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) :
                                    A.leftRegularHomEquiv f = f.hom (Finsupp.single 1 1)
                                    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) :
                                    (A.leftRegularHomEquiv.symm x).hom (Finsupp.single g 1) = (A g) x
                                    noncomputable def Rep.ihom {k : Type u} {G : Type u} [CommRing k] [Group G] (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⁻¹).

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      @[simp]
                                      theorem Rep.ihom_obj {k : Type u} {G : Type u} [CommRing k] [Group G] (A : Rep k G) (B : Rep k G) :
                                      A.ihom.obj B = Rep.of (A.linHom B)
                                      @[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) :
                                      (A.ihom.map f).hom = ModuleCat.ofHom ((LinearMap.llcomp k (CoeSort.coe A) (CoeSort.coe X) (CoeSort.coe Y)) f.hom)
                                      @[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) :
                                      ((A.ihom.obj B) g) x = B g ∘ₗ x ∘ₗ A g⁻¹
                                      noncomputable 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) :

                                      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
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        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) :
                                        ((A.homEquiv B C) f).hom = (TensorProduct.curry f.hom).flip

                                        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 A.ihom.obj C) :
                                        ((A.homEquiv 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.

                                        noncomputable instance Rep.instMonoidalClosed {k : Type u} {G : Type u} [CommRing k] [Group G] :
                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        @[simp]
                                        theorem Rep.ihom_obj_ρ_def {k : Type u} {G : Type u} [CommRing k] [Group G] (A : Rep k G) (B : Rep k G) :
                                        ((CategoryTheory.ihom A).obj B) = (A.ihom.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.ihom.adjunction A).homEquiv B C = A.homEquiv 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) :
                                        @[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 = (TensorProduct.mk k (CoeSort.coe A) ((CategoryTheory.Functor.id (Rep k G)).obj B).V).flip
                                        noncomputable 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) :

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

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          noncomputable 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) :

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

                                          Equations
                                          Instances For
                                            @[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) :
                                            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) :
                                            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) :
                                            noncomputable 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) :

                                            Tautological isomorphism to help Lean in typechecking.

                                            Equations
                                            Instances For
                                              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) :
                                              (ρ.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) :
                                              (ρ.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), f ∘ₗ ρ g = σ 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.

                                              noncomputable 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) V.asModule ModuleCat.of (MonoidAlgebra k G) W.asModule

                                              Auxiliary definition for toModuleMonoidAlgebra.

                                              Equations
                                              Instances For
                                                noncomputable def Rep.toModuleMonoidAlgebra {k : Type u} {G : Type u} [CommRing k] [Monoid G] :

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

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  noncomputable def Rep.ofModuleMonoidAlgebra {k : Type u} {G : Type u} [CommRing k] [Monoid G] :

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

                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For
                                                    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.ofModuleMonoidAlgebra.obj M) = Representation.ofModule M
                                                    noncomputable def Rep.counitIsoAddEquiv {k : Type u} {G : Type u} [CommRing k] [Monoid G] {M : ModuleCat (MonoidAlgebra k G)} :
                                                    ((Rep.ofModuleMonoidAlgebra.comp Rep.toModuleMonoidAlgebra).obj M) ≃+ M

                                                    Auxiliary definition for equivalenceModuleMonoidAlgebra.

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

                                                      Auxiliary definition for equivalenceModuleMonoidAlgebra.

                                                      Equations
                                                      Instances For
                                                        noncomputable def Rep.counitIso {k : Type u} {G : Type u} [CommRing k] [Monoid G] (M : ModuleCat (MonoidAlgebra k G)) :
                                                        (Rep.ofModuleMonoidAlgebra.comp Rep.toModuleMonoidAlgebra).obj M M

                                                        Auxiliary definition for equivalenceModuleMonoidAlgebra.

                                                        Equations
                                                        • Rep.counitIso M = (let __src := Rep.counitIsoAddEquiv; { toFun := __src.toFun, map_add' := , map_smul' := , invFun := __src.invFun, left_inv := , right_inv := }).toModuleIso'
                                                        Instances For
                                                          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 ((V g).toFun x) = ((Rep.ofModuleMonoidAlgebra.obj (Rep.toModuleMonoidAlgebra.obj V)) g).toFun (Rep.unitIsoAddEquiv x)
                                                          noncomputable def Rep.unitIso {k : Type u} {G : Type u} [CommRing k] [Monoid G] (V : Rep k G) :
                                                          V (Rep.toModuleMonoidAlgebra.comp Rep.ofModuleMonoidAlgebra).obj V

                                                          Auxiliary definition for equivalenceModuleMonoidAlgebra.

                                                          Equations
                                                          • One or more equations did not get rendered due to their size.
                                                          Instances For
                                                            noncomputable def Rep.equivalenceModuleMonoidAlgebra {k : Type u} {G : Type u} [CommRing k] [Monoid G] :

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

                                                            Equations
                                                            • One or more equations did not get rendered due to their size.
                                                            Instances For