English
Let C and D be categories and F, G: C → D be functors. If F and G agree on every morphism of C (i.e., for all objects X,Y and f: X → Y, F(f) = G(f)), then F = G.
Русский
Пусть C и D — категории, а F, G: C → D —_functors. Если они совпадают на всех морфизмах C (для всех X,Y и f: X → Y выполнено F(f) = G(f)), то F = G.
LaTeX
$$$(\forall F,G: \mathcal{C} \to \mathcal{D})\; (\forall X,Y \in \mathrm{Ob}(\mathcal{C}), \forall f: X \to Y,\ F(f) = G(f)) \Rightarrow F = G.$$$
Lean4
/-- Extensionality lemma for functors `C ⥤ D` which uses as an assumption
that the induced maps `Arrow C → Arrow D` coincide. -/
theorem functor_ext {F G : C ⥤ D}
(h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), F.mapArrow.obj (Arrow.mk f) = G.mapArrow.obj (Arrow.mk f)) : F = G :=
Functor.ext (fun X ↦ congr_arg Comma.left (h (𝟙 X)))
(fun X Y f ↦ by
have := h f
simp only [Functor.mapArrow_obj, mk_eq_mk_iff] at this
tauto)
