Commit 2020-07-03 04:28 303740d4

View on Github →

feat(category_theory/abelian): every abelian category is preadditive (#3247)

Estimated changes

Modified src/category_theory/abelian/basic.lean

added def category_theory.abelian.has_finite_biproducts

added def category_theory.non_preadditive_abelian.abelian

Created src/category_theory/abelian/non_preadditive.lean

added theorem category_theory.non_preadditive_abelian.add_assoc

added theorem category_theory.non_preadditive_abelian.add_comm

added theorem category_theory.non_preadditive_abelian.add_comp

added theorem category_theory.non_preadditive_abelian.add_def

added theorem category_theory.non_preadditive_abelian.add_neg

added theorem category_theory.non_preadditive_abelian.add_neg_self

added theorem category_theory.non_preadditive_abelian.add_zero

added theorem category_theory.non_preadditive_abelian.comp_add

added theorem category_theory.non_preadditive_abelian.comp_sub

added def category_theory.non_preadditive_abelian.epi_is_cokernel_of_kernel

added theorem category_theory.non_preadditive_abelian.epi_of_zero_cancel

added theorem category_theory.non_preadditive_abelian.epi_of_zero_cokernel

added def category_theory.non_preadditive_abelian.has_add

added def category_theory.non_preadditive_abelian.has_colimit_parallel_pair

added def category_theory.non_preadditive_abelian.has_limit_parallel_pair

added def category_theory.non_preadditive_abelian.has_neg

added def category_theory.non_preadditive_abelian.has_sub

added def category_theory.non_preadditive_abelian.is_colimit_σ

added def category_theory.non_preadditive_abelian.is_iso_of_mono_of_epi

added theorem category_theory.non_preadditive_abelian.lift_map

added theorem category_theory.non_preadditive_abelian.lift_sub_lift

added theorem category_theory.non_preadditive_abelian.lift_σ

added def category_theory.non_preadditive_abelian.mono_is_kernel_of_cokernel

added theorem category_theory.non_preadditive_abelian.mono_of_cancel_zero

added theorem category_theory.non_preadditive_abelian.mono_of_zero_kernel

added theorem category_theory.non_preadditive_abelian.neg_add

added theorem category_theory.non_preadditive_abelian.neg_add_self

added theorem category_theory.non_preadditive_abelian.neg_def

added theorem category_theory.non_preadditive_abelian.neg_neg

added theorem category_theory.non_preadditive_abelian.neg_sub'

added theorem category_theory.non_preadditive_abelian.neg_sub

added def category_theory.non_preadditive_abelian.preadditive

added def category_theory.non_preadditive_abelian.pullback_of_mono

added def category_theory.non_preadditive_abelian.pushout_of_epi

added def category_theory.non_preadditive_abelian.r

added def category_theory.non_preadditive_abelian.strong_epi_of_epi

added theorem category_theory.non_preadditive_abelian.sub_add

added theorem category_theory.non_preadditive_abelian.sub_comp

added theorem category_theory.non_preadditive_abelian.sub_def

added theorem category_theory.non_preadditive_abelian.sub_self

added theorem category_theory.non_preadditive_abelian.sub_sub_sub

added theorem category_theory.non_preadditive_abelian.sub_zero

added def category_theory.non_preadditive_abelian.zero_cokernel_of_zero_cancel

added def category_theory.non_preadditive_abelian.zero_kernel_of_cancel_zero

added def category_theory.non_preadditive_abelian.Δ

added theorem category_theory.non_preadditive_abelian.Δ_map

added theorem category_theory.non_preadditive_abelian.Δ_σ

added def category_theory.non_preadditive_abelian.σ

added theorem category_theory.non_preadditive_abelian.σ_comp

Modified src/category_theory/discrete_category.lean

added def category_theory.discrete.nat_iso_functor

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

added def category_theory.limits.has_finite_biproducts.of_has_finite_coproducts

added def category_theory.limits.has_finite_biproducts.of_has_finite_products

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

added theorem category_theory.limits.cokernel_cofork.π_of_π

added theorem category_theory.limits.kernel_fork.ι_of_ι