Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-08 06:24 0c64b3d3

View on Github →

feat(algebra/category/Module): biproducts (#13908) Following the same pattern for AddCommGroup, create the instance for biproducts in Module R, and check they are isomorphic to the usual construction.

Estimated changes

Modified src/algebra/category/Group/biproducts.lean

added theorem AddCommGroup.binary_product_limit_cone_cone_π_app_left

added theorem AddCommGroup.binary_product_limit_cone_cone_π_app_right

modified def AddCommGroup.biproduct_iso_pi

added theorem AddCommGroup.biproduct_iso_pi_inv_comp_π

modified def AddCommGroup.has_limit.product_limit_cone

Created src/algebra/category/Module/biproducts.lean

added def Module.binary_product_limit_cone

added theorem Module.binary_product_limit_cone_cone_π_app_left

added theorem Module.binary_product_limit_cone_cone_π_app_right

added def Module.biprod_iso_prod

added theorem Module.biprod_iso_prod_inv_comp_fst

added theorem Module.biprod_iso_prod_inv_comp_snd

added def Module.biproduct_iso_pi

added theorem Module.biproduct_iso_pi_inv_comp_π

added def Module.has_limit.lift

added theorem Module.has_limit.lift_apply

added def Module.has_limit.product_limit_cone