English
If 0 → X₁ → X₂ → X₃ is exact, then 0 → X₁.cycles i → X₂.cycles i → X₃.cycles i is exact at X₂.cycles i.
Русский
Если 0 → X₁ → X₂ → X₃ точна, то 0 → X₁.cycles i → X₂.cycles i → X₃.cycles i точна в X₂.cycles i.
LaTeX
$$$0 \to X_1^{\mathrm{cycles}}(i) \to X_2^{\mathrm{cycles}}(i) \to X_3^{\mathrm{cycles}}(i)$ is exact at $X_2^{\mathrm{cycles}}(i)$$$
Lean4
/-- If `0 ⟶ X₁ ⟶ X₂ ⟶ X₃` is an exact sequence of homological complex, then
`0 ⟶ X₁.cycles i ⟶ X₂.cycles i ⟶ X₃.cycles i` is exact. This lemma states
the exactness at `X₂.cycles i`, while the fact that `X₁.cycles i ⟶ X₂.cycles i`
is a mono is an instance. -/
theorem cycles_left_exact (S : ShortComplex (HomologicalComplex C c)) (hS : S.Exact) [Mono S.f] (i : ι)
[S.X₁.HasHomology i] [S.X₂.HasHomology i] [S.X₃.HasHomology i] :
(ShortComplex.mk (cyclesMap S.f i) (cyclesMap S.g i) (by rw [← cyclesMap_comp, S.zero, cyclesMap_zero])).Exact :=
by
have : Mono (ShortComplex.map S (eval C c i)).f := by dsimp; infer_instance
have hi := (hS.map (HomologicalComplex.eval C c i)).fIsKernel
apply ShortComplex.exact_of_f_is_kernel
exact
KernelFork.IsLimit.ofι' _ _
(fun {A} k hk => by
dsimp at k hk ⊢
have H :=
KernelFork.IsLimit.lift' hi (k ≫ S.X₂.iCycles i)
(by
dsimp
rw [assoc, ← cyclesMap_i, reassoc_of% hk, zero_comp])
dsimp at H
refine ⟨S.X₁.liftCycles H.1 _ rfl ?_, ?_⟩
· rw [← cancel_mono (S.f.f _), assoc, zero_comp, ← Hom.comm, reassoc_of% H.2, iCycles_d, comp_zero]
· rw [← cancel_mono (S.X₂.iCycles i), liftCycles_comp_cyclesMap, liftCycles_i, H.2])
