English
Localization commuting with equivalences: a localization can be transported along equivalences to obtain a localization on the equivalent categories.
Русский
Локализация совместима с эквивалентностями: локализация может быть перенесена через эквивалентности на эквивалентные категории.
LaTeX
$$$L_2 = E.functor \\circ L_1 \\circ E'.inverse$, $L_2.IsLocalization W_2$$$
Lean4
/-- If `L₁ : C₁ ⥤ D₁` is a localization functor for `W₁ : MorphismProperty C₁`, then if we
transport this functor `L₁` via equivalences `C₁ ≌ C₂` and `D₁ ≌ D₂` to get a functor
`L₂ : C₂ ⥤ D₂`, then `L₂` is also a localization functor for
a suitable `W₂ : MorphismProperty C₂`. -/
theorem of_equivalences (L₁ : C₁ ⥤ D₁) (W₁ : MorphismProperty C₁) [L₁.IsLocalization W₁] (L₂ : C₂ ⥤ D₂)
(W₂ : MorphismProperty C₂) (E : C₁ ≌ C₂) (E' : D₁ ≌ D₂) [CatCommSq E.functor L₁ L₂ E'.functor]
(hW₁ : W₁ ≤ W₂.isoClosure.inverseImage E.functor) (hW₂ : W₂.IsInvertedBy L₂) : L₂.IsLocalization W₂ :=
by
haveI : (E.functor ⋙ L₂).IsLocalization W₁ := of_equivalence_target L₁ W₁ _ E' ((CatCommSq.iso _ _ _ _).symm)
exact of_equivalence_source (E.functor ⋙ L₂) W₁ L₂ W₂ E hW₁ hW₂ (Iso.refl _)
