Zulip Chat Archive

Stream: general

Topic: algebra over a ring


view this post on Zulip 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?

view this post on Zulip Johan Commelin (Dec 08 2018 at 20:26):

Why should this be a problem?

view this post on Zulip Johan Commelin (Dec 08 2018 at 20:26):

We can just define the category of R-algebras. That shouldn't be hard.

view this post on Zulip Kenny Lau (Dec 08 2018 at 20:27):

typeclass problems

view this post on Zulip Kenny Lau (Dec 08 2018 at 20:29):

https://leanprover.zulipchat.com/#narrow/stream/113488-general/subject/ring.20algebras/near/133299335

view this post on Zulip Kenny Lau (Dec 08 2018 at 20:29):

look, nobody gives a second look at this problem

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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: May 13 2021 at 22:15 UTC