of_isLocalization_of_isLocalization

English

If Φ is a localized equivalence, then the localized functor Φ.localizedFunctor L1 L2 is an equivalence.

Русский

Если Φ является локализованной эквивалентностью, то локализованный функтор Φ.localizedFunctor является эквивалентностью.

LaTeX

$$$(\Phi localizedFunctor L_1 L_2) \text{ is an equivalence}$$$

Lean4

/-- When `Φ : LocalizerMorphism W₁ W₂`, if the composition `Φ.functor ⋙ L₂` is a
localization functor for `W₁`, then `Φ` is a localized equivalence. -/
theorem of_isLocalization_of_isLocalization [(Φ.functor ⋙ L₂).IsLocalization W₁] : IsLocalizedEquivalence Φ :=
  by
  have : CatCommSq Φ.functor (Φ.functor ⋙ L₂) L₂ (𝟭 D₂) := CatCommSq.mk (rightUnitor _).symm
  exact IsLocalizedEquivalence.mk' Φ (Φ.functor ⋙ L₂) L₂ (𝟭 D₂)

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