preservesFiniteColimits_of_preservesHomology

English

If a functor preserves left-hand side exact sequences, then it preserves monomorphisms.

Русский

Если функтор сохраняет точные левосторонние последовательности, он сохраняет монохомоморфизмы.

LaTeX

$$$F\text{ preserves left-exact short sequences} \Rightarrow F\text{ preserves monomorphisms}$$$

Lean4

/-- An additive which preserves homology preserves finite colimits. -/
theorem preservesFiniteColimits_of_preservesHomology [HasFiniteCoproducts C] [HasCokernels C] :
    PreservesFiniteColimits F :=
  by
  have := fun {X Y : C} (f : X ⟶ Y) ↦ PreservesHomology.preservesCokernel F f
  have : HasBinaryBiproducts C := HasBinaryBiproducts.of_hasBinaryCoproducts
  have : HasCoequalizers C := Preadditive.hasCoequalizers_of_hasCokernels
  have : HasZeroObject D := ⟨F.obj 0, by rw [IsZero.iff_id_eq_zero, ← F.map_id, id_zero, F.map_zero]⟩
  exact preservesFiniteColimits_of_preservesCokernels F

Похожие утверждения