English
A fully faithful functor F induces a fully faithful functor on action-categories via mapAction.
Русский
Полно-фиделный функтор F порождает полно-фиделный функтор между категориями действий через mapAction.
LaTeX
$$mapAction {F : V ⥤ W} (h : F.FullyFaithful) (G : Type*) [Monoid G] : (F.mapAction G).FullyFaithful$$
Lean4
/-- A functor between categories induces a functor between
the categories of `G`-actions within those categories. -/
@[simps]
def mapAction (F : V ⥤ W) (G : Type*) [Monoid G] : Action V G ⥤ Action W G
where
obj
M :=
{ V := F.obj M.V
ρ :=
{ toFun := fun g => F.map (M.ρ g)
map_one' := by simp
map_mul' := fun g h => by
dsimp
rw [map_mul, End.mul_def, F.map_comp] } }
map
f :=
{ hom := F.map f.hom
comm := fun g => by dsimp; rw [← F.map_comp, f.comm, F.map_comp] }
map_id M := by ext; simp only [Action.id_hom, F.map_id]
map_comp f g := by ext; simp only [Action.comp_hom, F.map_comp]
