Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-27 16:37 bb44e1a0

View on Github →

feat(category_theory/subobject): generalise bot of subobject lattice (#8232)

Estimated changes

Modified src/algebra/homology/homology.lean

Modified src/category_theory/abelian/basic.lean

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

deleted theorem category_theory.limits.has_zero_object.has_initial

deleted theorem category_theory.limits.has_zero_object.has_terminal

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_of_has_initial_object

added def category_theory.limits.has_zero_object_of_has_terminal_object

Modified src/category_theory/subobject/factor_thru.lean

modified def category_theory.mono_over.factor_thru

modified def category_theory.mono_over.factors

Modified src/category_theory/subobject/lattice.lean

modified theorem category_theory.mono_over.bot_arrow

added theorem category_theory.mono_over.bot_arrow_eq_zero

added def category_theory.mono_over.bot_coe_iso_zero

modified theorem category_theory.mono_over.bot_left

added def category_theory.subobject.bot_coe_iso_initial

modified def category_theory.subobject.bot_coe_iso_zero

added theorem category_theory.subobject.bot_eq_initial_to

modified theorem category_theory.subobject.bot_eq_zero

Modified src/category_theory/subobject/limits.lean

modified theorem category_theory.limits.image_subobject_zero

modified theorem category_theory.limits.image_subobject_zero_arrow