Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
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_ι