hom_inv_id_triangle_hom₂ — Mathlib

English

For an isomorphism of triangles, the hom₁ component of the isomorphism times its inverse equals the identity on the first object.

Русский

Для изоморфизма треугольников произведение hom₁ компоненты на её обратную равняется тождественному морфизму на первом объекте.

LaTeX

$$$e.hom.hom_{1} \circ e.inv.hom_{1} = \mathrm{Id}_{A_{1}}$$$

Lean4

@[reassoc (attr := simp)]
theorem _root_.CategoryTheory.Iso.hom_inv_id_triangle_hom₂ {A B : Triangle C} (e : A ≅ B) :
    e.hom.hom₂ ≫ e.inv.hom₂ = 𝟙 _ := by rw [← comp_hom₂, e.hom_inv_id, id_hom₂]

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