English
If f = f' for ContinuousMonoidHom G H, then ContAction.res V f ≅ ContAction.res V f'.
Русский
Если f = f' для ContinuousMonoidHom G H, тогда ContAction.res V f ≅ ContAction.res V f'.
LaTeX
$$$\\forall \\{f,f'\\ :\\ G \\to_{}^{} H\\},\\ f=f'\\Rightarrow ContAction.res \\ V f \\cong ContAction.res \\ V f'.$$$
Lean4
/-- The "restriction" functor along a monoid homomorphism `f : G →* H`,
taking actions of `H` to actions of `G`. This is the analogue of
`Action.res` in the continuous setting. -/
@[simps! obj_obj map]
def res (f : G →ₜ* H) : ContAction V H ⥤ ContAction V G :=
ObjectProperty.lift _ (ObjectProperty.ι _ ⋙ Action.res _ f) fun X ↦
by
constructor
let v : G × (forget₂ _ TopCat).obj X → H × (forget₂ _ TopCat).obj X := fun p ↦ (f p.1, p.2)
have : Continuous v := by fun_prop
let u : H × (forget₂ _ TopCat).obj X → (forget₂ _ TopCat).obj X := fun p ↦ (forget₂ _ TopCat).map (X.obj.ρ p.1) p.2
have : Continuous u := X.2.1
change Continuous (u ∘ v)
fun_prop
