Commit 2020-09-01 12:18 6a5241f2

refactor(algebra/category/*, category_theory/concrete_category): generalize universes for concrete categories (#3687) Currently, concrete categories need to be large_categorys. 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, but unfortunately, it is. 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.