map_comp_apply — Mathlib

English

Let p: X = Y and q: Y = Z be equalities. For x ∈ F.obj X, transporting along q after transporting along p equals transporting along p.trans q: F.map (eqToHom q) (F.map (eqToHom p) x) = F.map (eqToHom (p.trans q)) x.

Русский

Пусть p: X=Y и q:Y=Z — равенства. Для x ∈ F.obj X применение преобразования вдоль q после вдоль p равно преобразованию вдоль p.trans q: F.map (eqToHom q) (F.map (eqToHom p) x) = F.map (eqToHom (p.trans q)) x.

LaTeX

$$$$ F.map (eqToHom q) (F.map (eqToHom p) x) = F.map (eqToHom (p.trans q)) x. $$$$

Lean4

@[simp]
theorem map_comp_apply (f : X ⟶ Y) (g : Y ⟶ Z) (a : F.obj X) : (F.map (f ≫ g)) a = (F.map g) ((F.map f) a) := by simp

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