English
In the action category of a monoid M acting on a set X, for any two objects p and q, the set of morphisms from p to q is canonically identified with the subtype { m ∈ M | m · p.back = q.back }, i.e., a morphism from p to q is precisely a monoid element that carries p to q under the action.
Русский
В действительной категории действия моноида M, действующего на множество X, для любых двух объектов p и q множество морфизмов p → q канонически отождествляется с подмножеством { m ∈ M | m · p.back = q.back }, то есть морфизм p → q есть именно элемент моноида, действующий так, что переводит p в q через действие.
LaTeX
$$$\\displaystyle \\mathrm{Hom}_{\\mathsf{ActionCategory}(M,X)}(p,q) = \\{\, m \\in M \\mid m \\cdot p.{\\tt back} = q.{\\tt back} \\}$$$
Lean4
theorem hom_as_subtype (p q : ActionCategory M X) : (p ⟶ q) = { m : M // m • p.back = q.back } :=
rfl
