Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-19 15:52 634eab10

View on Github →

feat(category_theory/limits): add characteristic predicate for zero objects (#13511)

Estimated changes

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

Modified src/analysis/normed/group/SemiNormedGroup.lean

Modified src/category_theory/closed/zero.lean

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

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

Renamed src/category_theory/limits/shapes/zero.lean to src/category_theory/limits/shapes/zero_morphisms.lean

deleted theorem category_theory.limits.has_zero_object.from_zero_ext

deleted theorem category_theory.limits.has_zero_object.to_zero_ext

deleted def category_theory.limits.has_zero_object.zero_is_initial

deleted def category_theory.limits.has_zero_object.zero_is_terminal

deleted def category_theory.limits.has_zero_object.zero_iso_initial

deleted def category_theory.limits.has_zero_object.zero_iso_is_initial

deleted def category_theory.limits.has_zero_object.zero_iso_is_terminal

deleted def category_theory.limits.has_zero_object.zero_iso_terminal

added def category_theory.limits.is_zero.has_zero_morphisms

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

added theorem category_theory.limits.has_zero_object.from_zero_ext

added def category_theory.limits.has_zero_object.is_zero.iso_zero

added theorem category_theory.limits.has_zero_object.is_zero_zero

added theorem category_theory.limits.has_zero_object.to_zero_ext

added def category_theory.limits.has_zero_object.zero_is_initial

added def category_theory.limits.has_zero_object.zero_is_terminal

added def category_theory.limits.has_zero_object.zero_iso_initial

added def category_theory.limits.has_zero_object.zero_iso_is_initial

added def category_theory.limits.has_zero_object.zero_iso_is_terminal

added def category_theory.limits.has_zero_object.zero_iso_terminal

added theorem category_theory.limits.is_zero.eq_from

added theorem category_theory.limits.is_zero.eq_of_src

added theorem category_theory.limits.is_zero.eq_of_tgt

added theorem category_theory.limits.is_zero.eq_to

added theorem category_theory.limits.is_zero.from_eq

added def category_theory.limits.is_zero.iso

added def category_theory.limits.is_zero.iso_is_initial

added def category_theory.limits.is_zero.iso_is_terminal

added theorem category_theory.limits.is_zero.of_iso

added theorem category_theory.limits.is_zero.to_eq

added structure category_theory.limits.is_zero

added theorem category_theory.limits.iso.is_zero_iff

Modified src/category_theory/simple.lean