English
Exactness of the right-hand part of the opcycles map sequence is established in the right exact lemma.
Русский
Точность правой части последовательности отображений opcycles устанавливается в правой точной лемме.
LaTeX
$$$\text{opcycles_right_exact}$ (lemma statement)$$
Lean4
/-- If `X₁ ⟶ X₂ ⟶ X₃ ⟶ 0` is an exact sequence of homological complexes, then
`X₁.opcycles i ⟶ X₂.opcycles i ⟶ X₃.opcycles i ⟶ 0` is exact. This lemma states
the exactness at `X₂.opcycles i`, while the fact that `X₂.opcycles i ⟶ X₃.opcycles i`
is an epi is an instance. -/
theorem opcycles_right_exact (S : ShortComplex (HomologicalComplex C c)) (hS : S.Exact) [Epi S.g] (i : ι)
[S.X₁.HasHomology i] [S.X₂.HasHomology i] [S.X₃.HasHomology i] :
(ShortComplex.mk (opcyclesMap S.f i) (opcyclesMap S.g i)
(by rw [← opcyclesMap_comp, S.zero, opcyclesMap_zero])).Exact :=
by
have : Epi (ShortComplex.map S (eval C c i)).g := by dsimp; infer_instance
have hj := (hS.map (HomologicalComplex.eval C c i)).gIsCokernel
apply ShortComplex.exact_of_g_is_cokernel
refine
CokernelCofork.IsColimit.ofπ' _ _
(fun {A} k hk => by
dsimp at k hk ⊢
have H :=
CokernelCofork.IsColimit.desc' hj (S.X₂.pOpcycles i ≫ k)
(by
dsimp
rw [← p_opcyclesMap_assoc, hk, comp_zero])
dsimp at H
refine ⟨S.X₃.descOpcycles H.1 _ rfl ?_, ?_⟩
· rw [← cancel_epi (S.g.f (c.prev i)), comp_zero, Hom.comm_assoc, H.2, d_pOpcycles_assoc, zero_comp]
· rw [← cancel_epi (S.X₂.pOpcycles i), opcyclesMap_comp_descOpcycles, p_descOpcycles, H.2])
