naturality_1' — Mathlib

English

If α : F ⟶ G is a natural transformation and α_X is an isomorphism, then inv(α_X) ∘ F.map f ∘ α_Y = G.map f for any f: X → Y.

Русский

Если α : F ⟶ G — натуральное преобразование и компонент α_X является изоморфизмом, то для любого f: X → Y выполняется inv(α_X) ∘ F.map f ∘ α_Y = G.map f.

LaTeX

$$$ inv(\alpha_X) \circ F(f) \circ \alpha_Y = G(f) $$$

Lean4

theorem naturality_1' (α : F ⟶ G) (f : X ⟶ Y) {_ : IsIso (α.app X)} : inv (α.app X) ≫ F.map f ≫ α.app Y = G.map f := by
  simp

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