eqToIso_map_trans — Mathlib

English

Exactly expresses the compatibility of transporting along two equalities with the functorial mapping of isomorphisms.

Русский

Точно выражает совместимость переноса вдоль двух равенств с отображением изоморфизмов функтором.

LaTeX

$$$F.mapIso(\\mathrm{eqToIso}(p)) \\circ F.mapIso(\\mathrm{eqToIso}(q)) = F.mapIso(\\mathrm{eqToIso}(p\\,\\mathrm{.trans}\\, q))$$$

Lean4

@[simp]
theorem eqToIso_map_trans (F : C ⥤ D) {X Y Z : C} (p : X = Y) (q : Y = Z) :
    F.mapIso (eqToIso p) ≪≫ F.mapIso (eqToIso q) = F.mapIso (eqToIso <| p.trans q) := by cat_disch

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