Left-derived functors #
We define the left-derived functors F.leftDerived n : C ⥤ D for any additive functor F
out of a category with projective resolutions.
We first define a functor
F.leftDerivedToHomotopyCategory : C ⥤ HomotopyCategory D (ComplexShape.down ℕ) which is
projectiveResolutions C ⋙ F.mapHomotopyCategory _. We show that if X : C and
P : ProjectiveResolution X, then F.leftDerivedToHomotopyCategory.obj X identifies
to the image in the homotopy category of the functor F applied objectwise to P.complex
(this isomorphism is P.isoLeftDerivedToHomotopyCategoryObj F).
Then, the left-derived functors F.leftDerived n : C ⥤ D are obtained by composing
F.leftDerivedToHomotopyCategory with the homology functors on the homotopy category.
Similarly we define natural transformations between left-derived functors coming from natural transformations between the original additive functors, and show how to compute the components.
Main results #
Functor.isZero_leftDerived_obj_projective_succ: projective objects have no higher left derived functor.NatTrans.leftDerived: the natural isomorphism between left derived functors induced by natural transformation.Functor.fromLeftDerivedZero: the natural transformationF.leftDerived 0 ⟶ F, which is an isomorphism whenFis right exact (i.e. preserves finite colimits), see alsoFunctor.leftDerivedZeroIsoSelf.
TODO #
- refactor
Functor.leftDerived(andFunctor.rightDerived) when the necessary material enters mathlib: derived categories, injective/projective derivability structures, existence of derived functors from derivability structures. Eventually, we shall get a right derived functorF.leftDerivedFunctorMinus : DerivedCategory.Minus C ⥤ DerivedCategory.Minus D, andF.leftDerivedshall be redefined usingF.leftDerivedFunctorMinus.
noncomputable def
CategoryTheory.Functor.leftDerivedToHomotopyCategory
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{u_2, u_1} D]
[Abelian C]
[HasProjectiveResolutions C]
[Abelian D]
(F : Functor C D)
[F.Additive]
:
Functor C (HomotopyCategory D (ComplexShape.down ℕ))
When F : C ⥤ D is an additive functor, this is
the functor C ⥤ HomotopyCategory D (ComplexShape.down ℕ) which
sends X : C to F applied to a projective resolution of X.
Equations
Instances For
noncomputable def
CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{u_2, u_1} D]
[Abelian C]
[HasProjectiveResolutions C]
[Abelian D]
{X : C}
(P : ProjectiveResolution X)
(F : Functor C D)
[F.Additive]
:
If P : ProjectiveResolution Z and F : C ⥤ D is an additive functor, this is
an isomorphism between F.leftDerivedToHomotopyCategory.obj X and the complex
obtained by applying F to P.complex.
Equations
Instances For
theorem
CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_inv_naturality
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{u_2, u_1} D]
[Abelian C]
[HasProjectiveResolutions C]
[Abelian D]
{X Y : C}
(f : X ⟶ Y)
(P : ProjectiveResolution X)
(Q : ProjectiveResolution Y)
(φ : P.complex ⟶ Q.complex)
(comm : CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryStruct.comp (P.π.f 0) f)
(F : Functor C D)
[F.Additive]
:
theorem
CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_inv_naturality_assoc
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{u_2, u_1} D]
[Abelian C]
[HasProjectiveResolutions C]
[Abelian D]
{X Y : C}
(f : X ⟶ Y)
(P : ProjectiveResolution X)
(Q : ProjectiveResolution Y)
(φ : P.complex ⟶ Q.complex)
(comm : CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryStruct.comp (P.π.f 0) f)
(F : Functor C D)
[F.Additive]
{Z : HomotopyCategory D (ComplexShape.down ℕ)}
(h : F.leftDerivedToHomotopyCategory.obj Y ⟶ Z)
:
CategoryStruct.comp (P.isoLeftDerivedToHomotopyCategoryObj F).inv
(CategoryStruct.comp (F.leftDerivedToHomotopyCategory.map f) h) = CategoryStruct.comp
((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map φ))
(CategoryStruct.comp (Q.isoLeftDerivedToHomotopyCategoryObj F).inv h)
theorem
CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_hom_naturality
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{u_2, u_1} D]
[Abelian C]
[HasProjectiveResolutions C]
[Abelian D]
{X Y : C}
(f : X ⟶ Y)
(P : ProjectiveResolution X)
(Q : ProjectiveResolution Y)
(φ : P.complex ⟶ Q.complex)
(comm : CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryStruct.comp (P.π.f 0) f)
(F : Functor C D)
[F.Additive]
:
theorem
CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_hom_naturality_assoc
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{u_2, u_1} D]
[Abelian C]
[HasProjectiveResolutions C]
[Abelian D]
{X Y : C}
(f : X ⟶ Y)
(P : ProjectiveResolution X)
(Q : ProjectiveResolution Y)
(φ : P.complex ⟶ Q.complex)
(comm : CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryStruct.comp (P.π.f 0) f)
(F : Functor C D)
[F.Additive]
{Z : HomotopyCategory D (ComplexShape.down ℕ)}
(h :
(HomotopyCategory.quotient D (ComplexShape.down ℕ)).obj
((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj Q.complex) ⟶ Z)
:
CategoryStruct.comp (F.leftDerivedToHomotopyCategory.map f)
(CategoryStruct.comp (Q.isoLeftDerivedToHomotopyCategoryObj F).hom h) = CategoryStruct.comp (P.isoLeftDerivedToHomotopyCategoryObj F).hom
(CategoryStruct.comp
((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map φ))
h)
noncomputable def
CategoryTheory.Functor.leftDerived
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{u_2, u_1} D]
[Abelian C]
[HasProjectiveResolutions C]
[Abelian D]
(F : Functor C D)
[F.Additive]
(n : ℕ)
:
Functor C D
The left derived functors of an additive functor.
Equations
Instances For
noncomputable def
CategoryTheory.ProjectiveResolution.isoLeftDerivedObj
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{u_2, u_1} D]
[Abelian C]
[HasProjectiveResolutions C]
[Abelian D]
{X : C}
(P : ProjectiveResolution X)
(F : Functor C D)
[F.Additive]
(n : ℕ)
:
(F.leftDerived n).obj X ≅ (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).obj
((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex)
We can compute a left derived functor using a chosen projective resolution.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.ProjectiveResolution.isoLeftDerivedObj_hom_naturality
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{u_2, u_1} D]
[Abelian C]
[HasProjectiveResolutions C]
[Abelian D]
{X Y : C}
(f : X ⟶ Y)
(P : ProjectiveResolution X)
(Q : ProjectiveResolution Y)
(φ : P.complex ⟶ Q.complex)
(comm : CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryStruct.comp (P.π.f 0) f)
(F : Functor C D)
[F.Additive]
(n : ℕ)
:
CategoryStruct.comp ((F.leftDerived n).map f) (Q.isoLeftDerivedObj F n).hom = CategoryStruct.comp (P.isoLeftDerivedObj F n).hom
(((F.mapHomologicalComplex (ComplexShape.down ℕ)).comp
(HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n)).map
φ)
theorem
CategoryTheory.ProjectiveResolution.isoLeftDerivedObj_hom_naturality_assoc
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{u_2, u_1} D]
[Abelian C]
[HasProjectiveResolutions C]
[Abelian D]
{X Y : C}
(f : X ⟶ Y)
(P : ProjectiveResolution X)
(Q : ProjectiveResolution Y)
(φ : P.complex ⟶ Q.complex)
(comm : CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryStruct.comp (P.π.f 0) f)
(F : Functor C D)
[F.Additive]
(n : ℕ)
{Z : D}
(h :
(HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).obj
((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj Q.complex) ⟶ Z)
:
CategoryStruct.comp ((F.leftDerived n).map f) (CategoryStruct.comp (Q.isoLeftDerivedObj F n).hom h) = CategoryStruct.comp (P.isoLeftDerivedObj F n).hom
(CategoryStruct.comp
((HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).map
((F.mapHomologicalComplex (ComplexShape.down ℕ)).map φ))
h)
theorem
CategoryTheory.ProjectiveResolution.isoLeftDerivedObj_inv_naturality
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{u_2, u_1} D]
[Abelian C]
[HasProjectiveResolutions C]
[Abelian D]
{X Y : C}
(f : X ⟶ Y)
(P : ProjectiveResolution X)
(Q : ProjectiveResolution Y)
(φ : P.complex ⟶ Q.complex)
(comm : CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryStruct.comp (P.π.f 0) f)
(F : Functor C D)
[F.Additive]
(n : ℕ)
:
CategoryStruct.comp (P.isoLeftDerivedObj F n).inv ((F.leftDerived n).map f) = CategoryStruct.comp
(((F.mapHomologicalComplex (ComplexShape.down ℕ)).comp
(HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n)).map
φ)
(Q.isoLeftDerivedObj F n).inv
theorem
CategoryTheory.ProjectiveResolution.isoLeftDerivedObj_inv_naturality_assoc
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{u_2, u_1} D]
[Abelian C]
[HasProjectiveResolutions C]
[Abelian D]
{X Y : C}
(f : X ⟶ Y)
(P : ProjectiveResolution X)
(Q : ProjectiveResolution Y)
(φ : P.complex ⟶ Q.complex)
(comm : CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryStruct.comp (P.π.f 0) f)
(F : Functor C D)
[F.Additive]
(n : ℕ)
{Z : D}
(h : (F.leftDerived n).obj Y ⟶ Z)
:
CategoryStruct.comp (P.isoLeftDerivedObj F n).inv (CategoryStruct.comp ((F.leftDerived n).map f) h) = CategoryStruct.comp
((HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).map
((F.mapHomologicalComplex (ComplexShape.down ℕ)).map φ))
(CategoryStruct.comp (Q.isoLeftDerivedObj F n).inv h)
theorem
CategoryTheory.Functor.isZero_leftDerived_obj_projective_succ
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{u_2, u_1} D]
[Abelian C]
[HasProjectiveResolutions C]
[Abelian D]
(F : Functor C D)
[F.Additive]
(n : ℕ)
(X : C)
[Projective X]
:
Limits.IsZero ((F.leftDerived (n + 1)).obj X)
The higher derived functors vanish on projective objects.
theorem
CategoryTheory.Functor.leftDerived_map_eq
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{u_2, u_1} D]
[Abelian C]
[HasProjectiveResolutions C]
[Abelian D]
(F : Functor C D)
[F.Additive]
(n : ℕ)
{X Y : C}
(f : X ⟶ Y)
{P : ProjectiveResolution X}
{Q : ProjectiveResolution Y}
(g : P.complex ⟶ Q.complex)
(w : CategoryStruct.comp g Q.π = CategoryStruct.comp P.π ((ChainComplex.single₀ C).map f))
:
(F.leftDerived n).map f = CategoryStruct.comp (P.isoLeftDerivedObj F n).hom
(CategoryStruct.comp
(((F.mapHomologicalComplex (ComplexShape.down ℕ)).comp
(HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n)).map
g)
(Q.isoLeftDerivedObj F n).inv)
We can compute a left derived functor on a morphism using a descent of that morphism to a chain map between chosen projective resolutions.
noncomputable def
CategoryTheory.NatTrans.leftDerivedToHomotopyCategory
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{u_2, u_1} D]
[Abelian C]
[HasProjectiveResolutions C]
[Abelian D]
{F G : Functor C D}
[F.Additive]
[G.Additive]
(α : F ⟶ G)
:
The natural transformation
F.leftDerivedToHomotopyCategory ⟶ G.leftDerivedToHomotopyCategory induced by
a natural transformation F ⟶ G between additive functors.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.ProjectiveResolution.leftDerivedToHomotopyCategory_app_eq
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{u_2, u_1} D]
[Abelian C]
[HasProjectiveResolutions C]
[Abelian D]
{F G : Functor C D}
[F.Additive]
[G.Additive]
(α : F ⟶ G)
{X : C}
(P : ProjectiveResolution X)
:
(NatTrans.leftDerivedToHomotopyCategory α).app X = CategoryStruct.comp (P.isoLeftDerivedToHomotopyCategoryObj F).hom
(CategoryStruct.comp
((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app P.complex))
(P.isoLeftDerivedToHomotopyCategoryObj G).inv)
@[simp]
theorem
CategoryTheory.NatTrans.leftDerivedToHomotopyCategory_id
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{u_2, u_1} D]
[Abelian C]
[HasProjectiveResolutions C]
[Abelian D]
(F : Functor C D)
[F.Additive]
:
@[simp]
theorem
CategoryTheory.NatTrans.leftDerivedToHomotopyCategory_comp
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{u_2, u_1} D]
[Abelian C]
[HasProjectiveResolutions C]
[Abelian D]
{F G H : Functor C D}
(α : F ⟶ G)
(β : G ⟶ H)
[F.Additive]
[G.Additive]
[H.Additive]
:
theorem
CategoryTheory.NatTrans.leftDerivedToHomotopyCategory_comp_assoc
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{u_2, u_1} D]
[Abelian C]
[HasProjectiveResolutions C]
[Abelian D]
{F G H : Functor C D}
(α : F ⟶ G)
(β : G ⟶ H)
[F.Additive]
[G.Additive]
[H.Additive]
{Z : Functor C (HomotopyCategory D (ComplexShape.down ℕ))}
(h : H.leftDerivedToHomotopyCategory ⟶ Z)
:
noncomputable def
CategoryTheory.NatTrans.leftDerived
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{u_2, u_1} D]
[Abelian C]
[HasProjectiveResolutions C]
[Abelian D]
{F G : Functor C D}
[F.Additive]
[G.Additive]
(α : F ⟶ G)
(n : ℕ)
:
The natural transformation between left-derived functors induced by a natural transformation.
Equations
Instances For
@[simp]
theorem
CategoryTheory.NatTrans.leftDerived_id
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{u_2, u_1} D]
[Abelian C]
[HasProjectiveResolutions C]
[Abelian D]
(F : Functor C D)
[F.Additive]
(n : ℕ)
:
@[simp]
theorem
CategoryTheory.NatTrans.leftDerived_comp
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{u_2, u_1} D]
[Abelian C]
[HasProjectiveResolutions C]
[Abelian D]
{F G H : Functor C D}
[F.Additive]
[G.Additive]
[H.Additive]
(α : F ⟶ G)
(β : G ⟶ H)
(n : ℕ)
:
theorem
CategoryTheory.NatTrans.leftDerived_comp_assoc
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{u_2, u_1} D]
[Abelian C]
[HasProjectiveResolutions C]
[Abelian D]
{F G H : Functor C D}
[F.Additive]
[G.Additive]
[H.Additive]
(α : F ⟶ G)
(β : G ⟶ H)
(n : ℕ)
{Z : Functor C D}
(h : H.leftDerived n ⟶ Z)
:
CategoryStruct.comp (leftDerived (CategoryStruct.comp α β) n) h = CategoryStruct.comp (leftDerived α n) (CategoryStruct.comp (leftDerived β n) h)
theorem
CategoryTheory.ProjectiveResolution.leftDerived_app_eq
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{u_2, u_1} D]
[Abelian C]
[HasProjectiveResolutions C]
[Abelian D]
{F G : Functor C D}
[F.Additive]
[G.Additive]
(α : F ⟶ G)
{X : C}
(P : ProjectiveResolution X)
(n : ℕ)
:
(NatTrans.leftDerived α n).app X = CategoryStruct.comp (P.isoLeftDerivedObj F n).hom
(CategoryStruct.comp
((HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).map
((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app P.complex))
(P.isoLeftDerivedObj G n).inv)
A component of the natural transformation between left-derived functors can be computed using a chosen projective resolution.
noncomputable def
CategoryTheory.ProjectiveResolution.fromLeftDerivedZero'
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{u_2, u_1} D]
[Abelian C]
[Abelian D]
{X : C}
(P : ProjectiveResolution X)
(F : Functor C D)
[F.Additive]
:
If P : ProjectiveResolution X and F is an additive functor, this is
the canonical morphism from the opcycles in degree 0 of
(F.mapHomologicalComplex _).obj P.complex to F.obj X.
Equations
- P.fromLeftDerivedZero' F = ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex).descOpcycles (F.map (P.π.f 0)) 1 CategoryTheory.ProjectiveResolution.fromLeftDerivedZero'._proof_5 ⋯
Instances For
@[simp]
theorem
CategoryTheory.ProjectiveResolution.pOpcycles_comp_fromLeftDerivedZero'
{D : Type u_1}
[Category.{u_4, u_1} D]
[Abelian D]
{C : Type u_2}
[Category.{u_3, u_2} C]
[Abelian C]
{X : C}
(P : ProjectiveResolution X)
(F : Functor C D)
[F.Additive]
:
CategoryStruct.comp (((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex).pOpcycles 0)
(P.fromLeftDerivedZero' F) = F.map (P.π.f 0)
@[simp]
theorem
CategoryTheory.ProjectiveResolution.pOpcycles_comp_fromLeftDerivedZero'_assoc
{D : Type u_1}
[Category.{u_4, u_1} D]
[Abelian D]
{C : Type u_2}
[Category.{u_3, u_2} C]
[Abelian C]
{X : C}
(P : ProjectiveResolution X)
(F : Functor C D)
[F.Additive]
{Z : D}
(h : F.obj X ⟶ Z)
:
CategoryStruct.comp (((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex).pOpcycles 0)
(CategoryStruct.comp (P.fromLeftDerivedZero' F) h) = CategoryStruct.comp (F.map (P.π.f 0)) h
theorem
CategoryTheory.ProjectiveResolution.fromLeftDerivedZero'_naturality
{D : Type u_1}
[Category.{u_4, u_1} D]
[Abelian D]
{C : Type u_2}
[Category.{u_3, u_2} C]
[Abelian C]
{X Y : C}
(f : X ⟶ Y)
(P : ProjectiveResolution X)
(Q : ProjectiveResolution Y)
(φ : P.complex ⟶ Q.complex)
(comm : CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryStruct.comp (P.π.f 0) f)
(F : Functor C D)
[F.Additive]
:
CategoryStruct.comp (HomologicalComplex.opcyclesMap ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map φ) 0)
(Q.fromLeftDerivedZero' F) = CategoryStruct.comp (P.fromLeftDerivedZero' F) (F.map f)
theorem
CategoryTheory.ProjectiveResolution.fromLeftDerivedZero'_naturality_assoc
{D : Type u_1}
[Category.{u_4, u_1} D]
[Abelian D]
{C : Type u_2}
[Category.{u_3, u_2} C]
[Abelian C]
{X Y : C}
(f : X ⟶ Y)
(P : ProjectiveResolution X)
(Q : ProjectiveResolution Y)
(φ : P.complex ⟶ Q.complex)
(comm : CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryStruct.comp (P.π.f 0) f)
(F : Functor C D)
[F.Additive]
{Z : D}
(h : F.obj Y ⟶ Z)
:
CategoryStruct.comp (HomologicalComplex.opcyclesMap ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map φ) 0)
(CategoryStruct.comp (Q.fromLeftDerivedZero' F) h) = CategoryStruct.comp (P.fromLeftDerivedZero' F) (CategoryStruct.comp (F.map f) h)
instance
CategoryTheory.ProjectiveResolution.instIsIsoFromLeftDerivedZero'Self
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{u_2, u_1} D]
[Abelian C]
[Abelian D]
(F : Functor C D)
[F.Additive]
(X : C)
[Projective X]
:
IsIso ((self X).fromLeftDerivedZero' F)
noncomputable def
CategoryTheory.Functor.fromLeftDerivedZero
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{u_2, u_1} D]
[Abelian C]
[HasProjectiveResolutions C]
[Abelian D]
(F : Functor C D)
[F.Additive]
:
The natural transformation F.leftDerived 0 ⟶ F.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.ProjectiveResolution.fromLeftDerivedZero_eq
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{u_2, u_1} D]
[Abelian C]
[HasProjectiveResolutions C]
[Abelian D]
{X : C}
(P : ProjectiveResolution X)
(F : Functor C D)
[F.Additive]
:
F.fromLeftDerivedZero.app X = CategoryStruct.comp (P.isoLeftDerivedObj F 0).hom
(CategoryStruct.comp
(ChainComplex.isoHomologyι₀ ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex)).hom
(P.fromLeftDerivedZero' F))
instance
CategoryTheory.instIsIsoAppFromLeftDerivedZeroOfProjective
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{u_2, u_1} D]
[Abelian C]
[HasProjectiveResolutions C]
[Abelian D]
(F : Functor C D)
[F.Additive]
(X : C)
[Projective X]
:
IsIso (F.fromLeftDerivedZero.app X)
instance
CategoryTheory.instIsIsoFromLeftDerivedZero'
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{u_2, u_1} D]
[Abelian C]
[Abelian D]
(F : Functor C D)
[F.Additive]
[Limits.PreservesFiniteColimits F]
{X : C}
(P : ProjectiveResolution X)
:
IsIso (P.fromLeftDerivedZero' F)
instance
CategoryTheory.instIsIsoAppFromLeftDerivedZero
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{u_2, u_1} D]
[Abelian C]
[HasProjectiveResolutions C]
[Abelian D]
(F : Functor C D)
[F.Additive]
[Limits.PreservesFiniteColimits F]
(X : C)
:
IsIso (F.fromLeftDerivedZero.app X)
instance
CategoryTheory.instIsIsoFunctorFromLeftDerivedZero
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{u_2, u_1} D]
[Abelian C]
[HasProjectiveResolutions C]
[Abelian D]
(F : Functor C D)
[F.Additive]
[Limits.PreservesFiniteColimits F]
:
noncomputable def
CategoryTheory.Functor.leftDerivedZeroIsoSelf
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{u_2, u_1} D]
[Abelian C]
[HasProjectiveResolutions C]
[Abelian D]
(F : Functor C D)
[F.Additive]
[Limits.PreservesFiniteColimits F]
:
The canonical isomorphism F.leftDerived 0 ≅ F when F is right exact
(i.e. preserves finite colimits).
Equations
Instances For
@[simp]
theorem
CategoryTheory.Functor.leftDerivedZeroIsoSelf_hom
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{u_2, u_1} D]
[Abelian C]
[HasProjectiveResolutions C]
[Abelian D]
(F : Functor C D)
[F.Additive]
[Limits.PreservesFiniteColimits F]
:
@[simp]
theorem
CategoryTheory.Functor.leftDerivedZeroIsoSelf_hom_inv_id
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{u_2, u_1} D]
[Abelian C]
[HasProjectiveResolutions C]
[Abelian D]
(F : Functor C D)
[F.Additive]
[Limits.PreservesFiniteColimits F]
:
@[simp]
theorem
CategoryTheory.Functor.leftDerivedZeroIsoSelf_hom_inv_id_assoc
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{u_2, u_1} D]
[Abelian C]
[HasProjectiveResolutions C]
[Abelian D]
(F : Functor C D)
[F.Additive]
[Limits.PreservesFiniteColimits F]
{Z : Functor C D}
(h : F.leftDerived 0 ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Functor.leftDerivedZeroIsoSelf_inv_hom_id
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{u_2, u_1} D]
[Abelian C]
[HasProjectiveResolutions C]
[Abelian D]
(F : Functor C D)
[F.Additive]
[Limits.PreservesFiniteColimits F]
:
@[simp]
theorem
CategoryTheory.Functor.leftDerivedZeroIsoSelf_inv_hom_id_assoc
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{u_2, u_1} D]
[Abelian C]
[HasProjectiveResolutions C]
[Abelian D]
(F : Functor C D)
[F.Additive]
[Limits.PreservesFiniteColimits F]
{Z : Functor C D}
(h : F ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Functor.leftDerivedZeroIsoSelf_hom_inv_id_app
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{u_2, u_1} D]
[Abelian C]
[HasProjectiveResolutions C]
[Abelian D]
(F : Functor C D)
[F.Additive]
[Limits.PreservesFiniteColimits F]
(X : C)
:
CategoryStruct.comp (F.fromLeftDerivedZero.app X) (F.leftDerivedZeroIsoSelf.inv.app X) = CategoryStruct.id ((F.leftDerived 0).obj X)
@[simp]
theorem
CategoryTheory.Functor.leftDerivedZeroIsoSelf_hom_inv_id_app_assoc
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{u_2, u_1} D]
[Abelian C]
[HasProjectiveResolutions C]
[Abelian D]
(F : Functor C D)
[F.Additive]
[Limits.PreservesFiniteColimits F]
(X : C)
{Z : D}
(h : (F.leftDerived 0).obj X ⟶ Z)
:
CategoryStruct.comp (F.fromLeftDerivedZero.app X) (CategoryStruct.comp (F.leftDerivedZeroIsoSelf.inv.app X) h) = h
@[simp]
theorem
CategoryTheory.Functor.leftDerivedZeroIsoSelf_inv_hom_id_app
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{u_2, u_1} D]
[Abelian C]
[HasProjectiveResolutions C]
[Abelian D]
(F : Functor C D)
[F.Additive]
[Limits.PreservesFiniteColimits F]
(X : C)
:
CategoryStruct.comp (F.leftDerivedZeroIsoSelf.inv.app X) (F.fromLeftDerivedZero.app X) = CategoryStruct.id (F.obj X)
@[simp]
theorem
CategoryTheory.Functor.leftDerivedZeroIsoSelf_inv_hom_id_app_assoc
{C : Type u}
[Category.{v, u} C]
{D : Type u_1}
[Category.{u_2, u_1} D]
[Abelian C]
[HasProjectiveResolutions C]
[Abelian D]
(F : Functor C D)
[F.Additive]
[Limits.PreservesFiniteColimits F]
(X : C)
{Z : D}
(h : F.obj X ⟶ Z)
:
CategoryStruct.comp (F.leftDerivedZeroIsoSelf.inv.app X) (CategoryStruct.comp (F.fromLeftDerivedZero.app X) h) = h