Documentation

Mathlib.CategoryTheory.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} [Monoid G] [Monoid H] (f : G →* H) : Action V H ⥤ Action V G.

structure Action (V : Type u_1) [CategoryTheory.Category.{u_3, u_1} V] (G : Type u_2) [Monoid G] :
Type (max (max u_1 u_2) u_3)

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.

  • V : V

    The object this action acts on

  • The underlying monoid homomorphism of this action

Instances For

    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.Category.{u_3, u_1} V] {G : Type u_2} [Group G] (A : Action V G) (g : G) :
      (A.ρAut g).hom = A.ρ g
      @[simp]
      theorem Action.ρAut_apply_inv {V : Type u_1} [CategoryTheory.Category.{u_3, u_1} V] {G : Type u_2} [Group G] (A : Action V G) (g : G) :
      (A.ρAut g).inv = A.ρ g⁻¹
      instance Action.inhabited' (G : Type u_2) [Monoid G] :
      Equations

      The trivial representation of a group.

      Equations
      Instances For
        structure Action.Hom {V : Type u_1} [CategoryTheory.Category.{u_3, u_1} V] {G : Type u_2} [Monoid G] (M N : Action V G) :
        Type u_3

        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_iff {V : Type u_1} {inst✝ : CategoryTheory.Category.{u_3, u_1} V} {G : Type u_2} {inst✝¹ : Monoid G} {M N : Action V G} {x y : M.Hom N} :
          x = y x.hom = y.hom
          theorem Action.Hom.ext {V : Type u_1} {inst✝ : CategoryTheory.Category.{u_3, u_1} V} {G : Type u_2} {inst✝¹ : Monoid G} {M N : Action V G} {x y : M.Hom N} (hom : x.hom = y.hom) :
          x = y
          def Action.Hom.id {V : Type u_1} [CategoryTheory.Category.{u_3, u_1} V] {G : Type u_2} [Monoid G] (M : Action V G) :
          M.Hom M

          The identity morphism on an Action V G.

          Equations
          Instances For
            def Action.Hom.comp {V : Type u_1} [CategoryTheory.Category.{u_3, u_1} V] {G : Type u_2} [Monoid G] {M N 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.Category.{u_3, u_1} V] {G : Type u_2} [Monoid G] {M N K : Action V G} (p : M.Hom N) (q : N.Hom K) :
              Equations
              • One or more equations did not get rendered due to their size.
              theorem Action.hom_ext {V : Type u_1} [CategoryTheory.Category.{u_3, u_1} V] {G : Type u_2} [Monoid G] {M N : Action V G} (φ₁ φ₂ : M N) (h : φ₁.hom = φ₂.hom) :
              φ₁ = φ₂
              theorem Action.hom_ext_iff {V : Type u_1} [CategoryTheory.Category.{u_3, u_1} V] {G : Type u_2} [Monoid G] {M N : Action V G} {φ₁ φ₂ : M N} :
              φ₁ = φ₂ φ₁.hom = φ₂.hom
              def Action.mkIso {V : Type u_1} [CategoryTheory.Category.{u_3, u_1} V] {G : Type u_2} [Monoid G] {M N : Action V G} (f : M.V N.V) (comm : ∀ (g : G), CategoryTheory.CategoryStruct.comp (M.ρ g) f.hom = CategoryTheory.CategoryStruct.comp f.hom (N.ρ g) := by aesop_cat) :
              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_inv_hom {V : Type u_1} [CategoryTheory.Category.{u_3, u_1} V] {G : Type u_2} [Monoid G] {M N : Action V G} (f : M.V N.V) (comm : ∀ (g : G), CategoryTheory.CategoryStruct.comp (M.ρ g) f.hom = CategoryTheory.CategoryStruct.comp f.hom (N.ρ g) := by aesop_cat) :
                (mkIso f comm).inv.hom = f.inv
                @[simp]
                theorem Action.mkIso_hom_hom {V : Type u_1} [CategoryTheory.Category.{u_3, u_1} V] {G : Type u_2} [Monoid G] {M N : Action V G} (f : M.V N.V) (comm : ∀ (g : G), CategoryTheory.CategoryStruct.comp (M.ρ g) f.hom = CategoryTheory.CategoryStruct.comp f.hom (N.ρ g) := by aesop_cat) :
                (mkIso f comm).hom.hom = f.hom
                @[instance 100]
                instance Action.isIso_hom_mk {V : Type u_1} [CategoryTheory.Category.{u_3, u_1} V] {G : Type u_2} [Monoid G] {M 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 }

                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.Category.{u_3, u_1} V] {G : Type u_2} [Monoid G] (M : Action V G) {X✝ Y✝ : CategoryTheory.SingleObj G} (g : X✝ Y✝) :
                  (functor.obj M).map g = M.ρ g
                  @[simp]
                  theorem Action.FunctorCategoryEquivalence.functor_map_app {V : Type u_1} [CategoryTheory.Category.{u_3, u_1} V] {G : Type u_2} [Monoid G] {X✝ Y✝ : Action V G} (f : X✝ Y✝) (x✝ : CategoryTheory.SingleObj G) :
                  (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

                    Auxiliary definition for functorCategoryEquivalence.

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

                      Auxiliary definition for functorCategoryEquivalence.

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

                        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

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

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

                          Equations
                          Instances For
                            @[simp]
                            theorem Action.forget_obj (V : Type u_1) [CategoryTheory.Category.{u_3, u_1} V] (G : Type u_2) [Monoid G] (M : Action V G) :
                            (forget V G).obj M = M.V
                            @[simp]
                            theorem Action.forget_map (V : Type u_1) [CategoryTheory.Category.{u_3, u_1} V] (G : Type u_2) [Monoid G] {X✝ Y✝ : Action V G} (f : X✝ Y✝) :
                            (forget V G).map f = f.hom
                            @[reducible, inline]
                            abbrev Action.HomSubtype (V : Type u_1) [CategoryTheory.Category.{u_5, u_1} V] (G : Type u_2) [Monoid G] {FV : VVType u_3} {CV : VType u_4} [(X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] [CategoryTheory.ConcreteCategory V FV] (M N : Action V G) :
                            Type u_3

                            The type of V-morphisms that can be lifted back to morphisms in the category Action.

                            Equations
                            Instances For
                              instance Action.instFunLikeHomSubtypeV (V : Type u_1) [CategoryTheory.Category.{u_5, u_1} V] (G : Type u_2) [Monoid G] {FV : VVType u_3} {CV : VType u_4} [(X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] [CategoryTheory.ConcreteCategory V FV] (M N : Action V G) :
                              FunLike (HomSubtype V G M N) (CV M.V) (CV N.V)
                              Equations
                              instance Action.instConcreteCategoryHomSubtypeV (V : Type u_1) [CategoryTheory.Category.{u_5, u_1} V] (G : Type u_2) [Monoid G] {FV : VVType u_3} {CV : VType u_4} [(X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] [CategoryTheory.ConcreteCategory V FV] :
                              Equations
                              • One or more equations did not get rendered due to their size.
                              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.Category.{u_3, u_1} V] {G : Type u_2} [Monoid G] {M N : Action V G} (f : M N) (g : G) :
                                N.ρ g = ((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.Category.{u_5, u_1} V] {G : Type u_3} {H : Type u_4} [Monoid G] [Monoid H] (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
                                  Instances For
                                    @[simp]
                                    theorem Action.res_obj_ρ (V : Type u_1) [CategoryTheory.Category.{u_5, u_1} V] {G : Type u_3} {H : Type u_4} [Monoid G] [Monoid H] (f : G →* H) (M : Action V H) :
                                    ((res V f).obj M).ρ = M.ρ.comp f
                                    @[simp]
                                    theorem Action.res_obj_V (V : Type u_1) [CategoryTheory.Category.{u_5, u_1} V] {G : Type u_3} {H : Type u_4} [Monoid G] [Monoid H] (f : G →* H) (M : Action V H) :
                                    ((res V f).obj M).V = M.V
                                    @[simp]
                                    theorem Action.res_map_hom (V : Type u_1) [CategoryTheory.Category.{u_5, u_1} V] {G : Type u_3} {H : Type u_4} [Monoid G] [Monoid H] (f : G →* H) {X✝ Y✝ : Action V H} (p : X✝ Y✝) :
                                    ((res V f).map p).hom = p.hom

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

                                    Equations
                                    Instances For
                                      def Action.resComp (V : Type u_1) [CategoryTheory.Category.{u_6, u_1} V] {G : Type u_3} {H : Type u_4} {K : Type u_5} [Monoid G] [Monoid H] [Monoid K] (f : G →* H) (g : H →* K) :
                                      (res V g).comp (res V f) res V (g.comp f)

                                      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.Category.{u_6, u_1} V] {G : Type u_3} {H : Type u_4} {K : Type u_5} [Monoid G] [Monoid H] [Monoid K] (f : G →* H) (g : H →* K) (X : Action V K) :
                                        @[simp]
                                        theorem Action.resComp_hom_app_hom (V : Type u_1) [CategoryTheory.Category.{u_6, u_1} V] {G : Type u_3} {H : Type u_4} {K : Type u_5} [Monoid G] [Monoid H] [Monoid K] (f : G →* H) (g : H →* K) (X : Action V K) :
                                        def Action.resCongr (V : Type u_1) [CategoryTheory.Category.{u_5, u_1} V] {G : Type u_3} {H : Type u_4} [Monoid G] [Monoid H] {f f' : G →* H} (h : f = f') :
                                        res V f res V f'

                                        Restricting scalars along equal maps is naturally isomorphic.

                                        Equations
                                        Instances For
                                          @[simp]
                                          theorem Action.resCongr_hom (V : Type u_1) [CategoryTheory.Category.{u_5, u_1} V] {G : Type u_3} {H : Type u_4} [Monoid G] [Monoid H] {f f' : G →* H} (h : f = f') :
                                          (resCongr V h).hom = { app := fun (X : Action V H) => (mkIso (CategoryTheory.Iso.refl X.V) ).hom, naturality := }
                                          @[simp]
                                          theorem Action.resCongr_inv (V : Type u_1) [CategoryTheory.Category.{u_5, u_1} V] {G : Type u_3} {H : Type u_4} [Monoid G] [Monoid H] {f f' : G →* H} (h : f = f') :
                                          (resCongr V h).inv = { app := fun (X : Action V H) => (mkIso (CategoryTheory.Iso.refl X.V) ).inv, naturality := }
                                          def Action.resEquiv (V : Type u_1) [CategoryTheory.Category.{u_5, u_1} V] {G : Type u_3} {H : Type u_4} [Monoid G] [Monoid H] (f : G ≃* H) :
                                          Action V H Action V G

                                          Restricting scalars along a monoid isomorphism induces an equivalence of categories.

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            @[simp]
                                            theorem Action.resEquiv_inverse (V : Type u_1) [CategoryTheory.Category.{u_5, u_1} V] {G : Type u_3} {H : Type u_4} [Monoid G] [Monoid H] (f : G ≃* H) :
                                            (resEquiv V f).inverse = res V f.symm
                                            @[simp]
                                            theorem Action.resEquiv_functor (V : Type u_1) [CategoryTheory.Category.{u_5, u_1} V] {G : Type u_3} {H : Type u_4} [Monoid G] [Monoid H] (f : G ≃* H) :
                                            (resEquiv V f).functor = res V f
                                            instance Action.instFaithfulRes (V : Type u_1) [CategoryTheory.Category.{u_5, u_1} V] {G : Type u_3} {H : Type u_4} [Monoid G] [Monoid H] (f : G →* H) :

                                            The functor from Action V H to Action V G induced by a morphism f : G → H is faithful.

                                            theorem Action.full_res (V : Type u_1) [CategoryTheory.Category.{u_5, u_1} V] {G : Type u_3} {H : Type u_4} [Monoid G] [Monoid H] (f : G →* H) (f_surj : Function.Surjective f) :
                                            (res V f).Full

                                            The functor from Action V H to Action V G induced by a morphism f : G → H is full if f is surjective.

                                            def CategoryTheory.Functor.mapAction {V : Type u_1} [Category.{u_4, u_1} V] {W : Type u_2} [Category.{u_5, u_2} W] (F : Functor V W) (G : Type u_3) [Monoid G] :
                                            Functor (Action V G) (Action W G)

                                            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_V {V : Type u_1} [Category.{u_4, u_1} V] {W : Type u_2} [Category.{u_5, u_2} W] (F : Functor V W) (G : Type u_3) [Monoid G] (M : Action V G) :
                                              ((F.mapAction G).obj M).V = F.obj M.V
                                              @[simp]
                                              theorem CategoryTheory.Functor.mapAction_obj_ρ_apply {V : Type u_1} [Category.{u_4, u_1} V] {W : Type u_2} [Category.{u_5, u_2} W] (F : Functor V W) (G : Type u_3) [Monoid G] (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} [Category.{u_4, u_1} V] {W : Type u_2} [Category.{u_5, u_2} W] (F : Functor V W) (G : Type u_3) [Monoid G] {X✝ Y✝ : Action V G} (f : X✝ Y✝) :
                                              ((F.mapAction G).map f).hom = F.map f.hom
                                              def CategoryTheory.Functor.mapActionComp {V : Type u_1} [Category.{u_5, u_1} V] {W : Type u_2} [Category.{u_6, u_2} W] (G : Type u_3) [Monoid G] {T : Type u_4} [Category.{u_7, u_4} T] (F : Functor V W) (F' : Functor W T) :
                                              (F.comp F').mapAction G (F.mapAction G).comp (F'.mapAction G)

                                              Functor.mapAction is functorial in the functor.

                                              Equations
                                              Instances For
                                                @[simp]
                                                theorem CategoryTheory.Functor.mapActionComp_hom {V : Type u_1} [Category.{u_5, u_1} V] {W : Type u_2} [Category.{u_6, u_2} W] (G : Type u_3) [Monoid G] {T : Type u_4} [Category.{u_7, u_4} T] (F : Functor V W) (F' : Functor W T) :
                                                (mapActionComp G F F').hom = { app := fun (X : Action V G) => CategoryStruct.id (((F.comp F').mapAction G).obj X), naturality := }
                                                @[simp]
                                                theorem CategoryTheory.Functor.mapActionComp_inv {V : Type u_1} [Category.{u_5, u_1} V] {W : Type u_2} [Category.{u_6, u_2} W] (G : Type u_3) [Monoid G] {T : Type u_4} [Category.{u_7, u_4} T] (F : Functor V W) (F' : Functor W T) :
                                                (mapActionComp G F F').inv = { app := fun (X : Action V G) => CategoryStruct.id (((F.comp F').mapAction G).obj X), naturality := }
                                                def CategoryTheory.Functor.mapActionCongr {V : Type u_1} [Category.{u_4, u_1} V] {W : Type u_2} [Category.{u_5, u_2} W] (G : Type u_3) [Monoid G] {F F' : Functor V W} (e : F F') :

                                                Functor.mapAction preserves isomorphisms of functors.

                                                Equations
                                                Instances For
                                                  @[simp]
                                                  theorem CategoryTheory.Functor.mapActionCongr_inv {V : Type u_1} [Category.{u_4, u_1} V] {W : Type u_2} [Category.{u_5, u_2} W] (G : Type u_3) [Monoid G] {F F' : Functor V W} (e : F F') :
                                                  (mapActionCongr G e).inv = { app := fun (X : Action V G) => (Action.mkIso (e.app X.V) ).inv, naturality := }
                                                  @[simp]
                                                  theorem CategoryTheory.Functor.mapActionCongr_hom {V : Type u_1} [Category.{u_4, u_1} V] {W : Type u_2} [Category.{u_5, u_2} W] (G : Type u_3) [Monoid G] {F F' : Functor V W} (e : F F') :
                                                  (mapActionCongr G e).hom = { app := fun (X : Action V G) => (Action.mkIso (e.app X.V) ).hom, naturality := }
                                                  def CategoryTheory.Equivalence.mapAction {V : Type u_2} {W : Type u_3} [Category.{u_5, u_2} V] [Category.{u_6, u_3} W] (G : Type u_4) [Monoid G] (E : V W) :
                                                  Action V G Action W G

                                                  An equivalence of categories induces an equivalence of the categories of G-actions within those categories.

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