Theorems · Theorem · category theory

CategoryTheory.LocalizerMorphism.hasRightResolutions_arrow_of_functorial_resolutions

∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
  {ρ : CategoryTheory.Functor C₂ C₁} (i : CategoryTheory.Functor.id C₂ ⟶ ρ.comp Φ.functor),
  (∀ (X₂ : C₂), W₂ (i.app X₂)) → Φ.arrow.HasRightResolutions

Defined in

Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Category