leftUnitor_inv_app — Mathlib

English

The inverse hom component of the left unitor acts as expected on F(j).

Русский

Обратная гомоморфия левого унитора действует должным образом на F(j).

LaTeX

$$$$ (\lambda_ F).inv.app j = (\lambda_{F(j)}).inv. $$$$

Lean4

@[simp]
theorem leftUnitor_inv_app (F : J ⥤ C) (j : J) : (λ_ F).inv.app j = (λ_ (F.obj j)).inv := by
  rw [← cancel_mono ((λ_ (F.obj j)).hom), Iso.inv_hom_id, ← leftUnitor_hom_app, Iso.inv_hom_id_app]

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