English
Given F,G : SingleObj M ⥤ C and a morphism u : F(star) ⟶ G(star) compatible with all a ∈ M, there exists a natural transformation F ⟶ G whose components are u.
Русский
Для F,G : SingleObj M ⥤ C и морфизма u: F(star) ⟶ G(star), совместимого с каждым a∈M, существует естественное преобразование F ⟶ G с компонентами равными u.
LaTeX
$$$\\exists!\\ \\eta:F\\Rightarrow G\\text{ с }\\eta_{\\mathrm{star}} = u \\text{ и } F(a) \\circ u = u \\circ G(a)\\ \\forall a\\in M.$$$
Lean4
/-- Construct a natural transformation between functors `SingleObj M ⥤ C` by
giving a compatible morphism `SingleObj.star M`. -/
@[simps]
def natTrans {F G : SingleObj M ⥤ C} (u : F.obj (SingleObj.star M) ⟶ G.obj (SingleObj.star M))
(h : ∀ a : M, F.map a ≫ u = u ≫ G.map a) : F ⟶ G
where
app _ := u
naturality _ _ a := h a
