Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-27 07:21 89c27ccd

View on Github →

feat(category/subobjects): more API on limit subobjects (#7203)

Estimated changes

Modified src/category_theory/subobject/limits.lean

modified def category_theory.limits.equalizer_subobject

modified theorem category_theory.limits.equalizer_subobject_arrow'

added theorem category_theory.limits.factor_thru_image_subobject_comp_self

added theorem category_theory.limits.factor_thru_image_subobject_comp_self_assoc

modified def category_theory.limits.image_subobject

modified theorem category_theory.limits.image_subobject_arrow'

added def category_theory.limits.image_subobject_comp_iso

added theorem category_theory.limits.image_subobject_comp_iso_hom_arrow

added theorem category_theory.limits.image_subobject_comp_iso_inv_arrow

added theorem category_theory.limits.image_subobject_comp_le

added theorem category_theory.limits.image_subobject_zero

added theorem category_theory.limits.image_subobject_zero_arrow

modified def category_theory.limits.kernel_subobject

modified theorem category_theory.limits.kernel_subobject_arrow'

added theorem category_theory.limits.kernel_subobject_comp_le

added def category_theory.limits.kernel_subobject_iso_comp

added theorem category_theory.limits.kernel_subobject_iso_comp_hom_arrow

added theorem category_theory.limits.kernel_subobject_iso_comp_inv_arrow

added theorem category_theory.limits.kernel_subobject_zero