English
An additive functor preserving homology also preserves finite colimits, given the presence of zero object and cokernels, etc.
Русский
Аддитивный функтор, сохраняющий гомологию, сохраняет конечные колимиты, при условии существования нулевого объекта и кокernel.
LaTeX
$$$F\text{ additive} \land F\text{ preserves homology} \Rightarrow \mathrm{PreservesFiniteColimits}(F)$$$
Lean4
/-- 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 preservesFiniteColimits_tfae :
List.TFAE
[∀ (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), PreservesColimit (parallelPair f 0) F, PreservesFiniteColimits F] :=
by
tfae_have 1 → 2
| hF, S, ⟨hS, hf⟩ => by
have := preservesEpimorphisms_of_preserves_shortExact_right F hF
refine ⟨?_, inferInstance⟩
let T := ShortComplex.mk (Abelian.image.ι S.f) S.g (Abelian.image_ι_comp_eq_zero S.zero)
let φ : S.map F ⟶ T.map F :=
{ τ₁ := F.map <| Abelian.factorThruImage S.f
τ₂ := 𝟙 _
τ₃ := 𝟙 _
comm₁₂ :=
show _ ≫ F.map (kernel.ι _) = F.map _ ≫ 𝟙 _ by rw [← F.map_comp, Abelian.image.fac, Category.comp_id] }
exact (exact_iff_of_epi_of_isIso_of_mono φ).2 (hF T ⟨(S.exact_iff_exact_image_ι).1 hS⟩).1
tfae_have 2 → 3
| hF, X, Y, f => by
refine preservesColimit_of_preserves_colimit_cocone (cokernelIsCokernel f) ?_
apply (CokernelCofork.isColimitMapCoconeEquiv _ F).2
let S := ShortComplex.mk _ _ (cokernel.condition f)
let hS := hF S ⟨exact_cokernel f, inferInstance⟩
have : Epi (S.map F).g := hS.2
exact hS.1.gIsCokernel
tfae_have 3 → 4
| hF => by exact preservesFiniteColimits_of_preservesCokernels F
tfae_have 4 → 1
| ⟨_⟩, S, hS => (S.map F).exact_and_epi_g_iff_g_is_cokernel |>.2 ⟨CokernelCofork.mapIsColimit _ hS.gIsCokernel F⟩
tfae_finish
