naturality_2' — Mathlib

English

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

Русский

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

LaTeX

$$$ α_X \circ G(f) \circ inv(α_Y) = F(f) $$$

Lean4

@[reassoc (attr := simp)]
theorem naturality_2' (α : F ⟶ G) (f : X ⟶ Y) {_ : IsIso (α.app Y)} : α.app X ≫ G.map f ≫ inv (α.app Y) = F.map f := by
  cat_disch

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