iso_w — Mathlib

English

If e : f ≅ g is an isomorphism of arrows, then the underlying arrows satisfy g.hom = e.inv.left ≫ f.hom ≫ e.hom.right.

Русский

Если e : f ≅ g является изоморфизмом стрел, то тождественные стрелы удовлетворяют g.hom = e.inv.left ≫ f.hom ≫ e.hom.right.

LaTeX

$$$\forall f,g:(Arrow\ T)\; (e:\, f\cong g):\; g.hom = e.inv.left \circ f.hom \circ e.hom.right$$$

Lean4

theorem iso_w {f g : Arrow T} (e : f ≅ g) : g.hom = e.inv.left ≫ f.hom ≫ e.hom.right :=
  by
  have eq := Arrow.hom.congr_right e.inv_hom_id
  rw [Arrow.comp_right, Arrow.id_right] at eq
  rw [Arrow.w_assoc, eq, Category.comp_id]

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