Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-17 18:46 8575f592

View on Github →

feat(category_theory/limits): preservation of zero morphisms (#12068)

Estimated changes

Modified src/category_theory/differential_object.lean

Created src/category_theory/limits/preserves/shapes/zero.lean

added def category_theory.functor.map_zero_object

added theorem category_theory.functor.preserves_zero_morphisms_of_map_zero_object

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

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

added def category_theory.limits.initial_iso_is_initial

added def category_theory.limits.terminal_iso_is_terminal

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

deleted theorem category_theory.limits.equivalence_preserves_zero_morphisms

added def category_theory.limits.has_zero_object.zero_iso_initial

added theorem category_theory.limits.has_zero_object.zero_iso_initial_hom

added theorem category_theory.limits.has_zero_object.zero_iso_initial_inv

added def category_theory.limits.has_zero_object.zero_iso_is_initial

added theorem category_theory.limits.has_zero_object.zero_iso_is_initial_hom

added theorem category_theory.limits.has_zero_object.zero_iso_is_initial_inv

added def category_theory.limits.has_zero_object.zero_iso_is_terminal

added theorem category_theory.limits.has_zero_object.zero_iso_is_terminal_hom

added theorem category_theory.limits.has_zero_object.zero_iso_is_terminal_inv

added def category_theory.limits.has_zero_object.zero_iso_terminal

added theorem category_theory.limits.has_zero_object.zero_iso_terminal_hom

added theorem category_theory.limits.has_zero_object.zero_iso_terminal_inv

deleted theorem category_theory.limits.is_equivalence_preserves_zero_morphisms

Modified src/category_theory/preadditive/additive_functor.lean

deleted theorem category_theory.functor.map_zero

deleted def category_theory.functor.map_zero_object

Modified src/category_theory/shift.lean