isoOfHom_hom_inv_id — Mathlib

English

For all X in C and hf ∈ W, the inv of isoOfHom composed with L.map f equals the identity on X.

Русский

Для любого X в C и hf ∈ W обратный к isoOfHom после L.map f равен тождественному на X.

LaTeX

$$$(\\text{isoOfHom } L W f hf).inv \\; = \\; \\mathsf{Id} $$$

Lean4

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

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