Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-26 20:55 4cf0e600

View on Github →

feat(category_theory/limits): generalize has_biproduct.of_has_product (#12116)

Estimated changes

Modified src/category_theory/limits/shapes/biproducts.lean

added def category_theory.limits.bicone_is_bilimit_of_colimit_cocone_of_is_colimit

added def category_theory.limits.bicone_is_bilimit_of_limit_cone_of_is_limit

added theorem category_theory.limits.binary_bicone.binary_cofan_inl_to_cocone

added theorem category_theory.limits.binary_bicone.binary_cofan_inr_to_cocone

added theorem category_theory.limits.binary_bicone.binary_fan_fst_to_cone

added theorem category_theory.limits.binary_bicone.binary_fan_snd_to_cone

added def category_theory.limits.binary_bicone.of_colimit_cocone

added def category_theory.limits.binary_bicone.of_limit_cone

added def category_theory.limits.binary_bicone_is_bilimit_of_colimit_cocone_of_is_colimit

added def category_theory.limits.binary_bicone_is_bilimit_of_limit_cone_of_is_limit

added theorem category_theory.limits.fst_of_is_colimit

modified theorem category_theory.limits.has_biproduct.of_has_coproduct

modified theorem category_theory.limits.has_biproduct.of_has_product

added theorem category_theory.limits.inl_of_is_limit

added theorem category_theory.limits.inr_of_is_limit

added def category_theory.limits.is_bilimit_of_is_colimit

added def category_theory.limits.is_bilimit_of_is_limit

added def category_theory.limits.is_bilimit_of_total

added def category_theory.limits.is_binary_bilimit_of_is_colimit

added def category_theory.limits.is_binary_bilimit_of_is_limit

added def category_theory.limits.is_binary_bilimit_of_total

added theorem category_theory.limits.snd_of_is_colimit