The Type of R-algebras

Stream: maths

[Filippo A. E. Nuccio]

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]

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

[Johan Commelin]

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

[Filippo A. E. Nuccio]

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]

I think that comment is misleading

[Adam Topaz]

docs#Algebra

[Johan Commelin]

We have the category of R-algebras somewhere

[Patrick Massot]

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

[Filippo A. E. Nuccio]

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]

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]

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]

Compare with (G : Type) [group G]

[Patrick Massot]

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]

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]

Yes.

[Filippo A. E. Nuccio]

Ok, thanks so much to both of you.

[Adam Topaz]

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]

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

[Johan Commelin]

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]

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

[Adam Topaz]

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]

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]

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

[Adam Topaz]

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]

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

[Johan Commelin]

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

[Adam Topaz]

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