def Hypercohomology.applyDegreewise (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (D : Type u_1) [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] : CategoryTheory.Functor (CochainComplex C ℤ) (CochainComplex D ℤ)

Apply an additive functor F : C ⥤ D degreewise to a cochain complex, producing the induced functor on cochain complexes.

noncomputable def Hypercohomology.naiveHypercohomologyFunctor (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (D : Type u_1) [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] (n : ℤ) : CategoryTheory.Functor (CochainComplex C ℤ) D

Naive hypercohomology functor: apply F degreewise and then take homology in degree n. Agrees with true hypercohomology only when F is exact or the input is F-acyclic.

noncomputable def Hypercohomology.toDerivedOfD (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (D : Type u_1) [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian D] [HasDerivedCategory D] (F : CategoryTheory.Functor C D) [F.Additive] : CategoryTheory.Functor (CochainComplex C ℤ) (DerivedCategory D)

The composite functor sending a cochain complex K in C to the image of F(K) in the derived category of D. Its right derived functor is the source of hypercohomology.

theorem Hypercohomology.totalDerivedExists (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] [CategoryTheory.EnoughInjectives C] (D : Type u_1) [CategoryTheory.Category.{u_3, u_1} D] [CategoryTheory.Abelian D] [HasDerivedCategory D] (F : CategoryTheory.Functor C D) [F.Additive] : (toDerivedOfD C D F).HasRightDerivedFunctor (HomologicalComplex.quasiIso C (ComplexShape.up ℤ))

Existence of the total right derived functor of F along quasi-isomorphisms.

noncomputable def Hypercohomology.totalDerivedFunctor (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] [CategoryTheory.EnoughInjectives C] (D : Type u_1) [CategoryTheory.Category.{u_3, u_1} D] [CategoryTheory.Abelian D] [HasDerivedCategory D] (F : CategoryTheory.Functor C D) [F.Additive] : CategoryTheory.Functor (DerivedCategory C) (DerivedCategory D)

The total right derived functor RF : D(C) ⥤ D(D) of an additive functor F.

noncomputable def Hypercohomology.hypercohomologyFunctor (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] [CategoryTheory.EnoughInjectives C] (D : Type u_1) [CategoryTheory.Category.{u_3, u_1} D] [CategoryTheory.Abelian D] [HasDerivedCategory D] (F : CategoryTheory.Functor C D) [F.Additive] (n : ℤ) : CategoryTheory.Functor (CochainComplex C ℤ) D

The n-th hypercohomology functor ℝ^n F sending a complex K to the n-th cohomology of RF(K).

noncomputable def Hypercohomology.hypercohomology (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] [CategoryTheory.EnoughInjectives C] (D : Type u_1) [CategoryTheory.Category.{u_3, u_1} D] [CategoryTheory.Abelian D] [HasDerivedCategory D] (F : CategoryTheory.Functor C D) [F.Additive] (n : ℤ) (K : CochainComplex C ℤ) : D

The n-th hypercohomology object ℝ^n F (K) of a complex K.

noncomputable def Hypercohomology.hypercohomology_single_iso (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] [CategoryTheory.EnoughInjectives C] (D : Type u_1) [CategoryTheory.Category.{u_3, u_1} D] [CategoryTheory.Abelian D] [HasDerivedCategory D] (F : CategoryTheory.Functor C D) [F.Additive] (X : C) (n : ℕ) : hypercohomology C D F (↑n) ((HomologicalComplex.single C (ComplexShape.up ℤ) 0).obj X) ≅ (F.rightDerived n).obj X

Hypercohomology of an object placed in a single degree agrees with the usual right derived functor R^n F (X).

noncomputable def Hypercohomology.spectralSequence_E2_map (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] [CategoryTheory.EnoughInjectives C] (D : Type u_1) [CategoryTheory.Category.{u_3, u_1} D] [CategoryTheory.Abelian D] [HasDerivedCategory D] (F : CategoryTheory.Functor C D) [F.Additive] (K : CochainComplex C ℤ) (p : ℕ) (q : ℤ) : (F.rightDerived p).obj ((HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) q).obj K) ⟶ hypercohomology C D F (↑p + q) K

The E_2-edge map of the hypercohomology spectral sequence R^p F (H^q K) ⟹ ℝ^{p+q} F (K).

theorem Hypercohomology.spectralSequence_E2_natural (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] [CategoryTheory.EnoughInjectives C] (D : Type u_1) [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian D] [HasDerivedCategory D] (F : CategoryTheory.Functor C D) [F.Additive] {K L : CochainComplex C ℤ} (f : K ⟶ L) (p : ℕ) (q : ℤ) : CategoryTheory.CategoryStruct.comp ((F.rightDerived p).map ((HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) q).map f)) (spectralSequence_E2_map C D F L p q) = CategoryTheory.CategoryStruct.comp (spectralSequence_E2_map C D F K p q) ((hypercohomologyFunctor C D F (↑p + q)).map f)

Naturality of the E_2-edge map of the hypercohomology spectral sequence.

noncomputable def Hypercohomology.acyclic_degeneration (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] [CategoryTheory.EnoughInjectives C] (D : Type u_1) [CategoryTheory.Category.{u_3, u_1} D] [CategoryTheory.Abelian D] [HasDerivedCategory D] (F : CategoryTheory.Functor C D) [F.Additive] (K : CochainComplex C ℤ) (hacyclic : ∀ (i : ℤ) (p : ℕ), 0 < p → CategoryTheory.Limits.IsZero ((F.rightDerived p).obj (K.X i))) (n : ℤ) : hypercohomology C D F n K ≅ (naiveHypercohomologyFunctor C D F n).obj K

Spectral sequence degeneration: if every term K.X i is F-acyclic, then hypercohomology coincides with the naive degreewise version.