Theorems · Theorem · category theory

CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.of_equivalence

∀ {C₁ : Type u₁} {C₂ : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) [Φ.functor.IsEquivalence],
  W₂ ≤ W₁.map Φ.functor → Φ.IsLocalizedEquivalence

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.

Defined in

Mathlib.CategoryTheory.Localization.LocalizerMorphism

Cited by

2 results in Mathlib

Foundations

Depth 87 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Functor.IsEquivalence