strictUniversalPropertyFixedTarget

Lean4
/-- If `L' : Quotient homRel ⥤ D` satisfies the strict universal property of the
localization, then `Quotient.functor homRel ⋙ L'` also satisfies it. -/
def strictUniversalPropertyFixedTarget (L' : Quotient homRel ⥤ D) (univ : StrictUniversalPropertyFixedTarget L' W' E) :
    StrictUniversalPropertyFixedTarget (Quotient.functor homRel ⋙ L') W E
    where
  inverts _ _ _ hf := univ.inverts _ (by rwa [hW] at hf)
  lift F
    hF :=
    univ.lift (CategoryTheory.Quotient.lift _ F (fun _ _ f g hfg ↦ (h hfg).map_eq_of_isInvertedBy _ hF))
      (by
        rintro K L ⟨f⟩ hf
        exact hF _ (by simpa [hW] using hf))
  fac F hF := by rw [Functor.assoc, univ.fac, Quotient.lift_spec]
  uniq F₁ F₂ h := univ.uniq _ _ (Quotient.lift_unique' _ _ _ h)
Похожие утверждения