# Zulip Chat Archive

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

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.

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

I think that comment is misleading

#### Adam Topaz (Oct 18 2020 at 20:03):

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

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

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

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

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

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?

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