instHasLeftCalculusOfFractionsHomotopyCategoryIntUpQuasiIso

English

Every morphism f in the derived category can be written as f = inv(Q.map s) ≫ Q.map g for some X', a quasi-isomorphism s: X' → X, and a morphism g: X' → Y.

Русский

Каждый морфизм f в выводимой категории можно разложить как f = inv(Q.map s) ≫ Q.map g, где s: X' → X является квазиизом, и g: X' → Y.

LaTeX

$$$\\exists X', s, (hs : IsIso (Q.map s)), g:\\, X' \\to Y, \\quad f = inv(Q.map s) \\;\\gg\\; Q.map g$$$

Lean4

instance : (HomotopyCategory.quasiIso C (ComplexShape.up ℤ)).HasLeftCalculusOfFractions :=
  by
  rw [HomotopyCategory.quasiIso_eq_subcategoryAcyclic_W]
  infer_instance

Похожие утверждения