Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-14 11:12 7bb10813

View on Github →

feat(category_theory): turn a split mono with cokernel into a biproduct (#13184)

Estimated changes

Modified src/category_theory/limits/shapes/biproducts.lean

added def category_theory.limits.binary_bicone_of_split_epi_of_kernel

added def category_theory.limits.binary_bicone_of_split_mono_of_cokernel

added def category_theory.limits.is_bilimit_binary_bicone_of_split_epi_of_kernel

added def category_theory.limits.is_bilimit_binary_bicone_of_split_mono_of_cokernel

Modified src/category_theory/limits/shapes/equalizers.lean

Modified src/category_theory/limits/shapes/kernels.lean

modified def category_theory.limits.cokernel_epi_comp

modified def category_theory.limits.is_cokernel_epi_comp

added theorem category_theory.limits.is_cokernel_epi_comp_desc

modified def category_theory.limits.is_kernel_comp_mono

added theorem category_theory.limits.is_kernel_comp_mono_lift

Modified src/category_theory/preadditive/default.lean

added theorem category_theory.preadditive.cokernel_cofork_of_cofork_of_π

added theorem category_theory.preadditive.cokernel_cofork_of_cofork_π

added theorem category_theory.preadditive.is_colimit_cofork_of_cokernel_cofork_desc

added theorem category_theory.preadditive.is_limit_fork_of_kernel_fork_lift

added theorem category_theory.preadditive.kernel_fork_of_fork_of_ι

added theorem category_theory.preadditive.kernel_fork_of_fork_ι