inv_left — Mathlib

English

If e is an isomorphism in the comma category, then the left inverse relation holds: L.map (inv e.left) ≫ Y.hom ≫ R.map (inv e.right) = X.hom.

Русский

Если e — изоморфизм в комма‑категории, то выполняется тождество: L.map (inv e.left) ≫ Y.hom ≫ R.map (inv e.right) = X.hom.

LaTeX

$$$ L.map(\mathrm{inv}(e.left)) \; \ggg \; Y.hom \; \ggg \; R.map(\mathrm{inv}(e.right)) = X.hom. $$$

Lean4

@[simp]
theorem inv_left [IsIso e] : (inv e).left = inv e.left :=
  by
  apply IsIso.eq_inv_of_hom_inv_id
  rw [← Comma.comp_left, IsIso.hom_inv_id, id_left]

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