Degree-zero homology of the bounded-below right-derived functor

For an additive functor between abelian categories with enough injectives, Mathlib constructs a bounded-below right-derived functor and its universal unit. An injective resolution shows that the unit induces an isomorphism on H⁰ of a strictly nonnegative complex when the functor preserves the input's outgoing degree-zero kernel and those of nonnegative injective resolutions equipped with a quasi-isomorphism from that input. The degree-zero single case needs only its resolution-kernel condition.

The derived unit also gives a natural H⁰ comparison on degree-zero singles. Its components agree with the pointwise comparisons below, as proved by the two component-agreement theorems. Geometric identifications are separate.

Main definitions

• CategoryTheory.Functor.rightDerivedFunctorPlusHomologyZeroSingleIso: the pointwise comparison with the underived functor.
• CategoryTheory.Functor.rightDerivedFunctorPlusHomologyZeroSingleIsoOfPreservesFiniteLimits: a finite-limit-preserving specialization.
• CategoryTheory.Functor.rightDerivedFunctorPlusHomologyZeroSingleNatIso: a natural comparison under uniform resolution-kernel preservation.
• CategoryTheory.Functor.rightDerivedFunctorPlusHomologyZeroSingleNatIsoOfPreservesFiniteLimits: its finite-limit-preserving specialization.

Main results

• CategoryTheory.Functor.isIso_homologyZero_map_rightDerivedFunctorPlusUnit_of_isStrictlyGE_zero: the H⁰ unit is invertible on a nonnegative complex under local kernels.
• CategoryTheory.Functor.isIso_homologyZero_map_rightDerivedFunctorPlusUnit_single: the degree-zero single specialization.
• CategoryTheory.Functor.rightDerivedFunctorPlusHomologyZeroSingleNatIso_app: agreement with the pointwise comparison; the finite-limit specialization has the analogous result.

Implementation notes

The resolution is strictly nonnegative and termwise injective. Zero incoming differentials reduce H⁰ preservation to outgoing-kernel preservation. Unit naturality transfers invertibility from the injective resolution.

References

• Mathlib Algebra/Homology/DerivedCategory/RightDerivedFunctorPlus.lean and DerivabilityStructureInjectives.lean at pin 520045ab14e26149ee970e2e617ca04b09bde5d6.

Tags

right-derived functor, bounded-below derived category, degree-zero homology

theorem CategoryTheory.Functor.isIso_homologyZero_map_rightDerivedFunctorPlusUnit_of_isStrictlyGE_zero {C : Type u} {D : Type v} [Category.{u_1, u} C] [Category.{u_2, v} D] [Abelian C] [Abelian D] [HasDerivedCategory C] [HasDerivedCategory D] (F : Functor C D) [F.Additive] [EnoughInjectives C] (K : CochainComplex.Plus C) [K.obj.IsStrictlyGE 0] (hK : Limits.PreservesLimit (Limits.parallelPair (HomologicalComplex.sc K.obj 0).g 0) F) (hResKernel : ∀ (L : CochainComplex.Plus (InjectiveObject C)) [L.obj.IsStrictlyGE 0] (i : K ⟶ (InjectiveObject.ι C).mapCochainComplexPlus.obj L), CochainComplex.Plus.quasiIso C i → Limits.PreservesLimit (Limits.parallelPair (HomologicalComplex.sc ((InjectiveObject.ι C).mapCochainComplexPlus.obj L).obj 0).g 0) F) : IsIso ((DerivedCategory.Plus.homologyFunctor D 0).map (F.rightDerivedFunctorPlusUnit.app ((HomotopyCategory.Plus.quotient C).obj K)))

Resolve the input by a strictly nonnegative complex of injectives. Preservation of the input's outgoing kernel and the kernels in its chosen resolution makes the mapped resolution an H⁰ isomorphism; unit naturality then transfers invertibility to the input.

theorem CategoryTheory.Functor.isIso_homologyZero_map_rightDerivedFunctorPlusUnit_single {C : Type u} {D : Type v} [Category.{u_1, u} C] [Category.{u_2, v} D] [Abelian C] [Abelian D] [HasDerivedCategory C] [HasDerivedCategory D] (F : Functor C D) [F.Additive] [EnoughInjectives C] (X : C) (hResKernel : ∀ (L : CochainComplex.Plus (InjectiveObject C)) [L.obj.IsStrictlyGE 0] (i : { obj := (CochainComplex.singleFunctor C 0).obj X, property := ⋯ } ⟶ (InjectiveObject.ι C).mapCochainComplexPlus.obj L), CochainComplex.Plus.quasiIso C i → Limits.PreservesLimit (Limits.parallelPair (HomologicalComplex.sc ((InjectiveObject.ι C).mapCochainComplexPlus.obj L).obj 0).g 0) F) : IsIso ((DerivedCategory.Plus.homologyFunctor D 0).map (F.rightDerivedFunctorPlusUnit.app ((HomotopyCategory.Plus.singleFunctor C 0).obj X)))

For a degree-zero single, the source outgoing differential is zero and its kernel is automatically preserved. Only kernels in resolutions receiving a quasi-isomorphism from this single remain as premises.

noncomputable def CategoryTheory.Functor.rightDerivedFunctorPlusHomologyZeroSingleIso {C : Type u} {D : Type v} [Category.{u_1, u} C] [Category.{u_2, v} D] [Abelian C] [Abelian D] [HasDerivedCategory C] [HasDerivedCategory D] (F : Functor C D) [F.Additive] [EnoughInjectives C] (X : C) (hResKernel : ∀ (L : CochainComplex.Plus (InjectiveObject C)) [L.obj.IsStrictlyGE 0] (i : { obj := (CochainComplex.singleFunctor C 0).obj X, property := ⋯ } ⟶ (InjectiveObject.ι C).mapCochainComplexPlus.obj L), CochainComplex.Plus.quasiIso C i → Limits.PreservesLimit (Limits.parallelPair (HomologicalComplex.sc ((InjectiveObject.ι C).mapCochainComplexPlus.obj L).obj 0).g 0) F) : (DerivedCategory.Plus.homologyFunctor D 0).obj (F.rightDerivedFunctorPlus.obj ((DerivedCategory.Plus.singleFunctor C 0).obj X)) ≅ F.obj X

Invert H⁰ of the derived unit on this single, then compose with the canonical source comparison to F.obj X. This packages a pointwise isomorphism; naturality in X remains separate.

Equations

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

noncomputable def CategoryTheory.Functor.rightDerivedFunctorPlusHomologyZeroSingleIsoOfPreservesFiniteLimits {C : Type u} {D : Type v} [Category.{u_1, u} C] [Category.{u_2, v} D] [Abelian C] [Abelian D] [HasDerivedCategory C] [HasDerivedCategory D] (F : Functor C D) [F.Additive] [EnoughInjectives C] (X : C) [Limits.PreservesFiniteLimits F] : (DerivedCategory.Plus.homologyFunctor D 0).obj (F.rightDerivedFunctorPlus.obj ((DerivedCategory.Plus.singleFunctor C 0).obj X)) ≅ F.obj X

Finite-limit preservation supplies every outgoing kernel condition required by the pointwise single-object comparison.

Equations

• F.rightDerivedFunctorPlusHomologyZeroSingleIsoOfPreservesFiniteLimits X = F.rightDerivedFunctorPlusHomologyZeroSingleIso X ⋯

noncomputable def CategoryTheory.Functor.rightDerivedFunctorPlusHomologyZeroSingleNatIso {C : Type u} {D : Type v} [Category.{u_1, u} C] [Category.{u_2, v} D] [Abelian C] [Abelian D] [HasDerivedCategory C] [HasDerivedCategory D] (F : Functor C D) [F.Additive] [EnoughInjectives C] (hResKernel : ∀ (X : C) (L : CochainComplex.Plus (InjectiveObject C)) [L.obj.IsStrictlyGE 0] (i : { obj := (CochainComplex.singleFunctor C 0).obj X, property := ⋯ } ⟶ (InjectiveObject.ι C).mapCochainComplexPlus.obj L), CochainComplex.Plus.quasiIso C i → Limits.PreservesLimit (Limits.parallelPair (HomologicalComplex.sc ((InjectiveObject.ι C).mapCochainComplexPlus.obj L).obj 0).g 0) F) : ((DerivedCategory.Plus.singleFunctor C 0).comp F.rightDerivedFunctorPlus).comp (DerivedCategory.Plus.homologyFunctor D 0) ≅ F

A uniform family of outgoing-kernel conditions on injective resolutions makes the H⁰ comparison of the bounded-below right-derived functor natural in the degree-zero input. No choice of resolutions needs to be natural: the right-derived unit already is.

Equations

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

theorem CategoryTheory.Functor.rightDerivedFunctorPlusHomologyZeroSingleNatIso_app {C : Type u} {D : Type v} [Category.{u_1, u} C] [Category.{u_2, v} D] [Abelian C] [Abelian D] [HasDerivedCategory C] [HasDerivedCategory D] (F : Functor C D) [F.Additive] [EnoughInjectives C] (hResKernel : ∀ (X : C) (L : CochainComplex.Plus (InjectiveObject C)) [L.obj.IsStrictlyGE 0] (i : { obj := (CochainComplex.singleFunctor C 0).obj X, property := ⋯ } ⟶ (InjectiveObject.ι C).mapCochainComplexPlus.obj L), CochainComplex.Plus.quasiIso C i → Limits.PreservesLimit (Limits.parallelPair (HomologicalComplex.sc ((InjectiveObject.ι C).mapCochainComplexPlus.obj L).obj 0).g 0) F) (X : C) : (F.rightDerivedFunctorPlusHomologyZeroSingleNatIso hResKernel).app X = F.rightDerivedFunctorPlusHomologyZeroSingleIso X ⋯

Both constructions invert the same component of the derived unit and use the same source normalization, without choosing compatible resolutions.

noncomputable def CategoryTheory.Functor.rightDerivedFunctorPlusHomologyZeroSingleNatIsoOfPreservesFiniteLimits {C : Type u} {D : Type v} [Category.{u_1, u} C] [Category.{u_2, v} D] [Abelian C] [Abelian D] [HasDerivedCategory C] [HasDerivedCategory D] (F : Functor C D) [F.Additive] [EnoughInjectives C] [Limits.PreservesFiniteLimits F] : ((DerivedCategory.Plus.singleFunctor C 0).comp F.rightDerivedFunctorPlus).comp (DerivedCategory.Plus.homologyFunctor D 0) ≅ F

Finite-limit preservation supplies the resolution-kernel conditions for the natural H⁰ comparison of degree-zero singles.

Equations

• F.rightDerivedFunctorPlusHomologyZeroSingleNatIsoOfPreservesFiniteLimits = F.rightDerivedFunctorPlusHomologyZeroSingleNatIso ⋯

theorem CategoryTheory.Functor.rightDerivedFunctorPlusHomologyZeroSingleNatIsoOfPreservesFiniteLimits_app {C : Type u} {D : Type v} [Category.{u_1, u} C] [Category.{u_2, v} D] [Abelian C] [Abelian D] [HasDerivedCategory C] [HasDerivedCategory D] (F : Functor C D) [F.Additive] [EnoughInjectives C] [Limits.PreservesFiniteLimits F] (X : C) : F.rightDerivedFunctorPlusHomologyZeroSingleNatIsoOfPreservesFiniteLimits.app X = F.rightDerivedFunctorPlusHomologyZeroSingleIsoOfPreservesFiniteLimits X

Specializing uniform-kernel agreement recovers the existing finite-limit pointwise comparison without unfolding either construction.

theorem CategoryTheory.Functor.rightDerivedFunctorPlus_additive {C : Type u} {D : Type v} [Category.{u_2, u} C] [Category.{u_4, v} D] [Abelian C] [Abelian D] [HasDerivedCategory C] [HasDerivedCategory D] (F : Functor C D) [F.Additive] [EnoughInjectives C] : F.rightDerivedFunctorPlus.Additive

The bounded-below right-derived functor of an additive functor is additive. The bounded injective homotopy model is full and essentially surjective in the derived category, and the right-derived unit is invertible on that model. No finite-limit preservation or nonnegative bound is required.