English
Associated to a degreewise split short exact sequence of cochain complexes, there is a natural 1-cocycle determined by the splitting data, giving a canonical cocycle in the appropriate cochain Hom complex.
Русский
К связанному степенью разложенному короткому точному решению коцепановых комплексов соответствует естественный 1-коцикл, определяемый разбиением, задающий канонический кокцикл в соответствующем комплексе гомоморфизмов.
LaTeX
$$$\\text{cocycleOfDegreewiseSplit } S \\sigma : \\text{CochainComplex.HomComplex}(S.X_3,S.X_1,1)$$$
Lean4
/-- The `1`-cocycle attached to a degreewise split short exact sequence of cochain complexes. -/
def cocycleOfDegreewiseSplit : Cocycle S.X₃ S.X₁ 1 :=
Cocycle.mk (Cochain.mk (fun p q _ => (σ p).s ≫ S.X₂.d p q ≫ (σ q).r)) 2 (by cutsat)
(by
ext p _ rfl
have := mono_of_mono_fac (σ (p + 2)).f_r
have r_f := fun n => (σ n).r_f
have s_g := fun n => (σ n).s_g
dsimp at this r_f s_g ⊢
rw [δ_v 1 2 (by cutsat) _ p (p + 2) (by cutsat) (p + 1) (p + 1) (by cutsat) (by cutsat), Cochain.mk_v,
Cochain.mk_v, show Int.negOnePow 2 = 1 by rfl, one_smul, assoc, assoc, ← cancel_mono (S.f.f (p + 2)), add_comp,
assoc, assoc, assoc, assoc, assoc, assoc, zero_comp, ← S.f.comm, reassoc_of% (r_f (p + 1)), sub_comp, comp_sub,
comp_sub, assoc, id_comp, d_comp_d, comp_zero, zero_sub, ← S.g.comm_assoc, reassoc_of% (s_g p), r_f (p + 2),
comp_sub, comp_sub, comp_id, comp_sub, ← S.g.comm_assoc, reassoc_of% (s_g (p + 1)), d_comp_d_assoc, zero_comp,
sub_zero, neg_add_cancel])
