Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-12 20:36 ef4d2354

View on Github →

feat(category_theory): biproducts, and biproducts in AddCommGroup (#2187) This PR

  1. adds typeclasses has_biproducts (implicitly restricting to finite biproducts, which is the only interesting case) and has_binary_biproducts, and the usual tooling for special shapes of limits.
  2. provides customised has_products and has_coproducts instances for AddCommGroup, which are both just dependent functions (for has_coproducts we have to assume the indexed type is finite and decidable)
  3. because these custom instances have identical underlying objects, it's trivial to put them together to get a has_biproducts AddCommGroup.
  4. as for 2 & 3 with binary biproducts for AddCommGroup, implemented simply as the cartesian group.

Estimated changes