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 ≌ (singleObj G ⥤ V), and construct the restriction functors res {G H : Mon} (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) :
    @[simp]
    theorem Action.ρAut_apply_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : GroupCat} (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 : GroupCat} (A : Action V (MonCat.of G)) (g : G) :
    (A.ρAut g).inv = A 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
      Equations

      The trivial representation of a group.

      Equations
      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.ext_iff {V : Type (u + 1)} :
        ∀ {inst : CategoryTheory.LargeCategory V} {G : MonCat} {M N : Action V G} (x y : M.Hom N), x = y x.hom = y.hom
        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.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
            @[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
            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
              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.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
              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
                @[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
                • =
                @[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
                @[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_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

                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

                  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.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.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)
                      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_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
                        @[simp]
                        theorem Action.functorCategoryEquivalence_counitIso (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) :
                        (Action.functorCategoryEquivalence V G).counitIso = Action.FunctorCategoryEquivalence.counitIso

                        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.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

                          (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
                            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
                                @[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 : Type (u + 1)) [CategoryTheory.LargeCategory V] {G : MonCat} {H : MonCat} (f : G H) (M : Action V H) :
                                @[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
                                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]
                                  @[simp]

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

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

                                      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