square_to_iso_invert — Mathlib

English

Given i : X ≅ Y, p : Arrow T, and sq : i.hom ⟶ p, we have i.hom ≫ sq.right ≫ p.inv = sq.left.

Русский

Пусть i: X ≅ Y, p: Arrow T, sq: i.hom ⟶ p; тогда i.hom ≫ sq.right ≫ p.inv = sq.left.

LaTeX

$$$i.hom \circ sq.right \circ p.inv = sq.left$$$

Lean4

/-- Given a square from an arrow `i` to an isomorphism `p`, express the source part of `sq`
in terms of the inverse of `p`. -/
@[simp]
theorem square_to_iso_invert (i : Arrow T) {X Y : T} (p : X ≅ Y) (sq : i ⟶ Arrow.mk p.hom) :
    i.hom ≫ sq.right ≫ p.inv = sq.left := by
  simpa only [Category.assoc] using (Iso.comp_inv_eq p).mpr (Arrow.w_mk_right sq).symm

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