English
Let F, G be cochain complexes with a morphism φ: F → G that admits a homotopy cofibre. In the mapping cone construction, given suitable cochains α, β, α', β' and integers, the v-component of the lifted Cochain and the descendant v-component satisfy a bilinear relation: the composition of lift with desc equals the sum of two natural composites built from α, α' and β, β'.
Русский
Пусть F, G — когерентные комплексы и есть морфизм φ: F → G, существующий когировосстановимый перенос. В построении отображающего конуса для ког-произведения существует тождество в векторовой компоненты: композиция lift затем desc равна сумме двух композиции, построенных из α, α' и β, β'.
LaTeX
$$$\\text{For suitable } p_1,p_2,p_3\\in\\mathbb{Z},\\ h_{12},h_{23},q,hq:\\mathbb{Z}\\text{ with }p_1+n=p_2,\\ p_2+n'=p_3,\\ p_1+m=q,\\ n+n'=p,\\ \\text{the identity holds:} \n\\n(\\mathrm{lift}_{\\varphi}(\\alpha,\\beta,h)).v_{p_1p_2}^{h_{12}} \ \\, ·\\ (\\mathrm{desc}_{\\varphi}(\\alpha',\\beta',h')).v_{p_2p_3}^{h_{23}} \ = \ \\alpha.v_{p_1q}^{hq} \\cdot \\alpha'.v_{qn}^{(hnn')} \ + \ \\beta.v_{p_1p_2}^{h_{12}} \\cdot \\beta'.v_{p_2p_3}^{h_{23}},$$$
Lean4
theorem liftCochain_v_descCochain_v (p₁ p₂ p₃ : ℤ) (h₁₂ : p₁ + n = p₂) (h₂₃ : p₂ + n' = p₃) (q : ℤ) (hq : p₁ + m = q) :
(liftCochain φ α β h).v p₁ p₂ h₁₂ ≫ (descCochain φ α' β' h').v p₂ p₃ h₂₃ =
α.v p₁ q hq ≫ α'.v q p₃ (by cutsat) + β.v p₁ p₂ h₁₂ ≫ β'.v p₂ p₃ h₂₃ :=
by
have eq := Cochain.congr_v (liftCochain_descCochain φ α β α' β' h h' p hp) p₁ p₃ (by cutsat)
simpa only [Cochain.comp_v _ _ hp p₁ p₂ p₃ h₁₂ h₂₃, Cochain.add_v,
Cochain.comp_v _ _ _ _ _ _ hq (show q + m' = p₃ by cutsat)] using eq
