changeFunctor_trans — Mathlib

English

Compatibility of changeFunctor with composition of isomorphisms of functors: composing iso₁ then iso₂ gives the same result as a single composite iso.

Русский

Совместимость changeFunctor с композициями изоморфизмов функторов: композиция iso₁ ∘ iso₂ равна единому композитному изоморфизму.

LaTeX

$$$(e.changeFunctor iso_1).changeFunctor iso_2 = e.changeFunctor (iso_1 \ll iso_2)$$$

Lean4

/-- Compatibility of `changeFunctor` with the composition of isomorphisms of functors -/
theorem changeFunctor_trans (e : C ≌ D) {G G' : C ⥤ D} (iso₁ : e.functor ≅ G) (iso₂ : G ≅ G') :
    (e.changeFunctor iso₁).changeFunctor iso₂ = e.changeFunctor (iso₁ ≪≫ iso₂) := by cat_disch

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