Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-08 10:26 a3e21a88

View on Github →

feat(category_theory/zero): lemmas about zero objects and zero morphisms, and improve docs (#3315)

Estimated changes

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

added theorem category_theory.limits.cokernel.desc_zero

deleted def category_theory.limits.cokernel.π_zero_is_iso

added theorem category_theory.limits.kernel.lift_zero

deleted def category_theory.limits.kernel.ι_zero_is_iso

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

added theorem category_theory.limits.epi_of_target_iso_zero

added def category_theory.limits.has_image.zero

deleted theorem category_theory.limits.has_zero_object.zero_of_from_zero

deleted theorem category_theory.limits.has_zero_object.zero_of_to_zero

added theorem category_theory.limits.id_zero

added def category_theory.limits.id_zero_equiv_iso_zero

added theorem category_theory.limits.id_zero_equiv_iso_zero_apply_hom

added theorem category_theory.limits.id_zero_equiv_iso_zero_apply_inv

added theorem category_theory.limits.image.ι_zero'

added theorem category_theory.limits.image.ι_zero

added def category_theory.limits.image_zero'

added def category_theory.limits.image_zero

added def category_theory.limits.is_iso_zero_equiv

added def category_theory.limits.is_iso_zero_equiv_iso_zero

added def category_theory.limits.is_iso_zero_self_equiv

added def category_theory.limits.is_iso_zero_self_equiv_iso_zero

added def category_theory.limits.mono_factorisation_zero

added theorem category_theory.limits.mono_of_source_iso_zero

added theorem category_theory.limits.zero_of_from_zero

added theorem category_theory.limits.zero_of_source_iso_zero

added theorem category_theory.limits.zero_of_target_iso_zero

added theorem category_theory.limits.zero_of_to_zero