mapIso_trans — Mathlib

English

A functor preserves the composition of isomorphisms: F.mapIso (i ≪≫ j) = F.mapIso i ≪≫ F.mapIso j.

Русский

Функтор сохраняет композицию изоморфизмов: F.mapIso (i ≪≫ j) = F.mapIso i ≪≫ F.mapIso j.

LaTeX

$$$F.mapIso (i \\llamparrow j) = (F.mapIso i) \\llamparrow (F.mapIso j)$$$

Lean4

@[simp]
theorem mapIso_trans (F : C ⥤ D) {X Y Z : C} (i : X ≅ Y) (j : Y ≅ Z) : F.mapIso (i ≪≫ j) = F.mapIso i ≪≫ F.mapIso j :=
  by ext; apply Functor.map_comp

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