Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-06 06:56 f81f861e

View on Github →

feat(category_theory/limits): the kernel of the cokernel of an epimorphism is an isomorphism (#2088)

The kernel of the cokernel of an epimorphism is an isomorphism
Fix unused argument warnings
Remove a set_option
Fix a typo

Estimated changes

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

added theorem category_theory.limits.cocone_parallel_pair_ext

added theorem category_theory.limits.cocone_parallel_pair_left

added theorem category_theory.limits.cocone_parallel_pair_right

added def category_theory.limits.cocone_parallel_pair_self

added theorem category_theory.limits.cocone_parallel_pair_self_X

added theorem category_theory.limits.cocone_parallel_pair_self_ι_app_one

added theorem category_theory.limits.coequalizer.hom_ext

added theorem category_theory.limits.coequalizer.π.cofork

added theorem category_theory.limits.coequalizer.π.eq_app_one

added theorem category_theory.limits.coequalizer.π_epi

added def category_theory.limits.coequalizer.π_of_self'

added def category_theory.limits.coequalizer.π_of_self

added theorem category_theory.limits.cofork.eq_of_π_π

added def category_theory.limits.colimit_cocone_parallel_pair_self_is_iso'

added def category_theory.limits.colimit_cocone_parallel_pair_self_is_iso

added def category_theory.limits.equalizer.ι_of_self'

added def category_theory.limits.equalizer.ι_of_self

added def category_theory.limits.is_colimit_cocone_parallel_pair_self

added def category_theory.limits.limit_cone_parallel_pair_self_is_iso'

added def category_theory.limits.mono_limit_cocone_parallel_pair_is_iso

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

added def category_theory.limits.cokernel.is_colimit_cocone_zero_cocone

added def category_theory.limits.cokernel.of_epi

added def category_theory.limits.cokernel.of_kernel_of_mono

added def category_theory.limits.cokernel.zero_cocone

added theorem category_theory.limits.cokernel.π_of_epi

added def category_theory.limits.cokernel.π_of_zero

added def category_theory.limits.kernel.of_cokernel_of_epi

added def category_theory.limits.kernel.of_mono

added theorem category_theory.limits.kernel.ι_of_mono

added def category_theory.limits.kernel.ι_of_zero