Isomorphisms and units on the bounded-above projective locus

Natural isomorphisms between additive functors preserving projectives induce isomorphisms of their supported derived functors. In particular, the identity functor acts as the identity on the bounded-above projective locus.

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

A natural isomorphism between additive functors preserving projectives induces one on their bounded-above projective homotopy loci.

Equations

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

def CategoryTheory.mapBoundedAboveProjectiveHomotopyIdIso (C : Type u) [Category.{v, u} C] [Abelian C] : mapBoundedAboveProjectiveHomotopy (Functor.id C) ≅ Functor.id (BoundedAboveProjectiveHomotopyCategory C)

Mapping homotopy complexes by the identity functor is the identity on the bounded-above projective homotopy locus.

Equations

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

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

Naturally isomorphic additive functors induce naturally isomorphic supported derived functors.

Equations

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

noncomputable def CategoryTheory.boundedAboveProjectiveDerivedFunctorIdIso (C : Type u) [Category.{v, u} C] [Abelian C] : boundedAboveProjectiveDerivedFunctor (Functor.id C) ≅ Functor.id (BoundedAboveProjectiveDerivedCategory C)

The supported derived functor of the identity is naturally isomorphic to the identity functor on the supported derived locus.

Equations

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