Theorems · Theorem · category theory

CategoryTheory.LocalizerMorphism.isLocalizedEquivalence_of_unit_of_unit

∀ {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₂)
  (Ψ : CategoryTheory.LocalizerMorphism W₂ W₁) (ε₁ : CategoryTheory.Functor.id C₁ ⟶ Φ.functor.comp Ψ.functor)
  (ε₂ : CategoryTheory.Functor.id C₂ ⟶ Ψ.functor.comp Φ.functor),
  (∀ (X₁ : C₁), W₁ (ε₁.app X₁)) → (∀ (X₂ : C₂), W₂ (ε₂.app X₂)) → Φ.IsLocalizedEquivalence

Defined in

Mathlib.CategoryTheory.Localization.LocalizerMorphism

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Category