Documentation

Mathlib.RepresentationTheory.Basic

Monoid representations #

This file introduces monoid representations and their characters and defines a few ways to construct representations.

Main definitions #

Implementation notes #

Representations of a monoid G on a k-module V are implemented as homomorphisms G →* (V →ₗ[k] V).

@[inline, reducible]
abbrev Representation (k : Type u_1) (G : Type u_2) (V : Type u_3) [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] :
Type (max u_3 u_2)

A representation of G on the k-module V is a homomorphism G →* (V →ₗ[k] V).

Instances For
    def Representation.trivial (k : Type u_1) {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] :

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

    Instances For
      @[simp]
      theorem Representation.trivial_def (k : Type u_1) {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (g : G) (v : V) :
      ↑(↑(Representation.trivial k) g) v = v
      noncomputable def Representation.asAlgebraHom {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) :

      A k-linear representation of G on V can be thought of as an algebra map from MonoidAlgebra k G into the k-linear endomorphisms of V.

      Instances For
        theorem Representation.asAlgebraHom_def {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) :
        @[simp]
        theorem Representation.asAlgebraHom_single {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) (g : G) (r : k) :
        (↑(Representation.asAlgebraHom ρ) fun₀ | g => r) = r ρ g
        theorem Representation.asAlgebraHom_single_one {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) (g : G) :
        (↑(Representation.asAlgebraHom ρ) fun₀ | g => 1) = ρ g
        theorem Representation.asAlgebraHom_of {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) (g : G) :
        ↑(Representation.asAlgebraHom ρ) (↑(MonoidAlgebra.of k G) g) = ρ g
        def Representation.asModule {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] :
        Representation k G VType u_3

        If ρ : Representation k G V, then ρ.asModule is a type synonym for V, which we equip with an instance Module (MonoidAlgebra k G) ρ.asModule.

        You should use asModuleEquiv : ρ.asModule ≃+ V to translate terms.

        Instances For
          noncomputable instance Representation.asModuleModule {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) :

          A k-linear representation of G on V can be thought of as a module over MonoidAlgebra k G.

          def Representation.asModuleEquiv {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) :

          The additive equivalence from the Module (MonoidAlgebra k G) to the original vector space of the representative.

          This is just the identity, but it is helpful for typechecking and keeping track of instances.

          Instances For
            @[simp]
            @[simp]
            theorem Representation.asModuleEquiv_symm_map_smul {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) (r : k) (x : V) :
            @[simp]
            theorem Representation.asModuleEquiv_symm_map_rho {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) (g : G) (x : V) :
            noncomputable def Representation.ofModule' {k : Type u_1} {G : Type u_2} [CommSemiring k] [Monoid G] (M : Type u_4) [AddCommMonoid M] [Module k M] [Module (MonoidAlgebra k G) M] [IsScalarTower k (MonoidAlgebra k G) M] :

            Build a Representation k G M from a [Module (MonoidAlgebra k G) M].

            This version is not always what we want, as it relies on an existing [Module k M] instance, along with a [IsScalarTower k (MonoidAlgebra k G) M] instance.

            We remedy this below in ofModule (with the tradeoff that the representation is defined only on a type synonym of the original module.)

            Instances For
              noncomputable def Representation.ofModule {k : Type u_1} {G : Type u_2} [CommSemiring k] [Monoid G] (M : Type u_4) [AddCommMonoid M] [Module (MonoidAlgebra k G) M] :

              Build a Representation from a [Module (MonoidAlgebra k G) M].

              Note that the representation is built on restrictScalars k (MonoidAlgebra k G) M, rather than on M itself.

              Instances For

                ofModule and asModule are inverses. #

                This requires a little care in both directions: this is a categorical equivalence, not an isomorphism.

                See Rep.equivalenceModuleMonoidAlgebra for the full statement.

                Starting with ρ : Representation k G V, converting to a module and back again we have a Representation k G (restrictScalars k (MonoidAlgebra k G) ρ.asModule). To compare these, we use the composition of restrictScalarsAddEquiv and ρ.asModuleEquiv.

                Similarly, starting with Module (MonoidAlgebra k G) M, after we convert to a representation and back to a module, we have Module (MonoidAlgebra k G) (restrictScalars k (MonoidAlgebra k G) M).

                noncomputable def Representation.ofMulAction (k : Type u_1) [CommSemiring k] (G : Type u_2) [Monoid G] (H : Type u_3) [MulAction G H] :

                A G-action on H induces a representation G →* End(k[H]) in the natural way.

                Instances For
                  theorem Representation.ofMulAction_def {k : Type u_1} [CommSemiring k] {G : Type u_2} [Monoid G] {H : Type u_3} [MulAction G H] (g : G) :
                  ↑(Representation.ofMulAction k G H) g = Finsupp.lmapDomain k k ((fun x x_1 => x x_1) g)
                  theorem Representation.ofMulAction_single {k : Type u_1} [CommSemiring k] {G : Type u_2} [Monoid G] {H : Type u_3} [MulAction G H] (g : G) (x : H) (r : k) :
                  (↑(↑(Representation.ofMulAction k G H) g) fun₀ | x => r) = fun₀ | g x => r
                  @[simp]
                  theorem Representation.ofMulAction_apply {k : Type u_1} {G : Type u_2} [CommSemiring k] [Group G] {H : Type u_4} [MulAction G H] (g : G) (f : H →₀ k) (h : H) :
                  ↑(↑(↑(Representation.ofMulAction k G H) g) f) h = f (g⁻¹ h)
                  @[simp]
                  theorem Representation.ofMulActionSelfAsModuleEquiv_apply {k : Type u_1} {G : Type u_2} [CommSemiring k] [Group G] :
                  ∀ (a : Representation.asModule (Representation.ofMulAction k G G)), Representation.ofMulActionSelfAsModuleEquiv a = Equiv.toFun (Representation.asModuleEquiv (Representation.ofMulAction k G G)).toEquiv a
                  @[simp]
                  theorem Representation.ofMulActionSelfAsModuleEquiv_symm_apply {k : Type u_1} {G : Type u_2} [CommSemiring k] [Group G] :
                  ∀ (a : G →₀ k), ↑(LinearEquiv.symm Representation.ofMulActionSelfAsModuleEquiv) a = Equiv.invFun (Representation.asModuleEquiv (Representation.ofMulAction k G G)).toEquiv a

                  If we equip k[G] with the k-linear G-representation induced by the left regular action of G on itself, the resulting object is isomorphic as a k[G]-module to k[G] with its natural k[G]-module structure.

                  Instances For
                    def Representation.asGroupHom {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) :
                    G →* (V →ₗ[k] V)ˣ

                    When G is a group, a k-linear representation of G on V can be thought of as a group homomorphism from G into the invertible k-linear endomorphisms of V.

                    Instances For
                      theorem Representation.asGroupHom_apply {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) (g : G) :
                      ↑(↑(Representation.asGroupHom ρ) g) = ρ g
                      def Representation.tprod {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] [AddCommMonoid W] [Module k W] (ρV : Representation k G V) (ρW : Representation k G W) :

                      Given representations of G on V and W, there is a natural representation of G on their tensor product V ⊗[k] W.

                      Instances For
                        @[simp]
                        theorem Representation.tprod_apply {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] [AddCommMonoid W] [Module k W] (ρV : Representation k G V) (ρW : Representation k G W) (g : G) :
                        ↑(Representation.tprod ρV ρW) g = TensorProduct.map (ρV g) (ρW g)
                        theorem Representation.smul_tprod_one_asModule {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] [AddCommMonoid W] [Module k W] (ρV : Representation k G V) (r : MonoidAlgebra k G) (x : V) (y : W) :
                        let x' := x; let z := x ⊗ₜ[k] y; r z = (r x') ⊗ₜ[k] y
                        theorem Representation.smul_one_tprod_asModule {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] [AddCommMonoid W] [Module k W] (ρW : Representation k G W) (r : MonoidAlgebra k G) (x : V) (y : W) :
                        let y' := y; let z := x ⊗ₜ[k] y; r z = x ⊗ₜ[k] (r y')
                        def Representation.linHom {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] [AddCommMonoid W] [Module k W] (ρV : Representation k G V) (ρW : Representation k G W) :

                        Given representations of G on V and W, there is a natural representation of G on the module V →ₗ[k] W, where G acts by conjugation.

                        Instances For
                          @[simp]
                          theorem Representation.linHom_apply {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] [AddCommMonoid W] [Module k W] (ρV : Representation k G V) (ρW : Representation k G W) (g : G) (f : V →ₗ[k] W) :
                          ↑(↑(Representation.linHom ρV ρW) g) f = LinearMap.comp (ρW g) (LinearMap.comp f (ρV g⁻¹))
                          def Representation.dual {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] (ρV : Representation k G V) :

                          The dual of a representation ρ of G on a module V, given by (dual ρ) g f = f ∘ₗ (ρ g⁻¹), where f : Module.Dual k V.

                          Instances For
                            @[simp]
                            theorem Representation.dual_apply {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] (ρV : Representation k G V) (g : G) :
                            ↑(Representation.dual ρV) g = Module.Dual.transpose (ρV g⁻¹)
                            theorem Representation.dualTensorHom_comm {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] [AddCommMonoid W] [Module k W] (ρV : Representation k G V) (ρW : Representation k G W) (g : G) :

                            Given $k$-modules $V, W$, there is a homomorphism $φ : V^* ⊗ W → Hom_k(V, W)$ (implemented by LinearAlgebra.Contraction.dualTensorHom). Given representations of $G$ on $V$ and $W$,there are representations of $G$ on $V^* ⊗ W$ and on $Hom_k(V, W)$. This lemma says that $φ$ is $G$-linear.