CategoryTheory.ProjectiveResolution.leftDerived_app_eq
theorem CategoryTheory.ProjectiveResolution.leftDerived_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.HasProjectiveResolutions 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.ProjectiveResolution X) (n : ℕ),
(CategoryTheory.NatTrans.leftDerived α n).app X =
CategoryTheory.CategoryStruct.comp (P.isoLeftDerivedObj F n).hom
(CategoryTheory.CategoryStruct.comp
((HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).map
((CategoryTheory.NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app P.complex))
(P.isoLeftDerivedObj G n).inv)
The theorem `CategoryTheory.ProjectiveResolution.leftDerived_app_eq` states that for any categories `C` and `D`, where `C` is an Abelian category with projective resolutions, `D` is also an Abelian category, and `F` and `G` are functors from `C` to `D` that carry additive structures, the component of the natural transformation `α` between the left-derived functors `F` and `G` at a point `X` in `C`, given a projective resolution `P` of `X` and an integer `n`, can be computed using the composition of the isomorphism from `P` to the nth left-derived object of `F`, the map induced by `α` on the nth homology group of the homological complex associated to `P`, and the inverse of the isomorphism from `P` to the nth left-derived object of `G`.
More concisely: For functors F and G between Abelian categories with projective resolutions, the component of the natural transformation between their left-derived functors at an object X is given by the composition of the isomorphism from X's projective resolution to its nth left-derived object, the map induced by the transformation on the nth homology group, and the inverse of the isomorphism to the nth left-derived object of G.
|
CategoryTheory.NatTrans.leftDerived_id
theorem CategoryTheory.NatTrans.leftDerived_id :
∀ {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.HasProjectiveResolutions C] [inst_4 : CategoryTheory.Abelian D]
(F : CategoryTheory.Functor C D) [inst_5 : F.Additive] (n : ℕ),
CategoryTheory.NatTrans.leftDerived (CategoryTheory.CategoryStruct.id F) n =
CategoryTheory.CategoryStruct.id (F.leftDerived n)
This theorem, `CategoryTheory.NatTrans.leftDerived_id`, states that for any category `C` with instances `inst`, `inst_2`, and `inst_3` (which indicate that `C` is a category, an Abelian category, and has projective resolutions), and another category `D` with instances `inst_1` and `inst_4` (which indicate that `D` is a category and an Abelian category), given a functor `F` from `C` to `D` that is additive (as indicated by `inst_5`), for any natural number `n`, the `n`th left derived natural transformation of the identity morphism on `F` is equal to the identity morphism on the `n`th left derived functor of `F`. In other words, the theorem is about the naturality of the process of taking left derived functors in the context of Abelian categories.
More concisely: For any additive functor F between Abelian categories C and D, the n-th left derived natural transformation of the identity morphism on F is equal to the identity morphism on the n-th left derived functor of F.
|
CategoryTheory.Functor.leftDerived_map_eq
theorem CategoryTheory.Functor.leftDerived_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.HasProjectiveResolutions C] [inst_4 : CategoryTheory.Abelian D]
(F : CategoryTheory.Functor C D) [inst_5 : F.Additive] (n : ℕ) {X Y : C} (f : X ⟶ Y)
{P : CategoryTheory.ProjectiveResolution X} {Q : CategoryTheory.ProjectiveResolution Y}
(g : P.complex ⟶ Q.complex),
CategoryTheory.CategoryStruct.comp g Q.π =
CategoryTheory.CategoryStruct.comp P.π ((ChainComplex.single₀ C).map f) →
(F.leftDerived n).map f =
CategoryTheory.CategoryStruct.comp (P.isoLeftDerivedObj F n).hom
(CategoryTheory.CategoryStruct.comp
(((F.mapHomologicalComplex (ComplexShape.down ℕ)).comp
(HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n)).map
g)
(Q.isoLeftDerivedObj F n).inv)
This theorem states that, in the category theory context with the presence of additive categories and abelian categories, we can compute a left derived functor on a morphism using a descent of that morphism to a chain map between chosen projective resolutions. Given categories `C` and `D`, a functor `F` from `C` to `D`, and morphism `f` from `X` to `Y` in `C`, if we have projective resolutions `P` and `Q` of `X` and `Y` respectively, and a chain map `g` from the complex of `P` to the complex of `Q` that commutes with the morphism `f` and the projections `P.π` and `Q.π`, then the `n`-th left derived functor of `F` applied to the morphism `f` equals the composition of the isomorphisms from `P` and `Q` to their left derived objects and the map induced by `g` on the `n`-th homology groups, following through the functor `F` mapping the homological complexes associated to the down `ComplexShape` on `ℕ`.
More concisely: Given functor F from additive category C to abelian category D, morphism f : X -> Y in C, projective resolutions P of X and Q of Y, and a chain map g from the complex of P to the complex of Q commuting with f, projections, and F, the n-th left derived functor F.R^n(f) is equal to the composition of the isomorphisms from P and Q to their derived objects and the map induced by g on the n-th homology groups.
|
CategoryTheory.Functor.isZero_leftDerived_obj_projective_succ
theorem CategoryTheory.Functor.isZero_leftDerived_obj_projective_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.HasProjectiveResolutions C] [inst_4 : CategoryTheory.Abelian D]
(F : CategoryTheory.Functor C D) [inst_5 : F.Additive] (n : ℕ) (X : C) [inst_6 : CategoryTheory.Projective X],
CategoryTheory.Limits.IsZero ((F.leftDerived (n + 1)).obj X)
The theorem `CategoryTheory.Functor.isZero_leftDerived_obj_projective_succ` states that for any categories `C` and `D`, where `C` is abelian and has projective resolutions and `D` is abelian, for any functor `F` from `C` to `D` that is additive, and for any natural number `n` and any object `X` in `C` that is projective, the `(n + 1)`-th left derived functor of `F` applied to `X` is a zero object in the target category `D`. In other words, higher derived functors vanish on projective objects in abelian categories.
More concisely: For any additive functor F from an abelian category C with projective resolutions to an abelian category D, and for any projective object X in C, the (n+1)-th left derived functor of F applied to X is the zero object in D for all natural numbers n.
|
CategoryTheory.NatTrans.leftDerived_comp
theorem CategoryTheory.NatTrans.leftDerived_comp :
∀ {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.HasProjectiveResolutions C] [inst_4 : CategoryTheory.Abelian D]
{F G H : CategoryTheory.Functor C D} [inst_5 : F.Additive] [inst_6 : G.Additive] [inst_7 : H.Additive] (α : F ⟶ G)
(β : G ⟶ H) (n : ℕ),
CategoryTheory.NatTrans.leftDerived (CategoryTheory.CategoryStruct.comp α β) n =
CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.leftDerived α n)
(CategoryTheory.NatTrans.leftDerived β n)
This theorem, `CategoryTheory.NatTrans.leftDerived_comp`, states that for any categories `C` and `D` where `C` is an Abelian category and has projective resolutions, and `D` is also an Abelian category, given three functors `F`, `G`, and `H` from `C` to `D` that are additive, along with natural transformations `α` from `F` to `G` and `β` from `G` to `H`, and a natural number `n`, the `n`-th left derived functor of the composition of `α` and `β` is equal to the composition of the `n`-th left derived functor of `α` and the `n`-th left derived functor of `β`. This is a statement about the commutativity of certain operations in the context of Category Theory and Homological Algebra.
More concisely: For functors F, G, and H between Abelian categories C and D with projective resolutions, and additive natural transformations α: F ➔ G and β: G ➔ H, the n-th left derived functors of their composition agree, i.e., Lⁱ(H ∘ α) ≈ Lⁱ(α ∘ H).
|