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

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' := }
@[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
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.

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
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
@[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 := }
@[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.
@[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.

Auxiliary definition for functorCategoryEquivalence.

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

Auxiliary definition for functorCategoryEquivalence.

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

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.

(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
@[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
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.
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.
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
@[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
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
@[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
@[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.
@[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.
@[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
@[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
@[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.