English
The proof provides a natural iso between the two ways of combining mapContAction, ensuring coherence of the construction.
Русский
Доказательство обеспечивает натуральную изоморфность между двумя способами объединения mapContAction, обеспечивая когерентность конструкции.
LaTeX
$$$\\text{proof of }\\mathrm{mapContActionComp}$ is a natural isomorphism.$$
Lean4
/-- Continuous version of `Functor.mapActionComp`. -/
@[simps! hom inv]
def mapContActionComp {T : Type*} [Category T] [HasForget T] [HasForget₂ T TopCat] (F : V ⥤ W)
(H : ∀ X : ContAction V G, ((F.mapAction G).obj X.obj).IsContinuous) (F' : W ⥤ T)
(H' : ∀ X : ContAction W G, ((F'.mapAction G).obj X.obj).IsContinuous) :
Functor.mapContAction G (F ⋙ F') (fun X ↦ H' ((F.mapContAction G H).obj X)) ≅
Functor.mapContAction G F H ⋙ Functor.mapContAction G F' H' :=
NatIso.ofComponents (fun _ ↦ Iso.refl _)
