isoOfHom_inv_hom_id — Mathlib

English

The inverse of isoOfHom composed with L.map f equals the identity after applying functor on X.

Русский

Обратный от isoOfHom после L.map f равен тождеству после применения функторa к X.

LaTeX

$$$(\\text{isoOfHom } L W f hf).inv_hom_id$$$

Lean4

@[reassoc (attr := simp)]
theorem isoOfHom_inv_hom_id {X Y : C} (f : X ⟶ Y) (hf : W f) : (isoOfHom L W f hf).inv ≫ L.map f = 𝟙 _ :=
  (isoOfHom L W f hf).inv_hom_id

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