Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-04 07:49 f4db322f

View on Github →

feat(category_theory/subobject): factoring morphisms through subobjects (#6302) The predicate h : P.factors f, for P : subobject Y and f : X ⟶ Y asserts the existence of some P.factor_thru f : X ⟶ (P : C) making the obvious diagram commute. We provide conditions for P.factors f, when P is a kernel/equalizer/image/inf/sup subobject.

Estimated changes

Modified src/category_theory/subobject.lean

added theorem category_theory.limits.equalizer_subobject_factors

added theorem category_theory.limits.equalizer_subobject_factors_iff

added theorem category_theory.limits.image_subobject_factors

added theorem category_theory.limits.image_subobject_le

added theorem category_theory.limits.kernel_subobject_factors

added theorem category_theory.limits.kernel_subobject_factors_iff

added def category_theory.mono_over.factor_thru

added def category_theory.mono_over.factors

added theorem category_theory.mono_over.image_mono_over_arrow

added theorem category_theory.subobject.bot_arrow

added def category_theory.subobject.bot_coe_iso_zero

added theorem category_theory.subobject.bot_factors_iff_zero

added theorem category_theory.subobject.eq_of_comp_arrow_eq

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_left_of_inf_factors

added theorem category_theory.subobject.factors_of_factors_right

added theorem category_theory.subobject.factors_of_le

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 theorem category_theory.subobject.inf_arrow_factors_left

added theorem category_theory.subobject.inf_arrow_factors_right

added theorem category_theory.subobject.inf_factors

added theorem category_theory.subobject.le_of_comm

added theorem category_theory.subobject.representative_arrow

added theorem category_theory.subobject.representative_coe

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_factors

added theorem category_theory.subobject.underlying_iso_arrow

added theorem category_theory.subobject.underlying_iso_id_eq_top_coe_iso_self

added theorem category_theory.subobject.underlying_iso_inv_top_arrow