Exact functors

In this file, it is shown that additive functors which preserves homology also preserves finite limits and finite colimits.

TODO: provive alternate characterizations of left/right exact functors in terms of preservation of exactness.

noncomputable def CategoryTheory.Functor.preservesFiniteLimitsOfPreservesHomology {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] [CategoryTheory.Functor.PreservesHomology F] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasKernels C] : CategoryTheory.Limits.PreservesFiniteLimits F

An additive functor which preserves homology preserves finite limits.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.Functor.preservesFiniteColimitsOfPreservesHomology {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] [CategoryTheory.Functor.PreservesHomology F] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasFiniteCoproducts C] [CategoryTheory.Limits.HasCokernels C] : CategoryTheory.Limits.PreservesFiniteColimits F

An additive which preserves homology preserves finite colimits.

Equations

• One or more equations did not get rendered due to their size.