English
In a balanced abelian context, S.Exact ∧ Epi S.g holds if and only if the colimit of the cokernel fork exists, i.e., is the cokernel of π.
Русский
В сбалансированной абелевой категории: S.Exact ∧ Epi S.g эквивалентны существованию колимита форка кокernel, то есть кокernel π существует.
LaTeX
$$$S.Exact \land \mathrm{Epi}(S.g) \iff \exists\; \mathrm{IsColimit}(\mathrm{CokernelCofork.of\pi}\; S.g\; S.zero)$$$
Lean4
/-- Given a morphism of short complexes `φ : S₁ ⟶ S₂` in an abelian category, if `S₁.f`
and `S₁.g` are zero (e.g. when `S₁` is of the form `0 ⟶ S₁.X₂ ⟶ 0`) and `S₂.f = 0`
(e.g when `S₂` is of the form `0 ⟶ S₂.X₂ ⟶ S₂.X₃`), then `φ` is a quasi-isomorphism iff
the obvious short complex `S₁.X₂ ⟶ S₂.X₂ ⟶ S₂.X₃` is exact and `φ.τ₂` is a mono). -/
theorem quasiIso_iff_of_zeros {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (hf₁ : S₁.f = 0) (hg₁ : S₁.g = 0)
(hf₂ : S₂.f = 0) : QuasiIso φ ↔ (ShortComplex.mk φ.τ₂ S₂.g (by rw [φ.comm₂₃, hg₁, zero_comp])).Exact ∧ Mono φ.τ₂ :=
by
have w : φ.τ₂ ≫ S₂.g = 0 := by rw [φ.comm₂₃, hg₁, zero_comp]
rw [quasiIso_iff_isIso_liftCycles φ hf₁ hg₁ hf₂]
constructor
· intro h
have : Mono φ.τ₂ := by
rw [← S₂.liftCycles_i φ.τ₂ w]
apply mono_comp
refine ⟨?_, this⟩
apply exact_of_f_is_kernel
exact IsLimit.ofIsoLimit S₂.cyclesIsKernel (Fork.ext (asIso (S₂.liftCycles φ.τ₂ w)).symm (by simp))
· rintro ⟨h₁, h₂⟩
refine ⟨⟨h₁.lift S₂.iCycles (by simp), ?_, ?_⟩⟩
· rw [← cancel_mono φ.τ₂, assoc, h₁.lift_f, liftCycles_i, id_comp]
· rw [← cancel_mono S₂.iCycles, assoc, liftCycles_i, h₁.lift_f, id_comp]
