Theorems · Theorem · category theory

CategoryTheory.LocalizerMorphism.isLeftDerivabilityStructure_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 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] [W₂'.RespectsIso] [L.IsInduced]
  [L.functor.IsEquivalence] [R.IsInduced] [R.functor.IsEquivalence] [T.IsLeftDerivabilityStructure]
  (iso : T.functor.comp R.functor ≅ L.functor.comp B.functor), 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.MorphismProperty.RespectsIsoCategoryTheory.LocalizerMorphism.IsInducedCategoryTheory.Functor.IsEquivalenceCategoryTheory.LocalizerMorphism.IsInducedCategoryTheory.Functor.IsEquivalenceCategoryTheory.LocalizerMorphism.IsLeftDerivabilityStructure