Theorems · Definition · category theory

CategoryTheory.LocalizerMorphism.inv

{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] → [Φ.IsInduced] → [W₂.RespectsIso] → CategoryTheory.LocalizerMorphism W₂ W₁

The inverse of a localizer morphism Φ : LocalizerMorphism W₁ W₂, when Φ.functor is an equivalence, W₁ is induced by W₂ and W₂ respects isomorphisms.

Defined in

Mathlib.CategoryTheory.Localization.LocalizerMorphism

Cited by

3 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Functor.IsEquivalenceCategoryTheory.LocalizerMorphism.IsInducedCategoryTheory.MorphismProperty.RespectsIso