isEquivalence — Mathlib

English

If a LocalizerMorphism Φ is a localized equivalence, then any compatible functor between localized categories yields an equivalence.

Русский

Если LocalizerMorphism Φ является локализованной эквивалентностью, то любая совместимая с ней пара локализованных функторов порождает эквивалентность.

LaTeX

$$$\text{IsLocalizedEquivalence}(Φ) \Rightarrow (\text{for compatible } F,G,\ (F.localized) \text{ is equivalence})$$$

Lean4

/-- If a `LocalizerMorphism` is a localized equivalence, then any compatible functor
between the localized categories is an equivalence. -/
theorem isEquivalence [h : Φ.IsLocalizedEquivalence] [CatCommSq Φ.functor L₁ L₂ G] : G.IsEquivalence :=
  (by
    rw [Φ.isEquivalence_iff L₁ L₂ G W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)]
    exact h.isEquivalence)

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