map_inv_hom_id_app — Mathlib

English

Variant asserting the inverse order equality: (F.map e.inv).app Z composed with (F.map e.hom).app Z is the identity.

Русский

Вариант: (F.map e.inv).app Z затем (F.map e.hom).app Z равно тождеству.

LaTeX

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

Lean4

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

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