hom_inv_id_app_app — Mathlib

English

For an isomorphism α: F ≅ G of functors, the composite maps at each level form an isomorphism; i.e., (α.hom.app X₁).app X₂ is an isomorphism for all X₁,X₂.

Русский

Для изоморфизма α: F ≅ G над функторами композиция отображений на каждом уровне образует изоморфизм; то есть (α.hom.app X₁).app X₂ изоморфна для всех X₁, X₂.

LaTeX

$$$ \forall X_1:\, C,\forall X_2:\, D,\ IsIso( (\alpha.hom.app X_1).app X_2 ) $$$

Lean4

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

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