Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-03 11:29 3781435d

View on Github →

feat(algebra/category/Group): the category of abelian groups is abelian (#3621)

Estimated changes

Created src/algebra/category/Group/abelian.lean

added def AddCommGroup.normal_epi

added def AddCommGroup.normal_mono

Modified src/algebra/category/Module/abelian.lean

modified def Module.normal_epi

modified def Module.normal_mono

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

modified def category_theory.limits.parallel_pair

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

added def category_theory.limits.comp_nat_iso

added def category_theory.limits.iso_of_ι

added def category_theory.limits.iso_of_π

added def category_theory.limits.of_ι_congr

added def category_theory.limits.of_π_congr

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

added def category_theory.equivalence_reflects_normal_epi

added def category_theory.equivalence_reflects_normal_mono

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

modified theorem category_theory.limits.equivalence_preserves_zero_morphisms

added theorem category_theory.limits.is_equivalence_preserves_zero_morphisms