English
If X is strictly ≤ b and Y is strictly ≥ a and ≤ b, a morphism f: Q.obj X → Q.obj Y can be written with a Y' satisfying GE bounds and a quasi-iso s.
Русский
Если X ограничено сверху, Y ограничено GE сверху и снизу, то морфизм f распадается через Y' с GE‑ограничениями и квазиизоморфизмом s.
LaTeX
$$$\\exists Y', (Y'.IsStrictlyGE(a)) , (Y'.IsStrictlyLE(b)) , g : X \\to Y', (s : Y \\to Y') , (IsIso (Q.map s)), f = Q.map g \\circ inv(Q.map s)$$$
Lean4
/-- Any morphism `f : Q.obj X ⟶ Q.obj Y` in the derived category with `Y` strictly `≥ n`
can be written as `f = Q.map g ≫ inv (Q.map s)` with `g : X ⟶ Y'` and `s : Y ⟶ Y'`
a quasi-isomorphism with `Y'` strictly `≥ n`. -/
theorem left_fac_of_isStrictlyGE {X Y : CochainComplex C ℤ} (f : Q.obj X ⟶ Q.obj Y) (n : ℤ) [Y.IsStrictlyGE n] :
∃ (Y' : CochainComplex C ℤ) (_ : Y'.IsStrictlyGE n) (g : X ⟶ Y') (s : Y ⟶ Y') (_ : IsIso (Q.map s)),
f = Q.map g ≫ inv (Q.map s) :=
by
obtain ⟨Y', g, s, hs, rfl⟩ := left_fac f
have : IsIso (Q.map (CochainComplex.truncGEMap s n)) :=
by
rw [isIso_Q_map_iff_quasiIso, CochainComplex.quasiIso_truncGEMap_iff]
rw [isIso_Q_map_iff_quasiIso] at hs
infer_instance
refine
⟨Y'.truncGE n, inferInstance, X.πTruncGE n ≫ CochainComplex.truncGEMap g n,
Y.πTruncGE n ≫ CochainComplex.truncGEMap s n, ?_, ?_⟩
· rw [Q.map_comp]
infer_instance
· have eq := Q.congr_map (CochainComplex.πTruncGE_naturality s n)
have eq' := Q.congr_map (CochainComplex.πTruncGE_naturality g n)
simp only [Functor.map_comp] at eq eq'
simp only [Functor.map_comp,
← cancel_mono (Q.map (CochainComplex.πTruncGE Y n) ≫ Q.map (CochainComplex.truncGEMap s n)), assoc,
IsIso.inv_hom_id, comp_id]
simp only [eq, IsIso.inv_hom_id_assoc, eq']
