English
If G is a group object in a cartesian monoidal category, then for any X, the set of arrows X → G carries a natural group structure induced by the group-object structure of G.
Русский
Если G является групповым объектом в декартовой монадной категории, то множество стрелок X → G естественным образом образует группу, индуцированную структурой группового объекта на G.
LaTeX
$$$\mathrm{Hom}(X,G) \text{ carries a natural group structure induced by } G$$$
Lean4
/-- If `G` is a group object, then `Hom(X, G)` has a group structure. -/
abbrev group : Group (X ⟶ G) where
inv f := f ≫ ι
inv_mul_cancel
f :=
calc
lift (f ≫ ι) f ≫ μ
_ = (f ≫ lift ι (𝟙 G)) ≫ μ := by simp
_ = toUnit X ≫ η := by rw [Category.assoc]; simp
