Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-09 22:57 309e3b08

View on Github →

feat(category_theory/subobjects): improvements to API (#6932) These additions have been useful while setting up homology.

Estimated changes

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

Modified src/category_theory/subobject/basic.lean

added def category_theory.subobject.iso_of_eq

added def category_theory.subobject.iso_of_eq_mk

added def category_theory.subobject.iso_of_mk_eq

added def category_theory.subobject.iso_of_mk_eq_mk

modified def category_theory.subobject.of_le

modified theorem category_theory.subobject.of_le_arrow

added theorem category_theory.subobject.of_le_comp_of_le

added theorem category_theory.subobject.of_le_comp_of_le_mk

modified def category_theory.subobject.of_le_mk

added theorem category_theory.subobject.of_le_mk_comp_of_mk_le

added theorem category_theory.subobject.of_le_mk_comp_of_mk_le_mk

added theorem category_theory.subobject.of_le_refl

modified def category_theory.subobject.of_mk_le

added theorem category_theory.subobject.of_mk_le_comp_of_le

added theorem category_theory.subobject.of_mk_le_comp_of_le_mk

modified def category_theory.subobject.of_mk_le_mk

added theorem category_theory.subobject.of_mk_le_mk_comp_of_mk_le

added theorem category_theory.subobject.of_mk_le_mk_comp_of_mk_le_mk

added theorem category_theory.subobject.of_mk_le_mk_refl

Modified src/category_theory/subobject/factor_thru.lean

deleted theorem category_theory.limits.image_subobject_factors

added theorem category_theory.limits.image_subobject_factors_comp_self

added theorem category_theory.limits.image_subobject_iso_comp

added theorem category_theory.limits.image_subobject_le_mk

added def category_theory.limits.image_subobject_map

added theorem category_theory.limits.image_subobject_map_arrow

added theorem category_theory.limits.kernel_subobject_comp_mono

added theorem category_theory.limits.le_kernel_subobject

added theorem category_theory.subobject.factor_thru_comp_arrow

added theorem category_theory.subobject.factor_thru_comp_of_le

added theorem category_theory.subobject.factor_thru_self

added theorem category_theory.subobject.factor_thru_zero

added theorem category_theory.subobject.factors_self

added theorem category_theory.subobject.factors_zero

Modified src/category_theory/subobject/lattice.lean