Theorems · Theorem · category theory

CategoryTheory.LocalizerMorphism.hasLeftResolutions_arrow_iff_of_equivalences

∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D₁]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {W₁' : CategoryTheory.MorphismProperty D₁}
  {W₂' : CategoryTheory.MorphismProperty D₂} {T : CategoryTheory.LocalizerMorphism W₁ W₂}
  {L : CategoryTheory.LocalizerMorphism W₁ W₁'} {R : CategoryTheory.LocalizerMorphism W₂ W₂'}
  {B : CategoryTheory.LocalizerMorphism W₁' W₂'} [R.functor.IsEquivalence] [R.IsInduced] [L.functor.IsEquivalence]
  [W₂'.RespectsIso] (iso : T.functor.comp R.functor ≅ L.functor.comp B.functor),
  T.arrow.HasLeftResolutions ↔ B.arrow.HasLeftResolutions

Defined in

Mathlib.CategoryTheory.Localization.Resolution

Cited by

0 results in Mathlib

Foundations

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

Assumes

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