Theorems · Definition · category theory

CategoryTheory.LocalizerMorphism.Derives

{C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {H : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} H] →
            {W₁ : CategoryTheory.MorphismProperty C₁} →
              {W₂ : CategoryTheory.MorphismProperty C₂} →
                CategoryTheory.LocalizerMorphism W₁ W₂ → CategoryTheory.Functor C₂ H → Prop

Given a localizer morphism Φ : LocalizerMorphism W₁ W₂ between morphism properties on C₁ and C₂, and a functor C₂ ⥤ H, this is the property that W₁ is inverted by Φ.functor ⋙ F. In case Φ is a (left/right) derivability structure, this allows the construction of a derived functor for F relatively to W₂.

Defined in

Mathlib.CategoryTheory.Localization.DerivabilityStructure.Derives

Cited by

6 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Category