English
Let E: V ≌ W be an equivalence of categories, and suppose H₁ and H₂ give continuity data for all ContAction V G and ContAction W G respectively. Then there is a continuous-action equivalence ContAction V G ≌ ContAction W G induced by E.
Русский
Пусть E: V ≌ W — эквивалентности категорий, и даны условия непрерывности H₁ и H₂ для всех ContAction V G и ContAction W G соответственно. Тогда существует непрерывная эквивалентность ContAction V G ≌ ContAction W G, индуцированная E.
LaTeX
$$$\mathrm{ContAction}(V,G) \simeq \mathrm{ContAction}(W,G).$$$
Lean4
/-- Continuous version of `Equivalence.mapAction`. -/
@[simps functor inverse]
def mapContAction (E : V ≌ W) (H₁ : ∀ X : ContAction V G, ((E.functor.mapAction G).obj X.obj).IsContinuous)
(H₂ : ∀ X : ContAction W G, ((E.inverse.mapAction G).obj X.obj).IsContinuous) : ContAction V G ≌ ContAction W G
where
functor := E.functor.mapContAction G H₁
inverse := E.inverse.mapContAction G H₂
unitIso :=
Functor.mapContActionCongr G E.unitIso (fun X ↦ X.2) (fun X ↦ H₂ ((E.functor.mapContAction G H₁).obj X)) ≪≫
Functor.mapContActionComp G _ _ _ _
counitIso := (Functor.mapContActionComp G _ _ _ _).symm ≪≫ Functor.mapContActionCongr G E.counitIso _ (fun X ↦ X.2)
functor_unitIso_comp X := (E.mapAction G).functor_unitIso_comp X.obj
