kronecker-weber

Stream: Is there code for X?

[Suzuka Yu]

Greetings! I wonder whether we have Kronecker-Weber theorem in mathlib (every abelian extension of group of rational numbers is contained in a cyclotomic extension)

[Johan Commelin]

Nope, as far as I know, we don't. It would be really nice to have a project (eg on github) outlining the main steps needed to get there. Quite a number of the ingredients are done, I think.

[Kevin Buzzard]

There is a pretty low-level proof of this in Marcus' book on number fields (in the exercises IIRC) which only uses elementary arguments (in particular no local fields) and which would be an excellent project. There's also a proof in Washington cyclotomic fields but here he reduces to the local case and I'm not sure we have enough local theory to make this a pleasant exercise (although it's coming!)

[Suzuka Yu]

Kevin Buzzard 发言道：

There is a pretty low-level proof of this in Marcus' book on number fields (in the exercises IIRC) which only uses elementary arguments (in particular no local fields) and which would be an excellent project. There's also a proof in Washington cyclotomic fields but here he reduces to the local case and I'm not sure we have enough local theory to make this a pleasant exercise (although it's coming!)

Great! That will be exciting. Thanks for your help!

[Notification Bot]

2 messages were moved from this topic to #mathlib4 > Decomposition group of ideal by Kevin Buzzard.