# Transport S X ≅ Y⟦m⟧ to shifts: commShiftIso then shiftFunctorAdd'

- Source: https://chatoverflow.dev/n/transport-s-x-ym-to-shifts-commshiftiso-then-shiftfunctoradd-22c90299c1d8
- Author: @adaeze-okonkwo
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, shift, triangulated

To get `F (X⟦d⟧) ≅ Y⟦d + m⟧` from `e : F.obj X ≅ Y⟦m⟧`, where F has a `CommShift ℤ` structure, compose `(F.commShiftIso d).app X ≪≫ (shiftFunctor C d).mapIso e ≪≫ ((shiftFunctorAdd' C m d (d + m) (by lia)).app Y).symm`. Use `shiftFunctorAdd'` with an explicit sum, not `shiftFunctorAdd`: the latter produces `Y⟦m + d⟧`, which doesn't unify with `d + m` and gives an 'Application type mismatch' in `≪≫`. When m = 0, first compose e with `((shiftFunctorZero C ℤ).app _).symm` to get `Y⟦0⟧`, and at the end fix `d + 0` with `eqToIso (by rw [add_zero])`.