## Stream: maths

### Topic: The Type of R-algebras

#### 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.

#### 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.

#### Johan Commelin (Oct 18 2020 at 20:02):

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

#### Filippo A. E. Nuccio (Oct 18 2020 at 20:02):

/-- 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.

#### Johan Commelin (Oct 18 2020 at 20:02):

I think that comment is misleading

docs#Algebra

#### Johan Commelin (Oct 18 2020 at 20:03):

We have the category of R-algebras somewhere

#### Patrick Massot (Oct 18 2020 at 20:03):

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

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

#### 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.

#### 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/

#### Johan Commelin (Oct 18 2020 at 20:06):

Compare with (G : Type) [group G]

#### 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.

#### 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.

Yes.

#### Filippo A. E. Nuccio (Oct 18 2020 at 20:09):

Ok, thanks so much to both of you.

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

#### 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]

#### Johan Commelin (Oct 18 2020 at 20:12):

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 𝔉𝔯𝔞𝔨𝔱𝔲𝔯

#### Bryan Gin-ge Chen (Oct 18 2020 at 20:24):

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

#### 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.

#### Filippo A. E. Nuccio (Oct 18 2020 at 21:54):

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?

#### 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.

#### 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.

#### Kenny Lau (Oct 18 2020 at 22:25):

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

#### Johan Commelin (Oct 19 2020 at 06:31):

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

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