mathlib

6a5241f2 - refactor(algebra/category/*, category_theory/concrete_category): generalize universes for concrete categories (#3687)

refactor(algebra/category/*, category_theory/concrete_category): generalize universes for concrete categories (#3687) Currently, concrete categories need to be `large_category`s. In particular, if objects live in `Type u`, then morphisms live in `Type (u + 1)`. For the category of modules over some ring R, this is not necessarily true, because we have to take the universe of R into account. One way to deal with this problem is to just force the universe of the ring to be the same as the universe of the module. This [sounds like it shouldn't be much of an issue](https://github.com/leanprover-community/mathlib/pull/1420#discussion_r322607455), but unfortunately, [it is](https://github.com/leanprover-community/mathlib/pull/3621#issue-458293664). This PR * removes the constraint that a concrete category must be a `large_category`, * generalizes `Module R` and `Algebra R` to accept a universe parameter for the module/algebra and * adds a ton of universe annotations which become neccesary because of the change As a reward, we get `abelian AddCommGroup.{u}` for arbitrary `u` without any (additional) work. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>