Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-26 02:39 11179d53

View on Github →

feat(algebra/category/Group/*): compare categorical (co)kernels/images with the usual notions (#3443)

Estimated changes

Modified src/algebra/category/Group/colimits.lean

added def AddCommGroup.cokernel_iso_quotient

Modified src/algebra/category/Group/images.lean

added def AddCommGroup.image_iso_range

Modified src/algebra/category/Group/limits.lean

added def AddCommGroup.kernel_iso_ker

added theorem AddCommGroup.kernel_iso_ker_hom_comp_subtype

added theorem AddCommGroup.kernel_iso_ker_inv_comp_ι

added def AddCommGroup.kernel_iso_ker_over

Modified src/category_theory/limits/concrete_category.lean

Created src/category_theory/limits/shapes/concrete_category.lean

added theorem category_theory.limits.cokernel_condition_apply

added theorem category_theory.limits.kernel_condition_apply