English
Restricting along a monoid homomorphism yields a faithful functor on actions.
Русский
Ограничение по гомоморфизму моноидов даёт верный функтор на действиях.
LaTeX
$$instFaithfulRes {V} {G} {H} (f : G →* H) : (res V f).Faithful$$
Lean4
/-- The "restriction" functor along a monoid homomorphism `f : G ⟶ H`,
taking actions of `H` to actions of `G`.
(This makes sense for any homomorphism, but the name is natural when `f` is a monomorphism.)
-/
@[simps]
def res {G H : Type*} [Monoid G] [Monoid H] (f : G →* H) : Action V H ⥤ Action V G
where
obj
M :=
{ V := M.V
ρ := M.ρ.comp f }
map
p :=
{ hom := p.hom
comm := fun g => p.comm (f g) }
