The bounded-above projective derived locus

For any abelian category, this file cuts out the derived locus represented by bounded-above complexes of projective objects. Additive functors preserving projectives act functorially on this locus. Extension of scalars for module categories is a downstream affine instance.

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

Homotopy-category objects whose displayed complex is bounded above and degreewise projective.

Equations

• CategoryTheory.boundedAboveProjectiveHomotopy C K = ∃ (d : ℤ), CochainComplex.IsStrictlyLE K.as d ∧ ∀ (n : ℤ), CategoryTheory.Projective (K.as.X n)

@[reducible, inline]

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

The full homotopy category of displayed bounded-above complexes of projective objects.

Equations

• CategoryTheory.BoundedAboveProjectiveHomotopyCategory C = (CategoryTheory.boundedAboveProjectiveHomotopy C).FullSubcategory

theorem CategoryTheory.boundedAboveProjectiveHomotopy_le_kProjective (C : Type u) [Category.{v, u} C] [Abelian C] : boundedAboveProjectiveHomotopy C ≤ kProjectiveHomotopy C

A bounded-above degreewise-projective complex is K-projective.

def CategoryTheory.boundedAboveProjectiveToKProjective (C : Type u) [Category.{v, u} C] [Abelian C] : Functor (BoundedAboveProjectiveHomotopyCategory C) (KProjectiveHomotopyCategory C)

Inclusion of bounded-above projective representatives into all K-projective representatives.

Equations

• CategoryTheory.boundedAboveProjectiveToKProjective C = CategoryTheory.ObjectProperty.ιOfLE ⋯

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

Localization of bounded-above projective representatives.

Equations

• CategoryTheory.boundedAboveProjectiveQh C = (CategoryTheory.boundedAboveProjectiveHomotopy C).ι.comp DerivedCategory.Qh

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

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

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

@[reducible, inline]

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

The full derived locus represented by bounded-above complexes of projective objects.

Equations

• CategoryTheory.BoundedAboveProjectiveDerivedCategory C = (CategoryTheory.boundedAboveProjectiveQh C).EssImageSubcategory

noncomputable def CategoryTheory.boundedAboveProjectiveQhEquivalence (C : Type u) [Category.{v, u} C] [Abelian C] : BoundedAboveProjectiveHomotopyCategory C ≌ BoundedAboveProjectiveDerivedCategory C

Bounded-above projective representatives modulo homotopy are equivalent to their essential image in the derived category.

Equations

• CategoryTheory.boundedAboveProjectiveQhEquivalence C = (CategoryTheory.boundedAboveProjectiveQh C).toEssImage.asEquivalence

def CategoryTheory.mapBoundedAboveProjectiveHomotopy {C : Type u} {D : Type u'} [Category.{v, u} C] [Abelian C] [Category.{v', u'} D] [Abelian D] (F : Functor C D) [F.Additive] [F.PreservesProjectiveObjects] : Functor (BoundedAboveProjectiveHomotopyCategory C) (BoundedAboveProjectiveHomotopyCategory D)

An additive functor preserving projective objects acts on bounded-above projective representatives.

Equations

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

def CategoryTheory.mapBoundedAboveProjectiveHomotopyCompIso {C : Type u} {D : Type u'} {E : Type u_1} [Category.{v, u} C] [Abelian C] [Category.{v', u'} D] [Abelian D] [Category.{u_2, u_1} E] [Abelian E] (F : Functor C D) (G : Functor D E) (H : Functor C E) [F.Additive] [G.Additive] [H.Additive] [F.PreservesProjectiveObjects] [G.PreservesProjectiveObjects] [H.PreservesProjectiveObjects] (e : F.comp G ≅ H) : (mapBoundedAboveProjectiveHomotopy F).comp (mapBoundedAboveProjectiveHomotopy G) ≅ mapBoundedAboveProjectiveHomotopy H

Composition of functors preserving projectives agrees on the bounded-above projective homotopy loci.

Equations

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

noncomputable def CategoryTheory.boundedAboveProjectiveDerivedFunctor {C : Type u} {D : Type u'} [Category.{v, u} C] [Abelian C] [Category.{v', u'} D] [Abelian D] (F : Functor C D) [F.Additive] [F.PreservesProjectiveObjects] : Functor (BoundedAboveProjectiveDerivedCategory C) (BoundedAboveProjectiveDerivedCategory D)

The supported derived functor lands back in the bounded-above projective derived locus.

Equations

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

noncomputable def CategoryTheory.boundedAboveProjectiveDerivedFunctorCompIso {C : Type u} {D : Type u'} {E : Type u_1} [Category.{v, u} C] [Abelian C] [Category.{v', u'} D] [Abelian D] [Category.{u_2, u_1} E] [Abelian E] (F : Functor C D) (G : Functor D E) (H : Functor C E) [F.Additive] [G.Additive] [H.Additive] [F.PreservesProjectiveObjects] [G.PreservesProjectiveObjects] [H.PreservesProjectiveObjects] (e : F.comp G ≅ H) : (boundedAboveProjectiveDerivedFunctor F).comp (boundedAboveProjectiveDerivedFunctor G) ≅ boundedAboveProjectiveDerivedFunctor H

Composition of supported derived functors agrees with the supported derived functor of the composite.

Equations

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