inv_hom_id_triangle_hom₂ — Mathlib

English

In an isomorphism of triangles, the second component of the inverse followed by the second component of the forward morphism yields the identity on the second vertex of B.

Русский

Для изоморфизма треугольников вторая компонента обратного морфизма после второй компоненты прямого дает единицу на втором объекте B.

LaTeX

$$$e_{\text{inv},2} \circ e_{\text},2 = \mathrm{Id}_{B_2}$$$

Lean4

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

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