inv_hom_id_app_app — Mathlib

English

For a triple-layered functor iso α: F ≅ G, the nested composition (α.inv.app X₁).app X₂ ≫ (α.hom.app X₁).app X₂ equals the identity on (G.obj X₁).obj X₂.

Русский

Для тройного уровня изоморфизма α: F ≅ G, вложенная композиция (α.inv.app X₁).app X₂ ≫ (α.hom.app X₁).app X₂ равна единице на (G.obj X₁).obj X₂.

LaTeX

$$$ ((\alpha.inv.app X_1).app X_2) \circ ((\alpha.hom.app X_1).app X_2) = id_{(G.obj X_1).obj X_2}$$$

Lean4

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

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