shiftMap_zero — Mathlib

English

Relates shift iso hom-application when the added indices sum to zero; expresses a canonical simplification using shiftFunctorZero'.

Русский

Связывает гом-апп изоморфии сдвига при сложении индексов, равных нулю; использует каноническое упрощение через shiftFunctorZero'.

LaTeX

$$$[F.ShiftSequence G] {X Y} {m} (f : X ⟶ Y⟦m⟧) (n) (hnm : n + m = 0) (a a' : G) (ha' : m + a = a') :\ (F.shiftIso n a' a (by rw [\lt- ha', \lt- add_assoc, hnm])).hom.app X = \ (F.shift a').map (f⟦n⟧' ≫ (shiftFunctorCompIsoId C m n (by rw [\lt- add_left_inj m, \lt- add_assoc, hnm, \lt- add, \lt- add_zero])).hom.app Y) $$$

Lean4

@[simp]
theorem shiftMap_zero (X Y : C) (n a a' : M) (ha' : n + a = a') : F.shiftMap (0 : X ⟶ Y⟦n⟧) a a' ha' = 0 := by
  simp [shiftMap]

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