English
For a cochain complex K, the liftCycles map is iso exactly when a certain exactness and mono condition holds.
Русский
Для коцепочечного комплекса K отображение liftCycles является изоморфизмом тогда и только тогда, когда выполняются условия точности и моно.
LaTeX
$$$ \text{isIso}(K.liftCycles(\varphi,1,\text{by simp}, h\phi)) \iff ( ShortComplex.mk _ _ h\phi).Exact \land Mono \varphi $$$
Lean4
theorem isIso_liftCycles_iff (K : CochainComplex C ℕ) {X : C} (φ : X ⟶ K.X 0) [K.HasHomology 0] (hφ : φ ≫ K.d 0 1 = 0) :
IsIso (K.liftCycles φ 1 (by simp) hφ) ↔ (ShortComplex.mk _ _ hφ).Exact ∧ Mono φ :=
by
suffices
∀ (i : ℕ) (hx : (ComplexShape.up ℕ).next 0 = i) (hφ : φ ≫ K.d 0 i = 0),
IsIso (K.liftCycles φ i hx hφ) ↔ (ShortComplex.mk _ _ hφ).Exact ∧ Mono φ
from this 1 (by simp) hφ
rintro _ rfl hφ
let α : ShortComplex.mk (0 : X ⟶ X) (0 : X ⟶ X) (by simp) ⟶ K.sc 0 :=
{ τ₁ := 0
τ₂ := φ
τ₃ := 0 }
exact
(ShortComplex.quasiIso_iff_isIso_liftCycles α rfl rfl (by simp)).symm.trans
(ShortComplex.quasiIso_iff_of_zeros α rfl rfl (by simp))
