Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-28 09:27 a574db13

View on Github →

refactor(algebra/category/*/limits): refactor concrete limits (#3463) We used to construct categorical limits for AddCommGroup and CommRing. Now we construct them for

  • (Add)(Comm)Mon
  • (Add)(Comm)Group
  • (Comm)(Semi)Ring
  • Module R
  • Algebra R Even better, we reuse structure along the way, and show that all the relevant forgetful functors preserve limits. We're still not at the point were this can either be done by
  • automation, or
  • noticing that everything is a model of a Lawvere theory but ... maybe one day.

Estimated changes