English
Compatibility of the D1-differential with the total shift in the first index; expresses how the D1 map interacts with the totalShift1XIso hom component.
Русский
Совместимость D1-дифференциала с общим сдвигом по первому индексу; выражает влияние D1 на компоненту гомоморфизма totalShift1XIso.
LaTeX
$$$\\text{D₁-totalShift₁XIso-hom}$ states that for appropriate indices the homomorphism D₁ commutes (up to sign) with totalShift1XIso.$$
Lean4
instance : ((shiftFunctor₁ C x).obj K).HasTotal (up ℤ) := fun n =>
hasCoproduct_of_equiv_of_iso (K.toGradedObject.mapObjFun (π (up ℤ) (up ℤ) (up ℤ)) (n + x)) _
{ toFun := fun ⟨⟨a, b⟩, h⟩ =>
⟨⟨a + x, b⟩, by
simp only [Set.mem_preimage, π_def, Set.mem_singleton_iff] at h ⊢
cutsat⟩
invFun := fun ⟨⟨a, b⟩, h⟩ =>
⟨(a - x, b), by
simp only [Set.mem_preimage, π_def, Set.mem_singleton_iff] at h ⊢
cutsat⟩
left_inv := by
rintro ⟨⟨a, b⟩, h⟩
ext
· dsimp
cutsat
· rfl
right_inv := by
intro ⟨⟨a, b⟩, h⟩
ext
· dsimp
cutsat
· rfl }
(fun _ => Iso.refl _)
