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
.
When a group acts, we can lift the action to the group of automorphisms.
Equations
Instances For
Equations
- Action.inhabited' G = { default := { V := PUnit.{?u.10 + 1} , ρ := 1 } }
The trivial representation of a group.
Equations
- Action.trivial G = { V := AddCommGrp.of PUnit.{?u.10 + 1} , ρ := 1 }
Instances For
Equations
- Action.instInhabitedAddCommGrp G = { default := Action.trivial G }
A homomorphism of Action V G
s is a morphism between the underlying objects,
commuting with the action of G
.
- hom : M.V ⟶ N.V
- comm : ∀ (g : ↑G), CategoryTheory.CategoryStruct.comp (M.ρ g) self.hom = CategoryTheory.CategoryStruct.comp self.hom (N.ρ g)
Instances For
The identity morphism on an Action V G
.
Equations
- Action.Hom.id M = { hom := CategoryTheory.CategoryStruct.id M.V, comm := ⋯ }
Instances For
Equations
- Action.Hom.instInhabited M = { default := Action.Hom.id M }
The composition of two Action V G
homomorphisms is the composition of the underlying maps.
Equations
- p.comp q = { hom := CategoryTheory.CategoryStruct.comp p.hom q.hom, comm := ⋯ }
Instances For
Equations
- Action.instCategory = CategoryTheory.Category.mk ⋯ ⋯ ⋯
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
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
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
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
Equations
- ⋯ = ⋯
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
- Action.forget V G = { obj := fun (M : Action V G) => M.V, map := fun {X Y : Action V G} (f : X ⟶ Y) => f.hom, map_id := ⋯, map_comp := ⋯ }
Instances For
Equations
- ⋯ = ⋯
Equations
- Action.instConcreteCategory V G = CategoryTheory.ConcreteCategory.mk ((Action.forget V G).comp CategoryTheory.ConcreteCategory.forget)
Equations
- Action.hasForgetToV V G = { forget₂ := Action.forget V G, forget_comp := ⋯ }
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
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
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
The natural isomorphism from restriction along the identity homomorphism to
the identity functor on Action V G
.
Equations
- Action.resId V = CategoryTheory.NatIso.ofComponents (fun (M : Action V G) => Action.mkIso (CategoryTheory.Iso.refl ((Action.res V (CategoryTheory.CategoryStruct.id G)).obj M).V) ⋯) ⋯
Instances For
The natural isomorphism from the composition of restrictions along homomorphisms to the restriction along the composition of homomorphism.
Equations
- Action.resComp V f g = CategoryTheory.NatIso.ofComponents (fun (M : Action V K) => Action.mkIso (CategoryTheory.Iso.refl (((Action.res V g).comp (Action.res V f)).obj M).V) ⋯) ⋯
Instances For
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.