English
Restriction of scalars along a composition of topological monoid homomorphisms is naturally isomorphic to restricting first along one and then along the other. Precisely, ContAction.res V (h ∘ f) ≅ ContAction.res V h ∘ ContAction.res V f.
Русский
Ограничение по композиции гомоморфизмов топологических моноидов естественно изоморфно ограничению по одному после другого: Res_{h∘f} ≅ Res_h ∘ Res_f.
LaTeX
$$$\\mathrm{ContAction}.\\mathrm{res}\\ V\\ (h \\cdot f) \\cong \\mathrm{ContAction}.\\mathrm{res}\\ V h \\;\\circ\\; \\mathrm{ContAction}.\\mathrm{res}\\ V f.$$$
Lean4
/-- For `HasForget₂ V TopCat`, this is the full subcategory of `Action V G` where the induced
action is continuous. -/
def ContAction : Type _ :=
ObjectProperty.FullSubcategory (IsContinuous (V := V) (G := G))
