## 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):

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

#### 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: May 13 2021 at 22:15 UTC