hom_inv_id_hom — Mathlib

English

If e is an isomorphism of SingleFunctors, then the composition of the inverse hom with the hom equals the identity; i.e., e.inv.hom n ≫ e.hom.hom n = id.

Русский

Если e — изоморфизм между SingleFunctors, то композиция e.inv.hom n и e.hom.hom n равна идентичности.

LaTeX

$$$$ e.inv.hom n \\;\\circ\\; e.hom.hom n = 1_{G.functor n}. $$$$

Lean4

@[reassoc (attr := simp)]
theorem hom_inv_id_hom (e : F ≅ G) (n : A) : e.hom.hom n ≫ e.inv.hom n = 𝟙 _ := by rw [← comp_hom, e.hom_inv_id, id_hom]

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