inv_hom_id_app_app_app — Mathlib

English

In the nested app context, the composition α.inv.app X₁ ≫ α.hom.app X₁ at level X₂ and X₃ yields identity on the corresponding object.

Русский

Во вложенном контексте приложений композиция α.inv.app X₁ ≫ α.hom.app X₁ на уровнях X₂ и X₃ дает тождество над соответствующим объектом.

LaTeX

$$$ ((\alpha.inv.app X_1).app X_2).app X_3 ≫ ((\alpha.hom.app X_1).app X_2).app X_3 = 1 $$$

Lean4

@[reassoc (attr := simp)]
theorem inv_hom_id_app_app_app {F G : C ⥤ D ⥤ E ⥤ E'} (e : F ≅ G) (X₁ : C) (X₂ : D) (X₃ : E) :
    ((e.inv.app X₁).app X₂).app X₃ ≫ ((e.hom.app X₁).app X₂).app X₃ = 𝟙 _ := by cat_disch

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