Commit 2022-03-12 02:28 8364980d

View on Github →

feat(category_theory): interderivability of kernel and equalizers in preadditive cats (#12576)

Estimated changes

Modified src/category_theory/idempotents/basic.lean

Modified src/category_theory/preadditive/default.lean

added def category_theory.preadditive.cofork_of_cokernel_cofork

added def category_theory.preadditive.cokernel_cofork_of_cofork

added def category_theory.preadditive.fork_of_kernel_fork

added theorem category_theory.preadditive.has_coequalizer_of_has_cokernel

added theorem category_theory.preadditive.has_cokernel_of_has_coequalizer

deleted theorem category_theory.preadditive.has_colimit_parallel_pair

added theorem category_theory.preadditive.has_equalizer_of_has_kernel

modified theorem category_theory.preadditive.has_kernel_of_has_equalizer

deleted theorem category_theory.preadditive.has_limit_parallel_pair

added def category_theory.preadditive.is_colimit_cofork_of_cokernel_cofork

added def category_theory.preadditive.is_colimit_cokernel_cofork_of_cofork

added def category_theory.preadditive.is_limit_fork_of_kernel_fork

added def category_theory.preadditive.is_limit_kernel_fork_of_fork

added def category_theory.preadditive.kernel_fork_of_fork