Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-21 15:58 852064aa

View on Github →

refactor(category_theory/subobject): split into smaller files (#6796) No change in content, just splitting into four files.

Estimated changes

Deleted src/category_theory/subobject.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

deleted def category_theory.limits.image_subobject_iso

deleted theorem category_theory.limits.image_subobject_le

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_factors

deleted theorem category_theory.limits.kernel_subobject_factors_iff

deleted def category_theory.limits.kernel_subobject_iso

deleted def category_theory.mono_over.arrow

deleted theorem category_theory.mono_over.bot_arrow

deleted def category_theory.mono_over.bot_le

deleted theorem category_theory.mono_over.bot_left

deleted def category_theory.mono_over.exists_iso_map

deleted def category_theory.mono_over.exists_pullback_adj

deleted def category_theory.mono_over.factor_thru

deleted def category_theory.mono_over.factors

deleted def category_theory.mono_over.forget

deleted def category_theory.mono_over.forget_image

deleted theorem category_theory.mono_over.forget_obj_hom

deleted theorem category_theory.mono_over.forget_obj_left

deleted def category_theory.mono_over.hom_mk

deleted def category_theory.mono_over.image

deleted def category_theory.mono_over.image_forget_adj

deleted def category_theory.mono_over.image_mono_over

deleted theorem category_theory.mono_over.image_mono_over_arrow

deleted def category_theory.mono_over.inf

deleted def category_theory.mono_over.inf_le_left

deleted def category_theory.mono_over.inf_le_right

deleted def category_theory.mono_over.iso_mk

deleted def category_theory.mono_over.le_inf

deleted def category_theory.mono_over.le_sup_left

deleted def category_theory.mono_over.le_sup_right

deleted def category_theory.mono_over.le_top

deleted def category_theory.mono_over.lift

deleted theorem category_theory.mono_over.lift_comm

deleted def category_theory.mono_over.lift_comp

deleted def category_theory.mono_over.lift_id

deleted def category_theory.mono_over.lift_iso

deleted def category_theory.mono_over.map

deleted def category_theory.mono_over.map_bot

deleted def category_theory.mono_over.map_comp

deleted def category_theory.mono_over.map_id

deleted def category_theory.mono_over.map_iso

deleted theorem category_theory.mono_over.map_obj_arrow

deleted theorem category_theory.mono_over.map_obj_left

deleted def category_theory.mono_over.map_pullback_adj

deleted def category_theory.mono_over.map_top

deleted def category_theory.mono_over.mk'

deleted theorem category_theory.mono_over.mk'_arrow

deleted def category_theory.mono_over.pullback

deleted def category_theory.mono_over.pullback_comp

deleted def category_theory.mono_over.pullback_id

deleted def category_theory.mono_over.pullback_map_self

deleted theorem category_theory.mono_over.pullback_obj_arrow

deleted theorem category_theory.mono_over.pullback_obj_left

deleted def category_theory.mono_over.pullback_self

deleted def category_theory.mono_over.pullback_top

deleted def category_theory.mono_over.slice

deleted def category_theory.mono_over.sup

deleted def category_theory.mono_over.sup_le

deleted theorem category_theory.mono_over.top_arrow

deleted def category_theory.mono_over.top_le_pullback_self

deleted theorem category_theory.mono_over.top_left

deleted theorem category_theory.mono_over.w

deleted def category_theory.mono_over.«exists»

deleted def category_theory.mono_over

deleted def category_theory.subobject.arrow

deleted theorem category_theory.subobject.bot_arrow

deleted def category_theory.subobject.bot_coe_iso_zero

deleted theorem category_theory.subobject.bot_eq_zero

deleted theorem category_theory.subobject.bot_factors_iff_zero

deleted theorem category_theory.subobject.eq_of_comp_arrow_eq

deleted theorem category_theory.subobject.exists_iso_map

deleted def category_theory.subobject.exists_pullback_adj

deleted def category_theory.subobject.factor_thru

deleted theorem category_theory.subobject.factor_thru_arrow

deleted theorem category_theory.subobject.factor_thru_eq_zero

deleted theorem category_theory.subobject.factor_thru_right

deleted def category_theory.subobject.factors

deleted theorem category_theory.subobject.factors_comp_arrow

deleted theorem category_theory.subobject.factors_iff

deleted theorem category_theory.subobject.factors_left_of_inf_factors

deleted theorem category_theory.subobject.factors_of_factors_right

deleted theorem category_theory.subobject.factors_of_le

deleted theorem category_theory.subobject.factors_right_of_inf_factors

deleted theorem category_theory.subobject.finset_inf_arrow_factors

deleted theorem category_theory.subobject.finset_inf_factors

deleted theorem category_theory.subobject.finset_sup_factors

deleted def category_theory.subobject.functor

deleted def category_theory.subobject.inf

deleted theorem category_theory.subobject.inf_arrow_factors_left

deleted theorem category_theory.subobject.inf_arrow_factors_right

deleted theorem category_theory.subobject.inf_def

deleted theorem category_theory.subobject.inf_eq_map_pullback'

deleted theorem category_theory.subobject.inf_eq_map_pullback

deleted theorem category_theory.subobject.inf_factors

deleted theorem category_theory.subobject.inf_le_left

deleted theorem category_theory.subobject.inf_le_right

deleted theorem category_theory.subobject.inf_map

deleted theorem category_theory.subobject.inf_pullback

deleted theorem category_theory.subobject.le_inf

deleted theorem category_theory.subobject.le_of_comm

deleted def category_theory.subobject.lower

deleted def category_theory.subobject.lower_adjunction

deleted theorem category_theory.subobject.lower_comm

deleted def category_theory.subobject.lower_equivalence

deleted theorem category_theory.subobject.lower_iso

deleted def category_theory.subobject.lower₂

deleted def category_theory.subobject.map

deleted theorem category_theory.subobject.map_bot

deleted theorem category_theory.subobject.map_comp

deleted theorem category_theory.subobject.map_id

deleted def category_theory.subobject.map_iso

deleted def category_theory.subobject.map_iso_to_order_iso

deleted theorem category_theory.subobject.map_iso_to_order_iso_apply

deleted theorem category_theory.subobject.map_iso_to_order_iso_symm_apply

deleted theorem category_theory.subobject.map_pullback

deleted def category_theory.subobject.map_pullback_adj

deleted theorem category_theory.subobject.map_top

deleted def category_theory.subobject.mk

deleted theorem category_theory.subobject.prod_eq_inf

deleted def category_theory.subobject.pullback

deleted theorem category_theory.subobject.pullback_comp

deleted theorem category_theory.subobject.pullback_id

deleted theorem category_theory.subobject.pullback_map_self

deleted theorem category_theory.subobject.pullback_self

deleted theorem category_theory.subobject.pullback_top

deleted def category_theory.subobject.representative

deleted theorem category_theory.subobject.representative_arrow

deleted theorem category_theory.subobject.representative_coe

deleted def category_theory.subobject.representative_iso

deleted def category_theory.subobject.sup

deleted theorem category_theory.subobject.sup_factors_of_factors_left

deleted theorem category_theory.subobject.sup_factors_of_factors_right

deleted def category_theory.subobject.top_coe_iso_self

deleted theorem category_theory.subobject.top_eq_id

deleted theorem category_theory.subobject.top_factors

deleted def category_theory.subobject.underlying

deleted theorem category_theory.subobject.underlying_arrow

deleted theorem category_theory.subobject.underlying_as_coe

deleted def category_theory.subobject.underlying_iso

deleted theorem category_theory.subobject.underlying_iso_arrow

deleted theorem category_theory.subobject.underlying_iso_id_eq_top_coe_iso_self

deleted theorem category_theory.subobject.underlying_iso_inv_top_arrow

deleted def category_theory.subobject.«exists»

deleted def category_theory.subobject

Created src/category_theory/subobject/basic.lean

added def category_theory.subobject.arrow

added theorem category_theory.subobject.eq_of_comp_arrow_eq

added theorem category_theory.subobject.exists_iso_map

added def category_theory.subobject.exists_pullback_adj

added theorem category_theory.subobject.le_of_comm

added def category_theory.subobject.lower

added def category_theory.subobject.lower_adjunction

added theorem category_theory.subobject.lower_comm

added def category_theory.subobject.lower_equivalence

added theorem category_theory.subobject.lower_iso

added def category_theory.subobject.lower₂

added def category_theory.subobject.map

added theorem category_theory.subobject.map_comp

added theorem category_theory.subobject.map_id

added def category_theory.subobject.map_iso

added def category_theory.subobject.map_iso_to_order_iso

added theorem category_theory.subobject.map_iso_to_order_iso_apply

added theorem category_theory.subobject.map_iso_to_order_iso_symm_apply

added theorem category_theory.subobject.map_pullback

added def category_theory.subobject.map_pullback_adj

added def category_theory.subobject.mk

added def category_theory.subobject.pullback

added theorem category_theory.subobject.pullback_comp

added theorem category_theory.subobject.pullback_id

added theorem category_theory.subobject.pullback_map_self

added def category_theory.subobject.representative

added theorem category_theory.subobject.representative_arrow

added theorem category_theory.subobject.representative_coe

added def category_theory.subobject.representative_iso

added def category_theory.subobject.underlying

added theorem category_theory.subobject.underlying_arrow

added theorem category_theory.subobject.underlying_as_coe

added def category_theory.subobject.underlying_iso

added theorem category_theory.subobject.underlying_iso_arrow

added def category_theory.subobject.«exists»

added def category_theory.subobject

Created src/category_theory/subobject/default.lean

Created src/category_theory/subobject/factor_thru.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

added def category_theory.limits.image_subobject_iso

added theorem category_theory.limits.image_subobject_le

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_factors

added theorem category_theory.limits.kernel_subobject_factors_iff

added def category_theory.limits.kernel_subobject_iso

added def category_theory.mono_over.factor_thru

added def category_theory.mono_over.factors

added def category_theory.subobject.factor_thru

added theorem category_theory.subobject.factor_thru_arrow

added theorem category_theory.subobject.factor_thru_eq_zero

added theorem category_theory.subobject.factor_thru_right

added def category_theory.subobject.factors

added theorem category_theory.subobject.factors_comp_arrow

added theorem category_theory.subobject.factors_iff

added theorem category_theory.subobject.factors_of_factors_right

added theorem category_theory.subobject.factors_of_le

Created src/category_theory/subobject/lattice.lean

added theorem category_theory.mono_over.bot_arrow

added def category_theory.mono_over.bot_le

added theorem category_theory.mono_over.bot_left

added def category_theory.mono_over.inf

added def category_theory.mono_over.inf_le_left

added def category_theory.mono_over.inf_le_right

added def category_theory.mono_over.le_inf

added def category_theory.mono_over.le_sup_left

added def category_theory.mono_over.le_sup_right

added def category_theory.mono_over.le_top

added def category_theory.mono_over.map_bot

added def category_theory.mono_over.map_top

added def category_theory.mono_over.pullback_self

added def category_theory.mono_over.pullback_top

added def category_theory.mono_over.sup

added def category_theory.mono_over.sup_le

added theorem category_theory.mono_over.top_arrow

added def category_theory.mono_over.top_le_pullback_self

added theorem category_theory.mono_over.top_left

added theorem category_theory.subobject.bot_arrow

added def category_theory.subobject.bot_coe_iso_zero

added theorem category_theory.subobject.bot_eq_zero

added theorem category_theory.subobject.bot_factors_iff_zero

added theorem category_theory.subobject.factors_left_of_inf_factors

added theorem category_theory.subobject.factors_right_of_inf_factors

added theorem category_theory.subobject.finset_inf_arrow_factors

added theorem category_theory.subobject.finset_inf_factors

added theorem category_theory.subobject.finset_sup_factors

added def category_theory.subobject.functor

added def category_theory.subobject.inf

added theorem category_theory.subobject.inf_arrow_factors_left

added theorem category_theory.subobject.inf_arrow_factors_right

added theorem category_theory.subobject.inf_def

added theorem category_theory.subobject.inf_eq_map_pullback'

added theorem category_theory.subobject.inf_eq_map_pullback

added theorem category_theory.subobject.inf_factors

added theorem category_theory.subobject.inf_le_left

added theorem category_theory.subobject.inf_le_right

added theorem category_theory.subobject.inf_map

added theorem category_theory.subobject.inf_pullback

added theorem category_theory.subobject.le_inf

added theorem category_theory.subobject.map_bot

added theorem category_theory.subobject.map_top

added theorem category_theory.subobject.prod_eq_inf

added theorem category_theory.subobject.pullback_self

added theorem category_theory.subobject.pullback_top

added def category_theory.subobject.sup

added theorem category_theory.subobject.sup_factors_of_factors_left

added theorem category_theory.subobject.sup_factors_of_factors_right

added def category_theory.subobject.top_coe_iso_self

added theorem category_theory.subobject.top_eq_id

added theorem category_theory.subobject.top_factors

added theorem category_theory.subobject.underlying_iso_id_eq_top_coe_iso_self

added theorem category_theory.subobject.underlying_iso_inv_top_arrow

Created src/category_theory/subobject/mono_over.lean

added def category_theory.mono_over.arrow

added def category_theory.mono_over.exists_iso_map

added def category_theory.mono_over.exists_pullback_adj

added def category_theory.mono_over.forget

added def category_theory.mono_over.forget_image

added theorem category_theory.mono_over.forget_obj_hom

added theorem category_theory.mono_over.forget_obj_left

added def category_theory.mono_over.hom_mk

added def category_theory.mono_over.image

added def category_theory.mono_over.image_forget_adj

added def category_theory.mono_over.image_mono_over

added theorem category_theory.mono_over.image_mono_over_arrow

added def category_theory.mono_over.iso_mk

added def category_theory.mono_over.lift

added theorem category_theory.mono_over.lift_comm

added def category_theory.mono_over.lift_comp

added def category_theory.mono_over.lift_id

added def category_theory.mono_over.lift_iso

added def category_theory.mono_over.map

added def category_theory.mono_over.map_comp

added def category_theory.mono_over.map_id

added def category_theory.mono_over.map_iso

added theorem category_theory.mono_over.map_obj_arrow

added theorem category_theory.mono_over.map_obj_left

added def category_theory.mono_over.map_pullback_adj

added def category_theory.mono_over.mk'

added theorem category_theory.mono_over.mk'_arrow

added def category_theory.mono_over.pullback

added def category_theory.mono_over.pullback_comp

added def category_theory.mono_over.pullback_id

added def category_theory.mono_over.pullback_map_self

added theorem category_theory.mono_over.pullback_obj_arrow

added theorem category_theory.mono_over.pullback_obj_left

added def category_theory.mono_over.slice

added theorem category_theory.mono_over.w

added def category_theory.mono_over.«exists»

added def category_theory.mono_over

Modified src/category_theory/subterminal.lean