Zulip Chat Archive

Stream: maths

Topic: The Type of R-algebras


view this post on Zulip Filippo A. E. Nuccio (Oct 18 2020 at 19:58):

It seems to me that in algebra.basic the structure algebra R A is the type of all possible R-algebras structures on the semi-ring A. This seems to me to be pretty different from the "Type of R-algebras". For instance, a term in algebra R A is not something I can look at as an R-module (although I can extract an R-module structure on A from it). My first question is if I am right or wrong. Secondly, I wonder if after all the type of R-algebras (exists, and) cannot be recovered by the above structure.

view this post on Zulip Johan Commelin (Oct 18 2020 at 20:02):

You are right. [algebra R A] says: hey, I want to assume that A is an R-algebra.

view this post on Zulip Johan Commelin (Oct 18 2020 at 20:02):

It sounds like you are looking for the category of all R-algebras.

view this post on Zulip Filippo A. E. Nuccio (Oct 18 2020 at 20:02):

I am asking because reading the lines

/-- The category of R-algebras where R is a commutative
ring is the under category R ↓ CRing. In the categorical
setting we have a forgetful functor R-Alg ⥤ R-Mod.
However here it extends module in order to preserve
definitional equality in certain cases. -/

I thought at first that the file would contain something closer to Algebras R rather than the possible R-structures.

view this post on Zulip Johan Commelin (Oct 18 2020 at 20:02):

I think that comment is misleading

view this post on Zulip Adam Topaz (Oct 18 2020 at 20:03):

docs#Algebra

view this post on Zulip Johan Commelin (Oct 18 2020 at 20:03):

We have the category of R-algebras somewhere

view this post on Zulip Patrick Massot (Oct 18 2020 at 20:03):

Our category theory enthusiasts sometimes write that kind of misleading docstrings.

view this post on Zulip Filippo A. E. Nuccio (Oct 18 2020 at 20:03):

Thanks! It's a pity, it can really be misleading (in the sense that the type of mislead people is at least inhabited by me)

view this post on Zulip Johan Commelin (Oct 18 2020 at 20:04):

I think this comment was written a long time ago, before there was much category theory. By someone who doesn't necessarily use the category theory library a lot.

view this post on Zulip Filippo A. E. Nuccio (Oct 18 2020 at 20:05):

Johan Commelin said:

You are right. [algebra R A] says: hey, I want to assume that A is an R-algebra.

Can you speculate a bit on this? I mean, if algebra R A is a type, how can it say "hey, I want to assume something"? The proof that it is inhabited would be such an assumption, right? I am really sorry, I don't want to be pedantic, I am simply going very slowly with my digestion of Type theory/

view this post on Zulip Johan Commelin (Oct 18 2020 at 20:06):

Compare with (G : Type) [group G]

view this post on Zulip Patrick Massot (Oct 18 2020 at 20:08):

Filippo, you are right that algebra R A is the type of R-algebra structures on A. Johan is commenting on the way you can use it thanks to Lean's type class inference mechanism.

view this post on Zulip Filippo A. E. Nuccio (Oct 18 2020 at 20:08):

Ah ok! The square brackets were the point: you are saying that if I write (A : Type) [algebra R A] I am insisting that A be an R-algebra.

view this post on Zulip Patrick Massot (Oct 18 2020 at 20:09):

Yes.

view this post on Zulip Filippo A. E. Nuccio (Oct 18 2020 at 20:09):

Ok, thanks so much to both of you.

view this post on Zulip Adam Topaz (Oct 18 2020 at 20:10):

The usual convention is that lowercase foo is the class and uppercase Foo is the category, e.g. group vs Group, etc. I don't know what will happen in lean4 :grimacing:

view this post on Zulip Johan Commelin (Oct 18 2020 at 20:10):

Note that you need to use it as follows: (R A : Type) [comm_semiring R] [semiring A] [algebra R A]

view this post on Zulip Johan Commelin (Oct 18 2020 at 20:12):

Adam Topaz said:

The usual convention is that lowercase foo is the class and uppercase Foo is the category, e.g. group vs Group, etc. I don't know what will happen in lean4 :grimacing:

It seems that we will be using 𝔉𝔯𝔞𝔨𝔱𝔲𝔯

view this post on Zulip Bryan Gin-ge Chen (Oct 18 2020 at 20:24):

Please submit PRs to fix any incorrect docstrings you see! :pray:

view this post on Zulip Adam Topaz (Oct 18 2020 at 21:36):

Ha, the docstring about algebras is not just in the wrong place, but it's also wrong mathematically! Algebras in mathlib do not need to be commutative, so the category of R algebras (in mathlib) is not the under category in CRing. Also CRing is CommRing in mathlib.

view this post on Zulip Filippo A. E. Nuccio (Oct 18 2020 at 21:54):

Adam Topaz said:

Ha, the docstring about algebras is not just in the wrong place, but it's also wrong mathematically! Algebras in mathlib do not need to be commutative, so the category of R algebras (in mathlib) is not the under category in CRing. Also CRing is CommRing in mathlib.

Ah wow. Do you want then to go ahead with the PR, as you are clearly much more knowledgeable than I am?

view this post on Zulip Scott Morrison (Oct 18 2020 at 22:04):

That doc-string was written be Kenny essentially before the category theory library existed, and no one has touched it since.

view this post on Zulip Adam Topaz (Oct 18 2020 at 22:23):

I can PR a fix to the docs, but I won't have time until Tuesday, so anyone else should feel free to do it.

view this post on Zulip Kenny Lau (Oct 18 2020 at 22:25):

It was written in 2018, and Lean changes very very fast.

view this post on Zulip Johan Commelin (Oct 19 2020 at 06:31):

I think that also, back in the day, algebras were commutative

view this post on Zulip Adam Topaz (Oct 19 2020 at 13:54):

I'm not sure whether someone else has already opened a PR for this, but if not: #4689


Last updated: May 11 2021 at 16:22 UTC