English
There is a natural equivalence between monoid homomorphisms M →* N and functors SingleObj M ⥤ SingleObj N that is compatible with composition and identities.
Русский
Существует естественная эквивалентность между гомоморфизмами моноидов M →* N и функторaми SingleObj M ⥤ SingleObj N, сохраняющая композицию и тождественные переходы.
LaTeX
$$$mapHom : (M\\to^* N) \\simeq \\mathrm{Functor}(\\mathrm{SingleObj} M, \\mathrm{SingleObj} N)$$$
Lean4
/-- Given a function `f : C → G` from a category to a group, we get a functor
`C ⥤ G` sending any morphism `x ⟶ y` to `f y * (f x)⁻¹`. -/
@[simps]
def differenceFunctor (f : C → G) : C ⥤ SingleObj G
where
obj _ := ()
map {x y} _ := f y * (f x)⁻¹
map_id := by
intro
simp only [SingleObj.id_as_one, mul_inv_cancel]
map_comp := by
intros
rw [SingleObj.comp_as_mul, ← mul_assoc, mul_left_inj, mul_assoc, inv_mul_cancel, mul_one]
