Certain quotient categories are localizations

Let r : HomRel C be a relation on morphisms in a category C and W : MorphismProperty C. We assume that W is inverted by the quotient functor functor r : C ⥤ quotient r. If any relation r f₀ f₁ between morphisms f₀ : X ⟶ Y and f₁ : X ⟶ Y can be "explained" by the use of a homotopy involving a cylinder object (i.e. there exists an object cylinder : C, a morphism π : cylinder ⟶ X in W, a morphism φ : cylinder ⟶ Y and two sections i₀ and i₁ to π such that i₀ ≫ φ = f₀ and i₁ ≫ φ = f₁), then functor r : C ⥤ quotient r is a localization functor for W. We also deduce a slightly more general result involving a full and essentially surjective functor L : C ⥤ D instead of the quotient functor functor r : C ⥤ quotient r. Dual results involving path objects are also obtained.

theorem CategoryTheory.Quotient.isLocalization_functor {C : Type u_1} [Category.{v_1, u_1} C] (r : HomRel C) (W : MorphismProperty C) (hW : W.IsInvertedBy (functor r)) (hr : ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), r f₀ f₁ → ∃ (P : HomotopicalAlgebra.Precylinder X) (x : P.LeftHomotopy f₀ f₁), W P.π) : (functor r).IsLocalization W

theorem CategoryTheory.Functor.isLocalization_of_essSurj_of_full_of_exists_cylinders {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (L : Functor C D) [L.EssSurj] [L.Full] (W : MorphismProperty C) (hW : W.IsInvertedBy L) (hr : ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), L.map f₀ = L.map f₁ → ∃ (P : HomotopicalAlgebra.Precylinder X) (x : P.LeftHomotopy f₀ f₁), W P.π) : L.IsLocalization W

theorem CategoryTheory.Functor.isLocalization_of_essSurj_of_full_of_exists_pathObjects {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (L : Functor C D) [L.EssSurj] [L.Full] (W : MorphismProperty C) (hW : W.IsInvertedBy L) (hr : ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), L.map f₀ = L.map f₁ → ∃ (P : HomotopicalAlgebra.PrepathObject Y) (x : P.RightHomotopy f₀ f₁), W P.ι) : L.IsLocalization W

theorem CategoryTheory.Quotient.isLocalization_functor' {C : Type u_1} [Category.{v_1, u_1} C] (r : HomRel C) [Congruence r] (W : MorphismProperty C) (hW : W.IsInvertedBy (functor r)) (hr : ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), r f₀ f₁ → ∃ (P : HomotopicalAlgebra.PrepathObject Y) (x : P.RightHomotopy f₀ f₁), W P.ι) : (functor r).IsLocalization W