English
For a morphism φ: F → G of cochain complexes with a homotopy cofibre, and cocycles α, β and their companions α', β', the f-component relation in the lifting and descending maps is a sum of two composites: α with α' and β with β'.
Русский
Для морфизма φ: F → G когцепных комплексов с гомотопией кофигуратора, а также кохайн α, β и их пары α', β', равенство компонентов f для подъема и спуска выражается суммой двух композиционных выражений: α с α' и β с β'.
LaTeX
$$$\\text{If } α,β,α',β'\\text{ satisfy } δ(-1,0)α' = φ \\circ β'\\text{ and } δ(0,1)β + α.1 \\circ (φ) = 0, \n(\\mathrm{lift}_{\\varphi}(α,β,eq)).f_n = α.1.v_{n,n'} \\circ α'.v_{n'n} + β.v_{n,n} \\circ β'.f_n$$$
Lean4
theorem lift_desc_f {K L : CochainComplex C ℤ} (α : Cocycle K F 1) (β : Cochain K G 0)
(eq : δ 0 1 β + α.1.comp (Cochain.ofHom φ) (add_zero 1) = 0) (α' : Cochain F L (-1)) (β' : G ⟶ L)
(eq' : δ (-1) 0 α' = Cochain.ofHom (φ ≫ β')) (n n' : ℤ) (hnn' : n + 1 = n') :
(lift φ α β eq).f n ≫ (desc φ α' β' eq').f n =
α.1.v n n' hnn' ≫ α'.v n' n (by omega) + β.v n n (add_zero n) ≫ β'.f n :=
by
simp only [lift, desc, Cocycle.homOf_f, liftCocycle_coe, descCocycle_coe, Cocycle.ofHom_coe,
liftCochain_v_descCochain_v φ α.1 β α' (Cochain.ofHom β') (zero_add 1) (neg_add_cancel 1) 0 (add_zero 0) n n n
(add_zero n) (add_zero n) n' hnn',
Cochain.ofHom_v]
