English
A morphism f in the derived category induces an isomorphism after applying Q-map if and only if f is a quasi-isomorphism in the underlying homotopy/homology context.
Русский
Для морфизма f из выводимой категории изоморфизм после применения Q-map iff f является квазиизоморфизмом в соответствующем контексте гомологии/гомотопии.
LaTeX
$$IsIso (Qh.map f) ↔ HomotopyCategory.quasiIso C _ f$$
Lean4
/-- Any morphism `f : Q.obj X ⟶ Q.obj Y` in the derived category with `X` strictly `≤ n`
can be written as `f = inv (Q.map s) ≫ Q.map g` with `s : X' ⟶ X` a quasi-isomorphism with
`X'` strictly `≤ n` and `g : X' ⟶ Y`. -/
theorem right_fac_of_isStrictlyLE {X Y : CochainComplex C ℤ} (f : Q.obj X ⟶ Q.obj Y) (n : ℤ) [X.IsStrictlyLE n] :
∃ (X' : CochainComplex C ℤ) (_ : X'.IsStrictlyLE n) (s : X' ⟶ X) (_ : IsIso (Q.map s)) (g : X' ⟶ Y),
f = inv (Q.map s) ≫ Q.map g :=
by
obtain ⟨X', s, hs, g, rfl⟩ := right_fac f
have : IsIso (Q.map (CochainComplex.truncLEMap s n)) :=
by
rw [isIso_Q_map_iff_quasiIso, CochainComplex.quasiIso_truncLEMap_iff]
rw [isIso_Q_map_iff_quasiIso] at hs
infer_instance
refine
⟨X'.truncLE n, inferInstance, CochainComplex.truncLEMap s n ≫ X.ιTruncLE n, ?_,
CochainComplex.truncLEMap g n ≫ Y.ιTruncLE n, ?_⟩
· rw [Q.map_comp]
infer_instance
· simp
