CategoryTheory.Functor.rightDerived_map_eq
theorem CategoryTheory.Functor.rightDerived_map_eq :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1}
[inst_1 : CategoryTheory.Category.{u_2, u_1} D] [inst_2 : CategoryTheory.Abelian C]
[inst_3 : CategoryTheory.HasInjectiveResolutions C] [inst_4 : CategoryTheory.Abelian D]
(F : CategoryTheory.Functor C D) [inst_5 : F.Additive] (n : ℕ) {X Y : C} (f : X ⟶ Y)
{P : CategoryTheory.InjectiveResolution X} {Q : CategoryTheory.InjectiveResolution Y}
(g : P.cocomplex ⟶ Q.cocomplex),
CategoryTheory.CategoryStruct.comp P.ι g =
CategoryTheory.CategoryStruct.comp ((CochainComplex.single₀ C).map f) Q.ι →
(F.rightDerived n).map f =
CategoryTheory.CategoryStruct.comp (P.isoRightDerivedObj F n).hom
(CategoryTheory.CategoryStruct.comp
(((F.mapHomologicalComplex (ComplexShape.up ℕ)).comp
(HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n)).map
g)
(Q.isoRightDerivedObj F n).inv)
This theorem states that for any categories `C` and `D` where `C` is abelian and has injective resolutions, `D` is abelian, and a functor `F` from `C` to `D` which is additive, given natural number `n` and morphism `f` from objects `X` to `Y` in `C`, and injective resolutions `P` of `X` and `Q` of `Y`, with a morphism `g` from the cocomplex of `P` to the cocomplex of `Q`, if the composition of `P.ι` and `g` is equal to the composition of the mapping of `f` under the functor creating a cochain complex supported in degree zero and `Q.ι`, then the mapping of `f` under the `n`-th right derived functor of `F` is equal to the composition of the homomorphism from the `n`-th right derived object of `P` under `F` and the composition of the mapping of `g` under the functor composed of the functor mapping homological complexes with the cohomology shape to the `n`-th homology functor and the inverse homomorphism from the `n`-th right derived object of `Q` under `F`.
More concisely: Given additive functors F from an abelian category C with injective resolutions to an abelian category D, if for any objects X, Y in C, morphism f: X -> Y, and injective resolutions P of X and Q of Y with morphism g between their cocomplexes such that (P.ι circular arrow g) = (F(P.ι) circular arrow F(f) circular arrow Q.ι), then F(f) = (F(P^(n)[0]) circular arrow F(g)^(n) circular arrow F(Q^(n)[0])^(-1)) for the n-th right derived functor.
|
CategoryTheory.Functor.isZero_rightDerived_obj_injective_succ
theorem CategoryTheory.Functor.isZero_rightDerived_obj_injective_succ :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1}
[inst_1 : CategoryTheory.Category.{u_2, u_1} D] [inst_2 : CategoryTheory.Abelian C]
[inst_3 : CategoryTheory.HasInjectiveResolutions C] [inst_4 : CategoryTheory.Abelian D]
(F : CategoryTheory.Functor C D) [inst_5 : F.Additive] (n : ℕ) (X : C) [inst_6 : CategoryTheory.Injective X],
CategoryTheory.Limits.IsZero ((F.rightDerived (n + 1)).obj X)
This theorem states that, given categories `C` and `D` where `C` is Abelian and has injective resolutions, and `D` is also Abelian, if we have a functor `F` from `C` to `D` that is additive, then for any injective object `X` in `C` and any natural number `n`, the higher derived functors, specifically the `(n + 1)`-th right derived functor of `F` applied to `X`, is zero. This essentially means that the higher derived functors have no effect on injective objects.
More concisely: Given an additive functor F from an Abelian category C with injective objects to an Abelian category D, the (n+1)-th right derived functor of F applied to any injective object in C is zero.
|
CategoryTheory.InjectiveResolution.rightDerived_app_eq
theorem CategoryTheory.InjectiveResolution.rightDerived_app_eq :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1}
[inst_1 : CategoryTheory.Category.{u_2, u_1} D] [inst_2 : CategoryTheory.Abelian C]
[inst_3 : CategoryTheory.HasInjectiveResolutions C] [inst_4 : CategoryTheory.Abelian D]
{F G : CategoryTheory.Functor C D} [inst_5 : F.Additive] [inst_6 : G.Additive] (α : F ⟶ G) {X : C}
(P : CategoryTheory.InjectiveResolution X) (n : ℕ),
(CategoryTheory.NatTrans.rightDerived α n).app X =
CategoryTheory.CategoryStruct.comp (P.isoRightDerivedObj F n).hom
(CategoryTheory.CategoryStruct.comp
((HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).map
((CategoryTheory.NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex))
(P.isoRightDerivedObj G n).inv)
This theorem states that for any categories `C` and `D`, given Abelian structures on them and injective resolutions in `C`, along with two functors `F` and `G` from `C` to `D`, and a natural transformation `α` from `F` to `G`, we can compute a component of the natural transformation between the right-derived functors using a chosen injective resolution. Specifically, for any object `X` in `C` and its injective resolution `P`, this component (for a given natural number `n`) is equal to the composition of the homomorphism from the `n`-th right-derived object of `F` (associated with `P`) to `X`, and the map induced on the `n`-th homology group by the natural transformation `α` (acting on the homological complex associated with `P`), and the inverse of the homomorphism from the `n`-th right-derived object of `G` (associated with `P`) to `X`.
More concisely: Given Abelian categories `C` and `D`, functors `F` and `G` with a natural transformation `α` between them, injective resolutions `P` in `C`, and objects `X` in `C`, the `n`-th component of the natural transformation between their right-derived functors `R^n F` and `R^n G` is equal to the composition of the homomorphism from `R^n F(P)` to `X`, the map induced by `α` on the `n`-th homology group, and the inverse of the homomorphism from `R^n G(P)` to `X`.
|