Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-22 01:34 77236cd2

View on Github →

refactor(category_theory): make has_zero_object a Prop (#13517)

Estimated changes

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

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

added theorem CommGroup.is_zero_of_subsingleton

added theorem Group.is_zero_of_subsingleton

Modified src/algebra/category/Module/basic.lean

added theorem Module.is_zero_of_subsingleton

Modified src/algebra/homology/augment.lean

Modified src/algebra/homology/homological_complex.lean

added theorem homological_complex.is_zero_zero

Modified src/algebra/homology/single.lean

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

added theorem SemiNormedGroup.is_zero_of_subsingleton

added theorem SemiNormedGroup₁.is_zero_of_subsingleton

Modified src/category_theory/abelian/basic.lean

Modified src/category_theory/abelian/right_derived.lean

Modified src/category_theory/differential_object.lean

Modified src/category_theory/functor/left_derived.lean

Modified src/category_theory/graded_object.lean

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

deleted def category_theory.limits.has_zero_object_of_has_finite_biproducts

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

added theorem category_theory.functor.zero_obj

deleted theorem category_theory.limits.has_zero_object.functor.zero_map

deleted theorem category_theory.limits.has_zero_object.functor.zero_obj

added theorem category_theory.limits.has_zero_object_of_has_initial_object

deleted def category_theory.limits.has_zero_object_of_has_initial_object

added theorem category_theory.limits.has_zero_object_of_has_terminal_object

deleted def category_theory.limits.has_zero_object_of_has_terminal_object

added theorem category_theory.limits.is_zero.map

added theorem category_theory.zero_map

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

added theorem category_theory.functor.is_zero

added theorem category_theory.functor.is_zero_iff

added theorem category_theory.iso.is_zero_iff

deleted def category_theory.limits.has_zero_object.is_zero.iso_zero

deleted theorem category_theory.limits.has_zero_object.is_zero_zero

added theorem category_theory.limits.is_zero.has_zero_object

added def category_theory.limits.is_zero.iso_zero

added theorem category_theory.limits.is_zero.obj

added theorem category_theory.limits.is_zero_zero

deleted theorem category_theory.limits.iso.is_zero_iff