English
If X is strictly LE and Y is strictly GE, then any f: Q.obj X → Q.obj Y admits a representation with truncated maps respecting LE/GE bounds and a quasi-iso.
Русский
Если X имеет строгое ограничение снизу, а Y — сверху, то любой f имеет представление через тротеки, соблюдающие границы LE/GE и квазиизоморфизм.
LaTeX
$$$\\exists X', (X'.IsStrictlyGE(a)) , (X'.IsStrictlyLE(b)) , (s : X' \\to X) , (IsIso (Q.map s)) , (g : X' \\to Y), f = inv(Q.map s) \\circ Q.map g$$$
Lean4
/-- Any morphism `f : Q.obj X ⟶ Q.obj Y` in the derived category
with `X` strictly `≥ a` and `≤ b`, and `Y` strictly `≥ a`
can be written as `f = inv (Q.map s) ≫ Q.map g` with `s : X' ⟶ X`
a quasi-isomorphism with `X'` strictly `≥ a` and `≤ b`, and `g : X' ⟶ Y`. -/
theorem right_fac_of_isStrictlyLE_of_isStrictlyGE {X Y : CochainComplex C ℤ} (a b : ℤ) [X.IsStrictlyGE a]
[X.IsStrictlyLE b] [Y.IsStrictlyGE a] (f : Q.obj X ⟶ Q.obj Y) :
∃ (X' : CochainComplex C ℤ) (_ : X'.IsStrictlyGE a) (_ : X'.IsStrictlyLE b) (s : X' ⟶ X) (_ : IsIso (Q.map s)) (g :
X' ⟶ Y), f = inv (Q.map s) ≫ Q.map g :=
by
obtain ⟨X', hX', s, hs, g, fac⟩ := right_fac_of_isStrictlyLE f b
have : IsIso (Q.map (CochainComplex.truncGEMap s a)) :=
by
rw [isIso_Q_map_iff_quasiIso] at hs
rw [isIso_Q_map_iff_quasiIso, CochainComplex.quasiIso_truncGEMap_iff]
infer_instance
refine
⟨X'.truncGE a, inferInstance, inferInstance, CochainComplex.truncGEMap s a ≫ inv (X.πTruncGE a), ?_,
CochainComplex.truncGEMap g a ≫ inv (Y.πTruncGE a), ?_⟩
· rw [Q.map_comp]
infer_instance
· simp only [Functor.map_comp, Functor.map_inv, IsIso.inv_comp, IsIso.inv_inv, assoc, fac, ← cancel_epi (Q.map s),
IsIso.hom_inv_id_assoc]
rw [← Functor.map_comp_assoc, ← CochainComplex.πTruncGE_naturality s a, Functor.map_comp, assoc,
IsIso.hom_inv_id_assoc, ← Functor.map_comp_assoc, CochainComplex.πTruncGE_naturality g a, Functor.map_comp, assoc,
IsIso.hom_inv_id, comp_id]
