English
Definition of the restriction-of-scalars functor along a ContinuousMonoidHom f: G →ₜ* H, from ContAction V H to ContAction V G; it acts on objects by applying the restriction and on morphisms by the corresponding map.
Русский
Определение функторa ограничения скалярного действия вдоль ContinuousMonoidHom f: G →ₜ* H: ContAction V H ⥤ ContAction V G; действует на объекты через ограничение действия и на морфизмы через соответствующее отображение.
LaTeX
$$$\\mathrm{res}(f) : \\mathrm{ContAction} V H ⥤ \\mathrm{ContAction} V G$ определяется как лифтинг через ObjectProperty.ι и соответствующие отображения.\n$$
Lean4
/-- Restricting scalars along a composition is naturally isomorphic to restricting scalars twice. -/
@[simps! hom inv]
def resComp {K : Type*} [Monoid K] [TopologicalSpace K] (f : G →ₜ* H) (h : H →ₜ* K) :
ContAction.res V (h.comp f) ≅ ContAction.res V h ⋙ ContAction.res V f :=
NatIso.ofComponents (fun _ ↦ Iso.refl _)
