English
The symmetry of uniq with respect to exchanging the two localization functors is preserved: uniq L1 L2 W' symm = uniq L2 L1 W'.
Русский
Симметрия уникальности относительно обмена локализационных функторов сохраняется: uniq L1 L2 W' symm = uniq L2 L1 W'.
LaTeX
$$$\\mathrm{uniq}\\,L_1 L_2 W'\\!^{\\mathrm{symm}} = \\mathrm{uniq}\\,L_2 L_1 W'$.$$
Lean4
/-- If `L : C ⥤ D` is a localization for `W : MorphismProperty C`, then it is also
the case of a functor obtained by post-composing `L` with an equivalence of categories. -/
theorem of_equivalence_target {E : Type*} [Category E] (L' : C ⥤ E) (eq : D ≌ E) [L.IsLocalization W]
(e : L ⋙ eq.functor ≅ L') : L'.IsLocalization W :=
by
have h : W.IsInvertedBy L' := by
rw [← MorphismProperty.IsInvertedBy.iff_of_iso W e]
exact MorphismProperty.IsInvertedBy.of_comp W L (Localization.inverts L W) eq.functor
let F₁ := Localization.Construction.lift L (Localization.inverts L W)
let F₂ := Localization.Construction.lift L' h
let e' : F₁ ⋙ eq.functor ≅ F₂ := liftNatIso W.Q W (L ⋙ eq.functor) L' _ _ e
exact
{ inverts := h
isEquivalence := Functor.isEquivalence_of_iso e' }
