English
Two localized functors G and G' are equivalent in the sense of IsEquivalence iff under Φ.isEquivalence_iff they agree.
Русский
У локализованных функторов G и G' условие IsEquivalence эквивалентно их равенству по Φ.isEquivalence_iff.
LaTeX
$$$G.IsEquivalence \iff G'.IsEquivalence$$$
Lean4
/-- When the underlying functor `Φ.functor` of `Φ : LocalizerMorphism W₁ W₂` is
an equivalence of categories and that `W₁` and `W₂` essentially correspond to each
other via this equivalence, then `Φ` is a localized equivalence. -/
theorem of_equivalence [Φ.functor.IsEquivalence] (h : W₂ ≤ W₁.map Φ.functor) : IsLocalizedEquivalence Φ :=
by
haveI : Functor.IsLocalization (Φ.functor ⋙ MorphismProperty.Q W₂) W₁ :=
by
refine
Functor.IsLocalization.of_equivalence_source W₂.Q W₂ (Φ.functor ⋙ W₂.Q) W₁ (asEquivalence Φ.functor).symm ?_
(Φ.inverts W₂.Q) ((associator _ _ _).symm ≪≫ isoWhiskerRight ((Equivalence.unitIso _).symm) _ ≪≫ leftUnitor _)
erw [W₁.isoClosure.inverseImage_equivalence_functor_eq_map_inverse]
rw [MorphismProperty.map_isoClosure]
exact h
exact IsLocalizedEquivalence.of_isLocalization_of_isLocalization Φ W₂.Q
