English
An equivalence E: V ≌ W induces an equivalence between the categories of G-actions: Action V G ≌ Action W G.
Русский
Эквивалентность E: V ≌ W порождает эквивалентность между категориями G-действий: Action V G ≌ Action W G.
LaTeX
$$$\\mathrm{mapAction}(G,E): \\mathrm{Action}\,V\,G \\simeq \\mathrm{Action}\,W\,G$$$
Lean4
/-- An equivalence of categories induces an equivalence of
the categories of `G`-actions within those categories. -/
@[simps functor inverse]
def mapAction {V W : Type*} [Category V] [Category W] (G : Type*) [Monoid G] (E : V ≌ W) : Action V G ≌ Action W G
where
functor := E.functor.mapAction G
inverse := E.inverse.mapAction G
unitIso := Functor.mapActionCongr G E.unitIso ≪≫ Functor.mapActionComp G _ _
counitIso := (Functor.mapActionComp G _ _).symm ≪≫ Functor.mapActionCongr G E.counitIso
functor_unitIso_comp X := by ext; simp
