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.preservesFiniteLimitsOfPreservesHomology: if F preserves homology, then F preserves finite limits.
• Functor.preservesFiniteColimitsOfPreservesHomology: 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.

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) [F.Additive] [F.PreservesHomology] [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) [F.Additive] [F.PreservesHomology] [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.

theorem CategoryTheory.Functor.preservesMonomorphisms_of_preserves_shortExact_left {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Abelian C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] (h : ∀ (S : CategoryTheory.ShortComplex C), S.ShortExact → (S.map F).Exact ∧ CategoryTheory.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} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Abelian C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] : [∀ (S : CategoryTheory.ShortComplex C), S.ShortExact → (S.map F).Exact ∧ CategoryTheory.Mono (F.map S.f), ∀ (S : CategoryTheory.ShortComplex C), S.Exact ∧ CategoryTheory.Mono S.f → (S.map F).Exact ∧ CategoryTheory.Mono (F.map S.f), ∀ ⦃X Y : C⦄ (f : X ⟶ Y), Nonempty (CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) F), Nonempty (CategoryTheory.Limits.PreservesFiniteLimits F)].TFAE

For an addivite 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.preservesEpimorphisms_of_preserves_shortExact_right {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Abelian C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] (h : ∀ (S : CategoryTheory.ShortComplex C), S.ShortExact → (S.map F).Exact ∧ CategoryTheory.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} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Abelian C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] : [∀ (S : CategoryTheory.ShortComplex C), S.ShortExact → (S.map F).Exact ∧ CategoryTheory.Epi (F.map S.g), ∀ (S : CategoryTheory.ShortComplex C), S.Exact ∧ CategoryTheory.Epi S.g → (S.map F).Exact ∧ CategoryTheory.Epi (F.map S.g), ∀ ⦃X Y : C⦄ (f : X ⟶ Y), Nonempty (CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) F), Nonempty (CategoryTheory.Limits.PreservesFiniteColimits F)].TFAE

For an addivite 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} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Abelian C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] : [∀ (S : CategoryTheory.ShortComplex C), S.ShortExact → (S.map F).ShortExact, ∀ (S : CategoryTheory.ShortComplex C), S.Exact → (S.map F).Exact, Nonempty F.PreservesHomology, Nonempty (CategoryTheory.Limits.PreservesFiniteLimits F) ∧ Nonempty (CategoryTheory.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.