preservesFiniteLimits_of_preservesHomology

English

An additive functor that preserves homology preserves finite limits, given existence of zero object and finite products/kernels in the source and target.

Русский

Аддитивный функтор, сохраняющий гомологию, сохраняет конечные пределы, если существуют нулевой объект, конечные произведения и ядра.

LaTeX

$$$F\text{ additive} \land F\text{ preserves homology} \Rightarrow \mathrm{PreservesFiniteLimits}(F)$$$

Lean4

/-- An additive functor which preserves homology preserves finite limits. -/
theorem preservesFiniteLimits_of_preservesHomology [HasFiniteProducts C] [HasKernels C] : PreservesFiniteLimits F :=
  by
  have := fun {X Y : C} (f : X ⟶ Y) ↦ PreservesHomology.preservesKernel F f
  have : HasBinaryBiproducts C := HasBinaryBiproducts.of_hasBinaryProducts
  have : HasEqualizers C := Preadditive.hasEqualizers_of_hasKernels
  have : HasZeroObject D := ⟨F.obj 0, by rw [IsZero.iff_id_eq_zero, ← F.map_id, id_zero, F.map_zero]⟩
  exact preservesFiniteLimits_of_preservesKernels F

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