hom_inv_id_triangle_hom₃ — Mathlib

English

Let e be an isomorphism between two triangulated objects A and B. Then the third component of the forward morphism composed with the third component of its inverse is the identity on the third object of A.

Русский

Пусть e — изоморфизм между треугольниками A и B. Тогда третий компонент прямого морфизма, композиции с третьим компонентом обратного, равен единице на третьем объекте A.

LaTeX

$$$e_{\text{hom},3} \circ e_{\text{inv},3} = \mathrm{Id}_{A_3}$$$

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₃]

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