English
Let e assign to each j a bijection e_j: F.obj j ≃ G.obj j, with naturality condition e_j' ∘ F.map f = G.map f ∘ e_j for all f: j ⟶ j'. Then for each f, (e_j').symm ∘ G.map f = F.map f ∘ (e_j).symm; i.e., inverses form a natural transformation compatible with F and G maps.
Русский
Пусть для каждого j задано биекция e_j: F.obj j ≃ G.obj j, и естественность e_j' ∘ F.map f = G.map f ∘ e_j для всех f: j ⟶ j'. Тогда для каждого f выполняется (e_j').symm ∘ G.map f = F.map f ∘ (e_j).symm; обратные отображения образуют естественную трансформацию, совместимую с F и G.
LaTeX
$$$$ (e_{j'})^{-1} \circ G(map\ f) = F(map\ f) \circ (e_j)^{-1} \quad \text{for all } f: j \to j'. $$$$
Lean4
theorem naturality_symm {F G : C ⥤ Type*} (e : ∀ j, F.obj j ≃ G.obj j)
(naturality : ∀ {j j'} (f : j ⟶ j'), e j' ∘ F.map f = G.map f ∘ e j) {j j' : C} (f : j ⟶ j') :
(e j').symm ∘ G.map f = F.map f ∘ (e j).symm := by
ext x
obtain ⟨y, rfl⟩ := (e j).surjective x
apply (e j').injective
dsimp
simp only [Equiv.apply_symm_apply, Equiv.symm_apply_apply]
exact (congr_fun (naturality f) y).symm
