English
For a natural transformation φ: F ⇒ G between functors, the naturality square at f: X → Y commutes, i.e., φ_Y ∘ F.map f = G.map f ∘ φ_X (on the underlying elements).
Русский
Для натурального преобразования φ: F ⇒ G между функторами естественна квадратная диаграмма, то есть φ_Y ∘ F.map f = G.map f ∘ φ_X на базовых элементах.
LaTeX
$$$\forall {F G : C \to D} (φ : F \Rightarrow G) {X Y : C} (f : X ⟶ Y) (x : ToType (F.obj X)), φ.app Y (F.map f x) = G.map f (φ.app X x)$$$
Lean4
@[simp]
theorem naturality_apply {C D : Type*} [Category C] [Category D] {FD : D → D → Type*} {CD : D → Type*}
[∀ X Y, FunLike (FD X Y) (CD X) (CD Y)] [ConcreteCategory D FD] {F G : C ⥤ D} (φ : F ⟶ G) {X Y : C} (f : X ⟶ Y)
(x : ToType (F.obj X)) : φ.app Y (F.map f x) = G.map f (φ.app X x) := by
simpa only [Functor.map_comp] using congr_fun ((forget D).congr_map (φ.naturality f)) x
