naturality_2 — Mathlib

English

Let α: F ≅ G be a natural isomorphism and f: X → Y a morphism in C. Then the naturality condition holds: α_X ∘ G(f) ∘ α_Y^{-1} = F(f).

Русский

Пусть α: F ≅ G — естественный изоморфизм между функторами F и G, и f: X → Y — морфизм в C. Тогда естественная тождественная диаграмма выполняется: α_X ∘ G(f) ∘ α_Y^{-1} = F(f).

LaTeX

$$$\alpha_X \circ G(f) \circ \alpha_Y^{-1} = F(f)$$$

Lean4

theorem naturality_2 (α : F ≅ G) (f : X ⟶ Y) : α.hom.app X ≫ G.map f ≫ α.inv.app Y = F.map f := by simp

Похожие утверждения