Theorems · Theorem · category theory

CategoryTheory.Localization.isEquivalence

∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_4} {D₂ : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_4, u_4} D₁]
  [inst_3 : CategoryTheory.Category.{v_5, u_5} D₂] (L₁ : CategoryTheory.Functor C₁ D₁)
  (W₁ : CategoryTheory.MorphismProperty C₁) [L₁.IsLocalization W₁] (L₂ : CategoryTheory.Functor C₂ D₂)
  (W₂ : CategoryTheory.MorphismProperty C₂) [L₂.IsLocalization W₂] (G : CategoryTheory.Functor C₁ D₂)
  (G' : CategoryTheory.Functor D₁ D₂) [CategoryTheory.Localization.Lifting L₁ W₁ G G']
  (F : CategoryTheory.Functor C₂ D₁) (F' : CategoryTheory.Functor D₂ D₁)
  [CategoryTheory.Localization.Lifting L₂ W₂ F F'] (α : G.comp F' ≅ L₁) (β : F.comp G' ≅ L₂), G'.IsEquivalence

Basic constructor of an equivalence between localized categories

Defined in

Mathlib.CategoryTheory.Localization.Equivalence

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Functor.IsLocalizationCategoryTheory.Functor.IsLocalizationCategoryTheory.Localization.LiftingCategoryTheory.Localization.Lifting