English
If G is an equivalence and CatCommSq holds, then the companion G' is also an equivalence.
Русский
Если G — эквивалентность и CatCommSq выполняется, то сопутствующая G' тоже эквивалентна.
LaTeX
$$$G'.IsEquivalence$$$
Lean4
/-- If a localizer morphism induces an equivalence on some choice of localized categories,
it will be so for any choice of localized categories. -/
theorem isEquivalence_imp [G.IsEquivalence] : G'.IsEquivalence :=
let E₁ := Localization.uniq L₁ L₁' W₁
let E₂ := Localization.uniq L₂ L₂' W₂
let e : L₁ ⋙ G ⋙ E₂.functor ≅ L₁ ⋙ E₁.functor ⋙ G' :=
calc
L₁ ⋙ G ⋙ E₂.functor ≅ Φ.functor ⋙ L₂ ⋙ E₂.functor :=
(associator _ _ _).symm ≪≫ isoWhiskerRight (CatCommSq.iso Φ.functor L₁ L₂ G).symm E₂.functor ≪≫ associator _ _ _
_ ≅ Φ.functor ⋙ L₂' := (isoWhiskerLeft Φ.functor (compUniqFunctor L₂ L₂' W₂))
_ ≅ L₁' ⋙ G' := (CatCommSq.iso Φ.functor L₁' L₂' G')
_ ≅ L₁ ⋙ E₁.functor ⋙ G' := isoWhiskerRight (compUniqFunctor L₁ L₁' W₁).symm G' ≪≫ associator _ _ _
have := Functor.isEquivalence_of_iso (liftNatIso L₁ W₁ _ _ (G ⋙ E₂.functor) (E₁.functor ⋙ G') e)
Functor.isEquivalence_of_comp_left E₁.functor G'
