English
If a morphism property factors through localization and its induced class on the quotient yields a localization, then the associated localizer morphism is an equivalence.
Русский
Если свойство морфизмов факorizуется через локализацию и индуцированный на фактор-категории класс дает локализацию, то соответствующая локализующая морфизм эквивалентен.
LaTeX
$$$\text{IsLocalizedEquivalence}((\mathrm{LocalizerMorphism}.ofEq\;hW))$$$
Lean4
/-- If `homRel : HomRel C` satisfies `homRel.FactorsThroughLocalization W` and
that the class of morphisms `W` induces a class of morphism `W'` on the quotient category,
then the localizer morphism given by the functor `Quotient.functor HomRel : C ⥤ Quotient homRel`
induces equivalences on localized categories. -/
theorem isLocalizedEquivalence : (LocalizerMorphism.ofEq hW).IsLocalizedEquivalence :=
have : ((LocalizerMorphism.ofEq hW).functor ⋙ W'.Q).IsLocalization W :=
Functor.IsLocalization.mk' _ _ (h.strictUniversalPropertyFixedTarget' hW _)
(h.strictUniversalPropertyFixedTarget' hW _)
LocalizerMorphism.IsLocalizedEquivalence.of_isLocalization_of_isLocalization _ W'.Q
