English
There is a factorization property for morphisms in the localized setting: a morphism can be represented as a fraction inv(s) ≫ g with s a morphism in the source and g a morphism to the target after passing to the localization.
Русский
Существование факторизации для морфизмов в локализованной категории: Морфизм представим как дробь inv(s) ≫ g, где s — морфизм в исходной категории, а g — морфизм к цели после локализации.
LaTeX
$$$\\exists X', s, g \\text{ with } IsIso(Q.map s) \\text{ and } f = inv(Q.map s) \\;\\gg\\; Q.map g$$$
Lean4
/-- Any morphism `f : Q.obj X ⟶ Q.obj Y` in the derived category can be written
as `f = inv (Q.map s) ≫ Q.map g` with `s : X' ⟶ X` a quasi-isomorphism and `g : X' ⟶ Y`. -/
theorem right_fac {X Y : CochainComplex C ℤ} (f : Q.obj X ⟶ Q.obj Y) :
∃ (X' : CochainComplex C ℤ) (s : X' ⟶ X) (_ : IsIso (Q.map s)) (g : X' ⟶ Y), f = inv (Q.map s) ≫ Q.map g :=
by
have ⟨φ, hφ⟩ := Localization.exists_rightFraction Qh (HomotopyCategory.quasiIso C _) f
obtain ⟨X', s, hs, g, rfl⟩ := φ.cases
obtain ⟨X', rfl⟩ := HomotopyCategory.quotient_obj_surjective X'
obtain ⟨s, rfl⟩ := (HomotopyCategory.quotient _ _).map_surjective s
obtain ⟨g, rfl⟩ := (HomotopyCategory.quotient _ _).map_surjective g
rw [← isIso_Qh_map_iff] at hs
exact ⟨X', s, hs, g, hφ⟩
