hom_inv_id — Mathlib

English

For any isomorphism of cones f: c ≅ d, the compositions f.hom.hom followed by f.inv.hom give the identity on c.pt.

Русский

Для изоморфизма конуса f: c ≅ d, композиция f.hom.hom затем f.inv.hom даёт тождественный морфизм на c.pt.

LaTeX

$$$f.hom.hom \\circ f.inv.hom = \\mathrm{id}_{c.pt}$$$

Lean4

@[reassoc (attr := simp)]
theorem hom_inv_id {c d : Cone F} (f : c ≅ d) : f.hom.hom ≫ f.inv.hom = 𝟙 _ := by simp [← Cone.category_comp_hom]

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