Theorems · Theorem · category theory

CategoryTheory.LocalizerMorphism.isLeftDerivabilityStructure_iff_of_isLocalizedEquivalence

∀ {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 D₁} {W₂ : CategoryTheory.MorphismProperty C₂}
  {W₂' : CategoryTheory.MorphismProperty D₂} {T : CategoryTheory.LocalizerMorphism W₁ W₂}
  {L : CategoryTheory.LocalizerMorphism W₁ W₁'} {R : CategoryTheory.LocalizerMorphism W₂ W₂'}
  {B : CategoryTheory.LocalizerMorphism W₁' W₂'} [W₂'.RespectsIso] [L.IsLocalizedEquivalence] [R.IsLocalizedEquivalence]
  [R.functor.EssSurj] [L.functor.EssSurj] [R.functor.Full] [R.IsInduced]
  (iso : T.functor.comp R.functor ≅ L.functor.comp B.functor) [CategoryTheory.TwoSquare.GuitartExact iso.inv],
  T.IsLeftDerivabilityStructure ↔ B.IsLeftDerivabilityStructure

Defined in

Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.MorphismProperty.RespectsIsoCategoryTheory.LocalizerMorphism.IsLocalizedEquivalenceCategoryTheory.LocalizerMorphism.IsLocalizedEquivalenceCategoryTheory.Functor.EssSurjCategoryTheory.Functor.EssSurjCategoryTheory.Functor.FullCategoryTheory.LocalizerMorphism.IsInducedCategoryTheory.TwoSquare.GuitartExact