strictUniversalPropertyFixedTarget'

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 `Quotient.functor homRel ⋙ W'.Q` satisfies the universal property of the
localization. This is used in `HomRel.FactorsThroughLocalization.isLocalizedEquivalence`
in order to show that as a localizer morphism, the quotient functor induces an
equivalence on localized categories. -/
noncomputable def strictUniversalPropertyFixedTarget' :
    StrictUniversalPropertyFixedTarget (Quotient.functor homRel ⋙ W'.Q) W E :=
  strictUniversalPropertyFixedTarget h hW _ (strictUniversalPropertyFixedTargetQ W' E)

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