English
There is an equivalence of desc and inl structures linking fst, desc, and inr to the underlying cochain maps in degree shifts.
Русский
Существует связь эквивалентности структур desc и inl, связывающая fst, desc и inr с соответствующими коchейн-морфизмами на сдвиге степеней.
LaTeX
$$$\text{InlDescEquiv}(φ, α, β, eq) :\text{fst}, \text{desc}, \text{inr}$$$
Lean4
theorem δ_liftCochain (m' : ℤ) (hm' : m + 1 = m') :
δ n m (liftCochain φ α β h) =
-(δ m m' α).comp (inl φ) (by cutsat) +
(δ n m β + α.comp (Cochain.ofHom φ) (add_zero m)).comp (Cochain.ofHom (inr φ)) (add_zero m) :=
by
dsimp only [liftCochain]
simp only [δ_add, δ_comp α (inl φ) _ m' _ _ h hm' (neg_add_cancel 1), δ_comp_zero_cochain _ _ _ h, δ_inl,
Cochain.ofHom_comp, Int.negOnePow_neg, Int.negOnePow_one, Units.neg_smul, one_smul, δ_ofHom, Cochain.comp_zero,
zero_add, Cochain.add_comp, Cochain.comp_assoc_of_second_is_zero_cochain]
abel
