Exact functors

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

Main results

Let F : C ⥤ D be an additive functor:

• Functor.preservesFiniteLimits_of_preservesHomology: if F preserves homology, then F preserves finite limits.
• Functor.preservesFiniteColimits_of_preservesHomology: if F preserves homology, then F preserves finite colimits.

If we further assume that C and D are abelian categories, then we have:

• Functor.preservesFiniteLimits_tfae: the following are equivalent:

  1. for every short exact sequence 0 ⟶ A ⟶ B ⟶ C ⟶ 0, 0 ⟶ F(A) ⟶ F(B) ⟶ F(C) ⟶ 0 is exact.
  2. for every exact sequence A ⟶ B ⟶ C where A ⟶ B is mono, F(A) ⟶ F(B) ⟶ F(C) is exact and F(A) ⟶ F(B) is mono.
  3. F preserves kernels.
  4. F preserves finite limits.

• Functor.preservesFiniteColimits_tfae: the following are equivalent:

  1. for every short exact sequence 0 ⟶ A ⟶ B ⟶ C ⟶ 0, F(A) ⟶ F(B) ⟶ F(C) ⟶ 0 is exact.
  2. for every exact sequence A ⟶ B ⟶ C where B ⟶ C is epi, F(A) ⟶ F(B) ⟶ F(C) is exact and F(B) ⟶ F(C) is epi.
  3. F preserves cokernels.
  4. F preserves finite colimits.

• Functor.exact_tfae: the following are equivalent:

  1. for every short exact sequence 0 ⟶ A ⟶ B ⟶ C ⟶ 0, 0 ⟶ F(A) ⟶ F(B) ⟶ F(C) ⟶ 0 is exact.
  2. for every exact sequence A ⟶ B ⟶ C, F(A) ⟶ F(B) ⟶ F(C) is exact.
  3. F preserves homology.
  4. F preserves both finite limits and finite colimits.

theorem CategoryTheory.Functor.preservesFiniteLimits_of_preservesHomology {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] (F : Functor C D) [F.Additive] [F.PreservesHomology] [Limits.HasZeroObject C] [Limits.HasFiniteProducts C] [Limits.HasKernels C] : Limits.PreservesFiniteLimits F

An additive functor which preserves homology preserves finite limits.

theorem CategoryTheory.Functor.preservesFiniteColimits_of_preservesHomology {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] (F : Functor C D) [F.Additive] [F.PreservesHomology] [Limits.HasZeroObject C] [Limits.HasFiniteCoproducts C] [Limits.HasCokernels C] : Limits.PreservesFiniteColimits F

An additive which preserves homology preserves finite colimits.

theorem CategoryTheory.Functor.preservesMonomorphisms_of_preserves_shortExact_left {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Abelian C] [Abelian D] (F : Functor C D) [F.Additive] (h : ∀ (S : ShortComplex C), S.ShortExact → (S.map F).Exact ∧ Mono (F.map S.f)) : F.PreservesMonomorphisms

If a functor F : C ⥤ D preserves short exact sequences on the left-hand side, (i.e. if 0 ⟶ A ⟶ B ⟶ C ⟶ 0 is exact then 0 ⟶ F(A) ⟶ F(B) ⟶ F(C) is exact) then it preserves monomorphism.

theorem CategoryTheory.Functor.preservesFiniteLimits_tfae {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Abelian C] [Abelian D] (F : Functor C D) [F.Additive] : [∀ (S : ShortComplex C), S.ShortExact → (S.map F).Exact ∧ Mono (F.map S.f), ∀ (S : ShortComplex C), S.Exact ∧ Mono S.f → (S.map F).Exact ∧ Mono (F.map S.f), ∀ ⦃X Y : C⦄ (f : X ⟶ Y), Limits.PreservesLimit (Limits.parallelPair f 0) F, Limits.PreservesFiniteLimits F].TFAE

For an additive functor F : C ⥤ D between abelian categories, the following are equivalent:

• F preserves short exact sequences on the left-hand side, i.e. if 0 ⟶ A ⟶ B ⟶ C ⟶ 0 is exact then 0 ⟶ F(A) ⟶ F(B) ⟶ F(C) is exact.
• F preserves exact sequences on the left-hand side, i.e. if A ⟶ B ⟶ C is exact where A ⟶ B is mono, then F(A) ⟶ F(B) ⟶ F(C) is exact and F(A) ⟶ F(B) is mono as well.
• F preserves kernels.
• F preserves finite limits.

theorem CategoryTheory.Functor.preservesFiniteLimits_iff_forall_exact_map_and_mono {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Abelian C] [Abelian D] (F : Functor C D) [F.Additive] : Limits.PreservesFiniteLimits F ↔ ∀ (S : ShortComplex C), S.ShortExact → (S.map F).Exact ∧ Mono (F.map S.f)

theorem CategoryTheory.Functor.preservesEpimorphisms_of_preserves_shortExact_right {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Abelian C] [Abelian D] (F : Functor C D) [F.Additive] (h : ∀ (S : ShortComplex C), S.ShortExact → (S.map F).Exact ∧ Epi (F.map S.g)) : F.PreservesEpimorphisms

If a functor F : C ⥤ D preserves exact sequences on the right-hand side (i.e. if 0 ⟶ A ⟶ B ⟶ C ⟶ 0 is exact then F(A) ⟶ F(B) ⟶ F(C) ⟶ 0 is exact), then it preserves epimorphisms.

theorem CategoryTheory.Functor.preservesFiniteColimits_tfae {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Abelian C] [Abelian D] (F : Functor C D) [F.Additive] : [∀ (S : ShortComplex C), S.ShortExact → (S.map F).Exact ∧ Epi (F.map S.g), ∀ (S : ShortComplex C), S.Exact ∧ Epi S.g → (S.map F).Exact ∧ Epi (F.map S.g), ∀ ⦃X Y : C⦄ (f : X ⟶ Y), Limits.PreservesColimit (Limits.parallelPair f 0) F, Limits.PreservesFiniteColimits F].TFAE

For an additive functor F : C ⥤ D between abelian categories, the following are equivalent:

• F preserves short exact sequences on the right-hand side, i.e. if 0 ⟶ A ⟶ B ⟶ C ⟶ 0 is exact then F(A) ⟶ F(B) ⟶ F(C) ⟶ 0 is exact.
• F preserves exact sequences on the right-hand side, i.e. if A ⟶ B ⟶ C is exact where B ⟶ C is epi, then F(A) ⟶ F(B) ⟶ F(C) ⟶ 0 is exact and F(B) ⟶ F(C) is epi as well.
• F preserves cokernels.
• F preserves finite colimits.

theorem CategoryTheory.Functor.exact_tfae {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Abelian C] [Abelian D] (F : Functor C D) [F.Additive] : [∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact, ∀ (S : ShortComplex C), S.Exact → (S.map F).Exact, F.PreservesHomology, Limits.PreservesFiniteLimits F ∧ Limits.PreservesFiniteColimits F].TFAE

For an additive functor F : C ⥤ D between abelian categories, the following are equivalent:

• F preserves short exact sequences, i.e. if 0 ⟶ A ⟶ B ⟶ C ⟶ 0 is exact then 0 ⟶ F(A) ⟶ F(B) ⟶ F(C) ⟶ 0 is exact.
• F preserves exact sequences, i.e. if A ⟶ B ⟶ C is exact then F(A) ⟶ F(B) ⟶ F(C) is exact.
• F preserves homology.
• F preserves both finite limits and finite colimits.

theorem CategoryTheory.Functor.preservesFiniteColimits_iff_forall_exact_map_and_epi {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Abelian C] [Abelian D] (F : Functor C D) [F.Additive] : Limits.PreservesFiniteColimits F ↔ ∀ (S : ShortComplex C), S.ShortExact → (S.map F).Exact ∧ Epi (F.map S.g)