instHasRightCalculusOfFractionsHomotopyCategoryIntUpQuasiIso

English

The localization of a suitable category (here the quasi-isomorphisms in the right context) admits a right calculus of fractions.

Русский

Локализация подходящей категории (здесь правые квазиизоморфизмы) имеет правый расчёт дробей.

LaTeX

$$$(\\text{HomotopyCategory.quasiIso } C (\\text{ComplexShape.up } \\mathbb{Z})).HasRightCalculusOfFractions$$$

Lean4

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

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