map_hom_inv_id_app — Mathlib

English

As in the standard isomorphism property, the composition of (F.map e.hom) and (F.map e.inv) yields the identity on the corresponding component.

Русский

Как и полагается свойству изоморфизма, композиция (F.map e.hom) и (F.map e.inv) дает тождественный морфизм на соответствующем компоненте.

LaTeX

$$$$ (F.map e.hom).app Z \\;\\circ\\; (F.map e.inv).app Z = \\mathrm{Id}. $$$$

Lean4

@[reassoc (attr := simp)]
theorem map_hom_inv_id_app {X Y : C} (e : X ≅ Y) (F : C ⥤ D ⥤ E) (Z : D) :
    (F.map e.hom).app Z ≫ (F.map e.inv).app Z = 𝟙 _ := by cat_disch

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