Derived functors on K-projective complexes

The K-projective homotopy category of any abelian category embeds fully faithfully in its derived category. An arbitrary additive functor can then be derived on this locus without exactness assumptions. Ring extension of scalars is one downstream consumer, not part of the construction itself.

def CategoryTheory.kProjectiveHomotopy (C : Type u) [Category.{v, u} C] [Abelian C] : ObjectProperty (HomotopyCategory C (ComplexShape.up ℤ))

K-projective objects in the homotopy category of cochain complexes.

Equations

• CategoryTheory.kProjectiveHomotopy C K = CochainComplex.IsKProjective K.as

@[reducible, inline]

abbrev CategoryTheory.KProjectiveHomotopyCategory (C : Type u) [Category.{v, u} C] [Abelian C] : Type (max u v)

The full homotopy category of K-projective cochain complexes.

Equations

• CategoryTheory.KProjectiveHomotopyCategory C = (CategoryTheory.kProjectiveHomotopy C).FullSubcategory

instance CategoryTheory.kProjectiveHomotopyCategory_isKProjective (C : Type u) [Category.{v, u} C] [Abelian C] (K : KProjectiveHomotopyCategory C) : CochainComplex.IsKProjective K.obj.as

The underlying complex of an object of the K-projective homotopy category is K-projective.

noncomputable def CategoryTheory.kProjectiveQh (C : Type u) [Category.{v, u} C] [Abelian C] : Functor (KProjectiveHomotopyCategory C) (DerivedCategory C)

Inclusion of the K-projective homotopy category into the derived category.

Equations

• CategoryTheory.kProjectiveQh C = (CategoryTheory.kProjectiveHomotopy C).ι.comp DerivedCategory.Qh

instance CategoryTheory.kProjectiveQh_full (C : Type u) [Category.{v, u} C] [Abelian C] : (kProjectiveQh C).Full

Localization is full on morphisms whose source is K-projective.

instance CategoryTheory.kProjectiveQh_faithful (C : Type u) [Category.{v, u} C] [Abelian C] : (kProjectiveQh C).Faithful

Localization is faithful on morphisms whose source is K-projective.

@[reducible, inline]

abbrev CategoryTheory.KProjectiveDerivedCategory (C : Type u) [Category.{v, u} C] [Abelian C] : Type (max u v)

The full derived subcategory consisting of objects represented by K-projective complexes.

Equations

• CategoryTheory.KProjectiveDerivedCategory C = (CategoryTheory.kProjectiveQh C).EssImageSubcategory

noncomputable def CategoryTheory.kProjectiveQhEquivalence (C : Type u) [Category.{v, u} C] [Abelian C] : KProjectiveHomotopyCategory C ≌ KProjectiveDerivedCategory C

K-projective complexes modulo homotopy are equivalent to their essential image in the derived category.

Equations

• CategoryTheory.kProjectiveQhEquivalence C = (CategoryTheory.kProjectiveQh C).toEssImage.asEquivalence

def CategoryTheory.KProjectiveHomotopyCategory.ofBoundedAboveProjectives {C : Type u} [Category.{v, u} C] [Abelian C] (K : CochainComplex C ℤ) (d : ℤ) [K.IsStrictlyLE d] [∀ (n : ℤ), Projective (K.X n)] : KProjectiveHomotopyCategory C

A bounded-above complex of projective objects, regarded as an object of the K-projective homotopy category.

Equations

• CategoryTheory.KProjectiveHomotopyCategory.ofBoundedAboveProjectives K d = { obj := (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K, property := ⋯ }

noncomputable def CategoryTheory.kProjectiveDerivedFunctor {C : Type u} {D : Type u'} [Category.{v, u} C] [Abelian C] [Category.{v', u'} D] [Abelian D] (F : Functor C D) [F.Additive] : Functor (KProjectiveHomotopyCategory C) (DerivedCategory D)

Apply an additive functor to K-projective representatives in the homotopy category, then localize the resulting complexes. This construction does not require the additive functor to be exact.

Equations

• CategoryTheory.kProjectiveDerivedFunctor F = (CategoryTheory.kProjectiveHomotopy C).ι.comp ((F.mapHomotopyCategory (ComplexShape.up ℤ)).comp DerivedCategory.Qh)

noncomputable def CategoryTheory.kProjectiveLocusDerivedFunctor {C : Type u} {D : Type u'} [Category.{v, u} C] [Abelian C] [Category.{v', u'} D] [Abelian D] (F : Functor C D) [F.Additive] : Functor (KProjectiveDerivedCategory C) (DerivedCategory D)

The supported derived functor, now expressed on an honest full subcategory of the source derived category rather than on chosen representatives.

Equations

• CategoryTheory.kProjectiveLocusDerivedFunctor F = (CategoryTheory.kProjectiveQhEquivalence C).inverse.comp (CategoryTheory.kProjectiveDerivedFunctor F)

noncomputable def CategoryTheory.kProjectiveLocusDerivedComparison {C : Type u} {D : Type u'} [Category.{v, u} C] [Abelian C] [Category.{v', u'} D] [Abelian D] (F : Functor C D) [F.Additive] : (kProjectiveQhEquivalence C).functor.comp (kProjectiveLocusDerivedFunctor F) ≅ kProjectiveDerivedFunctor F

Pulling an actual K-projective representative into the derived locus and then applying the locus functor recovers the representative-level construction.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.kProjectiveDerivedFunctorObjIso {C : Type u} {D : Type u'} [Category.{v, u} C] [Abelian C] [Category.{v', u'} D] [Abelian D] (F : Functor C D) [F.Additive] (K : CochainComplex C ℤ) (d : ℤ) [K.IsStrictlyLE d] [∀ (n : ℤ), Projective (K.X n)] : (kProjectiveDerivedFunctor F).obj (KProjectiveHomotopyCategory.ofBoundedAboveProjectives K d) ≅ DerivedCategory.Q.obj ((F.mapHomologicalComplex (ComplexShape.up ℤ)).obj K)

On a concrete bounded-above projective complex, the supported derived functor is represented by applying the original functor degreewise.

Equations

• One or more equations did not get rendered due to their size.

theorem CochainComplex.IsKProjective.homotopyEquivalences_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] {K L : CochainComplex C ℤ} [K.IsKProjective] [L.IsKProjective] {g : K ⟶ L} (hg : HomologicalComplex.quasiIso C (ComplexShape.up ℤ) g) : HomologicalComplex.homotopyEquivalences D (ComplexShape.up ℤ) ((F.mapHomologicalComplex (ComplexShape.up ℤ)).map g)

An additive functor carries a quasi-isomorphism between K-projective cochain complexes to a homotopy equivalence.

This is the mechanism behind every unconditional preservation statement for K-projective representatives: a quasi-isomorphism between K-projective complexes is already an isomorphism in the homotopy category, and every additive functor preserves homotopies. No exactness, flatness or limit-preservation hypothesis on F is used, and none is available.

theorem CochainComplex.IsKProjective.quasiIso_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] {K L : CochainComplex C ℤ} [K.IsKProjective] [L.IsKProjective] {g : K ⟶ L} (hg : HomologicalComplex.quasiIso C (ComplexShape.up ℤ) g) : HomologicalComplex.quasiIso D (ComplexShape.up ℤ) ((F.mapHomologicalComplex (ComplexShape.up ℤ)).map g)

An additive functor carries a quasi-isomorphism between K-projective cochain complexes to a quasi-isomorphism.

theorem CochainComplex.IsKProjective.quasiIso_map_of_projective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] {K L : CochainComplex C ℤ} (dK dL : ℤ) [K.IsStrictlyLE dK] [L.IsStrictlyLE dL] [∀ (n : ℤ), CategoryTheory.Projective (K.X n)] [∀ (n : ℤ), CategoryTheory.Projective (L.X n)] {g : K ⟶ L} (hg : HomologicalComplex.quasiIso C (ComplexShape.up ℤ) g) : HomologicalComplex.quasiIso D (ComplexShape.up ℤ) ((F.mapHomologicalComplex (ComplexShape.up ℤ)).map g)

The bounded-above degreewise-projective case of quasiIso_map.

This is the form in which the hypothesis is actually inhabited: every bounded-above complex of projective objects is K-projective, and in a module category such complexes are abundant. It records that an additive functor needs no exactness to be correct on bounded-above projective representatives.