eqToHom_map_comp — Mathlib

English

For any F: C ⥤ D and p: X = Y, q: Y = Z, the composition of the two eqToHom maps equals the eqToHom of the transitive composition: F.map (eqToHom p) ≫ F.map (eqToHom q) = F.map (eqToHom (p.trans q)).

Русский

Для любого F: C ⥤ D и p: X = Y, q: Y = Z, композиция двух отображений eqToHom равна eqToHom от трансп. композиции: F.map (eqToHom p) ≫ F.map (eqToHom q) = F.map (eqToHom (p.trans q)).

LaTeX

$$$ F.map (eqToHom p) \\; \\circ\\; F.map (eqToHom q) = F.map (eqToHom (p \\text{ trans } q)) $$$

Lean4

@[reassoc (attr := simp)]
theorem eqToHom_map_comp (F : C ⥤ D) {X Y Z : C} (p : X = Y) (q : Y = Z) :
    F.map (eqToHom p) ≫ F.map (eqToHom q) = F.map (eqToHom <| p.trans q) := by cat_disch

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