Documentation

Mathlib.RepresentationTheory.Action.Basic

Action V G, the category of actions of a monoid G inside some category V. #

The prototypical example is V = ModuleCat R, where Action (ModuleCat R) G is the category of R-linear representations of G.

We check Action V G ≌ (CategoryTheory.singleObj G ⥤ V), and construct the restriction functors res {G H : MonCat} (f : G ⟶ H) : Action V H ⥤ Action V G.

structure Action (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) :
Type (u + 1)

An Action V G represents a bundled action of the monoid G on an object of some category V.

As an example, when V = ModuleCat R, this is an R-linear representation of G, while when V = Type this is a G-action.

Instances For
    @[simp]
    theorem Action.ρ_one {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} (A : Action V G) :
    def Action.ρAut {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : Grp} (A : Action V (MonCat.of G)) :

    When a group acts, we can lift the action to the group of automorphisms.

    Equations
    • A.ρAut = { toFun := fun (g : G) => { hom := A g, inv := A g⁻¹, hom_inv_id := , inv_hom_id := }, map_one' := , map_mul' := }
    Instances For
      @[simp]
      theorem Action.ρAut_apply_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : Grp} (A : Action V (MonCat.of G)) (g : G) :
      (A.ρAut g).hom = A g
      @[simp]
      theorem Action.ρAut_apply_inv {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : Grp} (A : Action V (MonCat.of G)) (g : G) :
      (A.ρAut g).inv = A g⁻¹
      Equations

      The trivial representation of a group.

      Equations
      Instances For
        structure Action.Hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} (M : Action V G) (N : Action V G) :

        A homomorphism of Action V Gs is a morphism between the underlying objects, commuting with the action of G.

        Instances For
          theorem Action.Hom.ext {V : Type (u + 1)} :
          ∀ {inst : CategoryTheory.LargeCategory V} {G : MonCat} {M N : Action V G} {x y : M.Hom N}, x.hom = y.homx = y
          theorem Action.Hom.comm {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} {M : Action V G} {N : Action V G} (self : M.Hom N) (g : G) :
          theorem Action.Hom.comm_assoc {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} {M : Action V G} {N : Action V G} (self : M.Hom N) (g : G) {Z : V} (h : N.V Z) :
          def Action.Hom.id {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} (M : Action V G) :
          M.Hom M

          The identity morphism on an Action V G.

          Equations
          Instances For
            instance Action.Hom.instInhabited {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} (M : Action V G) :
            Inhabited (M.Hom M)
            Equations
            def Action.Hom.comp {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} {M : Action V G} {N : Action V G} {K : Action V G} (p : M.Hom N) (q : N.Hom K) :
            M.Hom K

            The composition of two Action V G homomorphisms is the composition of the underlying maps.

            Equations
            Instances For
              @[simp]
              theorem Action.Hom.comp_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} {M : Action V G} {N : Action V G} {K : Action V G} (p : M.Hom N) (q : N.Hom K) :
              (p.comp q).hom = CategoryTheory.CategoryStruct.comp p.hom q.hom
              Equations
              theorem Action.hom_ext {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} {M : Action V G} {N : Action V G} (φ₁ : M N) (φ₂ : M N) (h : φ₁.hom = φ₂.hom) :
              φ₁ = φ₂
              @[simp]
              theorem Action.comp_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} {M : Action V G} {N : Action V G} {K : Action V G} (f : M N) (g : N K) :
              @[simp]
              theorem Action.hom_inv_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} {M : Action V G} {N : Action V G} (f : M N) :
              @[simp]
              theorem Action.inv_hom_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} {M : Action V G} {N : Action V G} (f : M N) :
              def Action.mkIso {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} {M : Action V G} {N : Action V G} (f : M.V N.V) (comm : autoParam (∀ (g : G), CategoryTheory.CategoryStruct.comp (M g) f.hom = CategoryTheory.CategoryStruct.comp f.hom (N g)) _auto✝) :
              M N

              Construct an isomorphism of G actions/representations from an isomorphism of the underlying objects, where the forward direction commutes with the group action.

              Equations
              • Action.mkIso f comm = { hom := { hom := f.hom, comm := comm }, inv := { hom := f.inv, comm := }, hom_inv_id := , inv_hom_id := }
              Instances For
                @[simp]
                theorem Action.mkIso_hom_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} {M : Action V G} {N : Action V G} (f : M.V N.V) (comm : autoParam (∀ (g : G), CategoryTheory.CategoryStruct.comp (M g) f.hom = CategoryTheory.CategoryStruct.comp f.hom (N g)) _auto✝) :
                (Action.mkIso f comm).hom.hom = f.hom
                @[simp]
                theorem Action.mkIso_inv_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} {M : Action V G} {N : Action V G} (f : M.V N.V) (comm : autoParam (∀ (g : G), CategoryTheory.CategoryStruct.comp (M g) f.hom = CategoryTheory.CategoryStruct.comp f.hom (N g)) _auto✝) :
                (Action.mkIso f comm).inv.hom = f.inv
                @[instance 100]
                instance Action.isIso_of_hom_isIso {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} {M : Action V G} {N : Action V G} (f : M N) [CategoryTheory.IsIso f.hom] :
                Equations
                • =
                instance Action.isIso_hom_mk {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} {M : Action V G} {N : Action V G} (f : M.V N.V) [CategoryTheory.IsIso f] (w : ∀ (g : G), CategoryTheory.CategoryStruct.comp (M g) f = CategoryTheory.CategoryStruct.comp f (N g)) :
                CategoryTheory.IsIso { hom := f, comm := w }
                Equations
                • =
                instance Action.instIsIsoHomHom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} {M : Action V G} {N : Action V G} (f : M N) :
                Equations
                • =
                instance Action.instIsIsoHomInv {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} {M : Action V G} {N : Action V G} (f : M N) :
                Equations
                • =

                Auxiliary definition for functorCategoryEquivalence.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  @[simp]
                  theorem Action.FunctorCategoryEquivalence.functor_obj_map {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} (M : Action V G) :
                  ∀ {X Y : CategoryTheory.SingleObj G} (g : X Y), (Action.FunctorCategoryEquivalence.functor.obj M).map g = M g
                  @[simp]
                  theorem Action.FunctorCategoryEquivalence.functor_obj_obj {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} (M : Action V G) :
                  ∀ (x : CategoryTheory.SingleObj G), (Action.FunctorCategoryEquivalence.functor.obj M).obj x = M.V
                  @[simp]
                  theorem Action.FunctorCategoryEquivalence.functor_map_app {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} :
                  ∀ {X Y : Action V G} (f : X Y) (x : CategoryTheory.SingleObj G), (Action.FunctorCategoryEquivalence.functor.map f).app x = f.hom

                  Auxiliary definition for functorCategoryEquivalence.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    @[simp]
                    theorem Action.FunctorCategoryEquivalence.inverse_obj_V {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} (F : CategoryTheory.Functor (CategoryTheory.SingleObj G) V) :
                    (Action.FunctorCategoryEquivalence.inverse.obj F).V = F.obj PUnit.unit
                    @[simp]
                    theorem Action.FunctorCategoryEquivalence.inverse_obj_ρ_apply {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} (F : CategoryTheory.Functor (CategoryTheory.SingleObj G) V) (g : G) :
                    (Action.FunctorCategoryEquivalence.inverse.obj F) g = F.map g
                    @[simp]
                    theorem Action.FunctorCategoryEquivalence.inverse_map_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} :
                    ∀ {X Y : CategoryTheory.Functor (CategoryTheory.SingleObj G) V} (f : X Y), (Action.FunctorCategoryEquivalence.inverse.map f).hom = f.app PUnit.unit
                    def Action.FunctorCategoryEquivalence.unitIso {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} :
                    CategoryTheory.Functor.id (Action V G) Action.FunctorCategoryEquivalence.functor.comp Action.FunctorCategoryEquivalence.inverse

                    Auxiliary definition for functorCategoryEquivalence.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      @[simp]
                      theorem Action.FunctorCategoryEquivalence.unitIso_hom_app_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} (X : Action V G) :
                      (Action.FunctorCategoryEquivalence.unitIso.hom.app X).hom = CategoryTheory.CategoryStruct.id X.V
                      @[simp]
                      theorem Action.FunctorCategoryEquivalence.unitIso_inv_app_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} (X : Action V G) :
                      (Action.FunctorCategoryEquivalence.unitIso.inv.app X).hom = CategoryTheory.CategoryStruct.id X.V
                      def Action.FunctorCategoryEquivalence.counitIso {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} :
                      Action.FunctorCategoryEquivalence.inverse.comp Action.FunctorCategoryEquivalence.functor CategoryTheory.Functor.id (CategoryTheory.Functor (CategoryTheory.SingleObj G) V)

                      Auxiliary definition for functorCategoryEquivalence.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        @[simp]
                        theorem Action.FunctorCategoryEquivalence.counitIso_inv_app_app {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} (X : CategoryTheory.Functor (CategoryTheory.SingleObj G) V) (X : CategoryTheory.SingleObj G) :
                        (Action.FunctorCategoryEquivalence.counitIso.inv.app X✝).app X = CategoryTheory.CategoryStruct.id (X✝.obj PUnit.unit)
                        @[simp]
                        theorem Action.FunctorCategoryEquivalence.counitIso_hom_app_app {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} (X : CategoryTheory.Functor (CategoryTheory.SingleObj G) V) (X : CategoryTheory.SingleObj G) :
                        (Action.FunctorCategoryEquivalence.counitIso.hom.app X✝).app X = CategoryTheory.CategoryStruct.id (X✝.obj PUnit.unit)

                        The category of actions of G in the category V is equivalent to the functor category singleObj G ⥤ V.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          @[simp]
                          theorem Action.functorCategoryEquivalence_counitIso (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) :
                          (Action.functorCategoryEquivalence V G).counitIso = Action.FunctorCategoryEquivalence.counitIso
                          @[simp]
                          theorem Action.functorCategoryEquivalence_inverse (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) :
                          (Action.functorCategoryEquivalence V G).inverse = Action.FunctorCategoryEquivalence.inverse
                          @[simp]
                          theorem Action.functorCategoryEquivalence_functor (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) :
                          (Action.functorCategoryEquivalence V G).functor = Action.FunctorCategoryEquivalence.functor
                          @[simp]
                          theorem Action.functorCategoryEquivalence_unitIso (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) :
                          (Action.functorCategoryEquivalence V G).unitIso = Action.FunctorCategoryEquivalence.unitIso
                          instance Action.instIsEquivalenceFunctorSingleObjαMonoidFunctor (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) :
                          Action.FunctorCategoryEquivalence.functor.IsEquivalence
                          Equations
                          • =
                          instance Action.instIsEquivalenceFunctorSingleObjαMonoidInverse (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) :
                          Action.FunctorCategoryEquivalence.inverse.IsEquivalence
                          Equations
                          • =

                          (implementation) The forgetful functor from bundled actions to the underlying objects.

                          Use the CategoryTheory.forget API provided by the ConcreteCategory instance below, rather than using this directly.

                          Equations
                          Instances For
                            @[simp]
                            theorem Action.forget_map (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) :
                            ∀ {X Y : Action V G} (f : X Y), (Action.forget V G).map f = f.hom
                            @[simp]
                            theorem Action.forget_obj (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) (M : Action V G) :
                            (Action.forget V G).obj M = M.V
                            instance Action.instFaithfulForget (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) :
                            (Action.forget V G).Faithful
                            Equations
                            • =
                            Equations

                            The forgetful functor is intertwined by functorCategoryEquivalence with evaluation at PUnit.star.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              theorem Action.Iso.conj_ρ {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} {M : Action V G} {N : Action V G} (f : M N) (g : G) :
                              N g = ((Action.forget V G).mapIso f).conj (M g)

                              Actions/representations of the trivial group are just objects in the ambient category.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                def Action.res (V : Type (u + 1)) [CategoryTheory.LargeCategory V] {G : MonCat} {H : MonCat} (f : G H) :

                                The "restriction" functor along a monoid homomorphism f : G ⟶ H, taking actions of H to actions of G.

                                (This makes sense for any homomorphism, but the name is natural when f is a monomorphism.)

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  @[simp]
                                  theorem Action.res_obj_ρ (V : Type (u + 1)) [CategoryTheory.LargeCategory V] {G : MonCat} {H : MonCat} (f : G H) (M : Action V H) :
                                  @[simp]
                                  theorem Action.res_map_hom (V : Type (u + 1)) [CategoryTheory.LargeCategory V] {G : MonCat} {H : MonCat} (f : G H) :
                                  ∀ {X Y : Action V H} (p : X Y), ((Action.res V f).map p).hom = p.hom
                                  @[simp]
                                  theorem Action.res_obj_V (V : Type (u + 1)) [CategoryTheory.LargeCategory V] {G : MonCat} {H : MonCat} (f : G H) (M : Action V H) :
                                  ((Action.res V f).obj M).V = M.V

                                  The natural isomorphism from restriction along the identity homomorphism to the identity functor on Action V G.

                                  Equations
                                  Instances For
                                    @[simp]
                                    @[simp]
                                    def Action.resComp (V : Type (u + 1)) [CategoryTheory.LargeCategory V] {G : MonCat} {H : MonCat} {K : MonCat} (f : G H) (g : H K) :

                                    The natural isomorphism from the composition of restrictions along homomorphisms to the restriction along the composition of homomorphism.

                                    Equations
                                    Instances For
                                      @[simp]
                                      theorem Action.resComp_inv_app_hom (V : Type (u + 1)) [CategoryTheory.LargeCategory V] {G : MonCat} {H : MonCat} {K : MonCat} (f : G H) (g : H K) (X : Action V K) :
                                      @[simp]
                                      theorem Action.resComp_hom_app_hom (V : Type (u + 1)) [CategoryTheory.LargeCategory V] {G : MonCat} {H : MonCat} {K : MonCat} (f : G H) (g : H K) (X : Action V K) :

                                      A functor between categories induces a functor between the categories of G-actions within those categories.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        @[simp]
                                        theorem CategoryTheory.Functor.mapAction_obj_ρ_apply {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {W : Type (u + 1)} [CategoryTheory.LargeCategory W] (F : CategoryTheory.Functor V W) (G : MonCat) (M : Action V G) (g : G) :
                                        ((F.mapAction G).obj M) g = F.map (M g)
                                        @[simp]
                                        theorem CategoryTheory.Functor.mapAction_obj_V {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {W : Type (u + 1)} [CategoryTheory.LargeCategory W] (F : CategoryTheory.Functor V W) (G : MonCat) (M : Action V G) :
                                        ((F.mapAction G).obj M).V = F.obj M.V
                                        @[simp]
                                        theorem CategoryTheory.Functor.mapAction_map_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {W : Type (u + 1)} [CategoryTheory.LargeCategory W] (F : CategoryTheory.Functor V W) (G : MonCat) :
                                        ∀ {X Y : Action V G} (f : X Y), ((F.mapAction G).map f).hom = F.map f.hom