structure
RightDerivedDelta.RightDerivedDeltaFunctorData
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[CategoryTheory.EnoughInjectives C]
{D : Type u_1}
[CategoryTheory.Category.{u_2, u_1} D]
[CategoryTheory.Abelian D]
(F : CategoryTheory.Functor C D)
[F.Additive]
:
Type (max (max (max u u_1) u_2) v)
Data exhibiting a cohomological δ-functor as the right derived δ-functor
of an additive functor F : C ⥤ D: the underlying δ-functor δF, an
identification (δF)^n = F.rightDerived n in each degree, and effaceability.
- deltaFunctor : DerivedFunctorsDefs.CohomDeltaFunctor C D
- effaceable : self.deltaFunctor.IsEffaceable
Instances For
theorem
RightDerivedDelta.effaceable_of_degree_eq
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[CategoryTheory.EnoughInjectives C]
{D : Type u_1}
[CategoryTheory.Category.{u_2, u_1} D]
[CategoryTheory.Abelian D]
(F : CategoryTheory.Functor C D)
[F.Additive]
(δF : DerivedFunctorsDefs.CohomDeltaFunctor C D)
(h : ∀ (n : ℕ), δF.T n = F.rightDerived n)
:
δF.IsEffaceable
If a δ-functor agrees with the right derived functors in every degree then it is effaceable, since the right derived functors are.
def
RightDerivedDelta.nonSelfCechToDerivedData
{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₁ F₂ : DerivedFunctorsDefs.CohomDeltaFunctor C D)
(hF₁ : F₁.IsEffaceable)
:
Comparison data between an effaceable Čech-type δ-functor F₁ and an
arbitrary δ-functor F₂, packaged as a CechToDerivedData instance for
the universal property.