English
An action M ↻ X yields a functor from the one-object category of M to Type, sending the sole object to X and m ∈ M to the map x ↦ m·x.
Русский
Действие M↻X порождает функтор из однобордной категории M в Type: единственный объект идёт в X, а элемент m∈M действует как отображение x↦m·x.
LaTeX
$$$\text{actionAsFunctor}: \, \mathbf{1}_M \to \mathsf{Type}$ with $\text{map}(m)(x)=m\cdot x$$$
Lean4
/-- A multiplicative action M ↻ X viewed as a functor mapping the single object of M to X
and an element `m : M` to the map `X → X` given by multiplication by `m`. -/
@[simps]
def actionAsFunctor : SingleObj M ⥤ Type u where
obj _ := X
map := (· • ·)
map_id _ := funext <| MulAction.one_smul
map_comp f g := funext fun x => (smul_smul g f x).symm
