Zulip Chat Archive
Stream: general
Topic: algebra over a ring
Kenny Lau (Dec 08 2018 at 20:24):
@Mario Carneiro Can we do algebra over a ring now? Can we prove that every ring is an Z-algebra? every abelian group is a Z-module?
Johan Commelin (Dec 08 2018 at 20:26):
Why should this be a problem?
Johan Commelin (Dec 08 2018 at 20:26):
We can just define the category of R-algebras. That shouldn't be hard.
Kenny Lau (Dec 08 2018 at 20:27):
typeclass problems
Kenny Lau (Dec 08 2018 at 20:29):
Kenny Lau (Dec 08 2018 at 20:29):
look, nobody gives a second look at this problem
Johan Commelin (Dec 08 2018 at 20:39):
I haven't looked at it because all my Lean time is currently going to sheaves. But I'm certainly interested in this.
Johan Commelin (Dec 08 2018 at 20:40):
I think that in the case of algebras I would go category-theoretic straight away. The more you bundle, the less likely you run into crazy type-class diamonds.
Patrick Massot (Dec 08 2018 at 20:41):
Unfortunately I'm not sure we got enough module refactor yet. As far as I understand, Mario still has to work on getting modules over several base rings to behave nicely
Last updated: Dec 20 2023 at 11:08 UTC