Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-14 23:14 e4843ea0

View on Github →

chore(category_theory/subobject): split off specific subobjects (#7167)

Estimated changes

Modified src/category_theory/subobject/factor_thru.lean

deleted def category_theory.limits.equalizer_subobject

deleted theorem category_theory.limits.equalizer_subobject_arrow'

deleted theorem category_theory.limits.equalizer_subobject_arrow

deleted theorem category_theory.limits.equalizer_subobject_arrow_comp

deleted theorem category_theory.limits.equalizer_subobject_factors

deleted theorem category_theory.limits.equalizer_subobject_factors_iff

deleted def category_theory.limits.equalizer_subobject_iso

deleted def category_theory.limits.factor_thru_image_subobject

deleted def category_theory.limits.image_subobject

deleted theorem category_theory.limits.image_subobject_arrow'

deleted theorem category_theory.limits.image_subobject_arrow

deleted theorem category_theory.limits.image_subobject_arrow_comp

deleted theorem category_theory.limits.image_subobject_factors_comp_self

deleted def category_theory.limits.image_subobject_iso

deleted theorem category_theory.limits.image_subobject_iso_comp

deleted theorem category_theory.limits.image_subobject_le

deleted theorem category_theory.limits.image_subobject_le_mk

deleted def category_theory.limits.image_subobject_map

deleted theorem category_theory.limits.image_subobject_map_arrow

deleted def category_theory.limits.kernel_subobject

deleted theorem category_theory.limits.kernel_subobject_arrow'

deleted theorem category_theory.limits.kernel_subobject_arrow

deleted theorem category_theory.limits.kernel_subobject_arrow_comp

deleted theorem category_theory.limits.kernel_subobject_comp_mono

deleted theorem category_theory.limits.kernel_subobject_factors

deleted theorem category_theory.limits.kernel_subobject_factors_iff

deleted def category_theory.limits.kernel_subobject_iso

deleted theorem category_theory.limits.le_kernel_subobject

Created src/category_theory/subobject/limits.lean

added def category_theory.limits.equalizer_subobject

added theorem category_theory.limits.equalizer_subobject_arrow'

added theorem category_theory.limits.equalizer_subobject_arrow

added theorem category_theory.limits.equalizer_subobject_arrow_comp

added theorem category_theory.limits.equalizer_subobject_factors

added theorem category_theory.limits.equalizer_subobject_factors_iff

added def category_theory.limits.equalizer_subobject_iso

added def category_theory.limits.factor_thru_image_subobject

added def category_theory.limits.image_subobject

added theorem category_theory.limits.image_subobject_arrow'

added theorem category_theory.limits.image_subobject_arrow

added theorem category_theory.limits.image_subobject_arrow_comp

added theorem category_theory.limits.image_subobject_factors_comp_self

added def category_theory.limits.image_subobject_iso

added theorem category_theory.limits.image_subobject_iso_comp

added theorem category_theory.limits.image_subobject_le

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 def category_theory.limits.kernel_subobject

added theorem category_theory.limits.kernel_subobject_arrow'

added theorem category_theory.limits.kernel_subobject_arrow

added theorem category_theory.limits.kernel_subobject_arrow_comp

added theorem category_theory.limits.kernel_subobject_comp_mono

added theorem category_theory.limits.kernel_subobject_factors

added theorem category_theory.limits.kernel_subobject_factors_iff

added def category_theory.limits.kernel_subobject_iso

added theorem category_theory.limits.le_kernel_subobject