English
Conjugation compatibility for res along a monoid equivalence holds for all X,Y actions.
Русский
Совместимость конъюгирования для ограничения вдоль эквивалентности моноидов выполняется для любых действий X,Y.
LaTeX
$$theorem resEquiv_proof {G H} [Monoid G] [Monoid H] (f : G ≃* H) {X Y : Action V H} (f₁ : Action.instCategory.Hom X Y) : ...$$
Lean4
/-- Restricting scalars along a monoid isomorphism induces an equivalence of categories. -/
@[simps! functor inverse]
def resEquiv {G H : Type*} [Monoid G] [Monoid H] (f : G ≃* H) : Action V H ≌ Action V G
where
functor := Action.res _ f
inverse := Action.res _ f.symm
unitIso := Action.resCongr (f := MonoidHom.id H) V (by ext; simp) ≪≫ (Action.resComp _ _ _).symm
counitIso :=
Action.resComp _ _ _ ≪≫
Action.resCongr (f' := MonoidHom.id G) V
(by ext; simp)
-- TODO promote `res` to a pseudofunctor from
-- the locally discrete bicategory constructed from `Monᵒᵖ` to `Cat`, sending `G` to `Action V G`.
