English
A functor that preserves exactness of short complexes preserves homology.
Русский
Функтор, сохраняющий точность кратких комплексов, сохраняет гомологию.
LaTeX
$$$L$ preservesHomology$$
Lean4
/-- A functor which preserves the exactness of short complexes preserves homology. -/
theorem preservesHomology_of_map_exact : L.PreservesHomology
where
preservesCokernels X Y
f := by
have := preservesEpimorphisms_of_map_exact _ hL
apply preservesColimit_of_preserves_colimit_cocone (cokernelIsCokernel f)
apply (CokernelCofork.isColimitMapCoconeEquiv _ L).2
have : Epi ((ShortComplex.mk _ _ (cokernel.condition f)).map L).g :=
by
dsimp
infer_instance
exact
(hL (ShortComplex.mk _ _ (cokernel.condition f))
(ShortComplex.exact_of_g_is_cokernel _ (cokernelIsCokernel f))).gIsCokernel
preservesKernels X Y
f := by
have := preservesMonomorphisms_of_map_exact _ hL
apply preservesLimit_of_preserves_limit_cone (kernelIsKernel f)
apply (KernelFork.isLimitMapConeEquiv _ L).2
have : Mono ((ShortComplex.mk _ _ (kernel.condition f)).map L).f :=
by
dsimp
infer_instance
exact
(hL (ShortComplex.mk _ _ (kernel.condition f)) (ShortComplex.exact_of_f_is_kernel _ (kernelIsKernel f))).fIsKernel
