English
Restriction of scalars along a ContinuousMulEquiv f: G ≃ₜ* H yields an equivalence ContAction V H ≌ ContAction V G.
Русский
Ограничение скаляр по непрерывной эквивалентности f: G ≃ₜ* H дает эквалентность ContAction V H ≌ ContAction V G.
LaTeX
$$$\\mathrm{ResEquiv}\\ V f : \\mathrm{ContAction} V H \\simeq \\mathrm{ContAction} V G$ is an equivalence when f is a continuous monoid equivalence.$$
Lean4
/-- Restriction of scalars along a topological monoid isomorphism induces an equivalence of
categories. -/
@[simps! functor inverse]
def resEquiv (f : G ≃ₜ* H) : ContAction V H ≌ ContAction V G
where
functor := res _ f
inverse := res _ f.symm
unitIso := resCongr V (ContinuousMonoidHom.id H) _ (by ext; simp) ≪≫ ContAction.resComp _ _ _
counitIso := (ContAction.resComp _ _ _).symm ≪≫ ContAction.resCongr V _ (ContinuousMonoidHom.id G) (by ext; simp)
functor_unitIso_comp X := (Action.resEquiv V f.toMulEquiv).functor_unitIso_comp X.obj
