inv_hom_id_triangle_hom₁ — Mathlib

English

For an isomorphism e: A ≅ B of triangles, the second arrow component of the inverse composed with the second arrow component of the forward morphism equals the identity on B's first object.

Русский

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

LaTeX

$$$e_{\text{inv},1} \circ e_{\text,1} = \mathrm{Id}_{B_1}$$$

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

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