Zulip Chat Archive

Could someone PR a module docstring for algebra.norm_eq_prod_embeddings? It's just hit mathlib. I want to use this theorem as an example of something on my blog and it would be good if someone added a nice docstring so I could point blog readers to the community API entry and it would look less intimidating than it does now.

Kevin Buzzard (Nov 09 2021 at 13:33):

How about

for L/K a finite separable extension of fields and E an algebraically closed extension of K, the norm (down to K) of an element x of L is equal to the product of the images of x over all the K-embeddings $latex \sigma$ of L into E.

am on mobile right now going to Cambridge :D

Chris Birkbeck (Nov 09 2021 at 13:40):

Sure I can try and do it .

Eric Rodriguez (Nov 09 2021 at 14:03):

#10242, for those following along here!

Chris Birkbeck (Nov 09 2021 at 14:04):

Ah yes, thank you!

Riccardo Brasca (Nov 09 2021 at 14:28):

Thanks! I wanted to do it before PRing it but I forgot

Riccardo Brasca (Nov 09 2021 at 17:13):

@Kevin Buzzard Depending on what you want to talk about, you may want to mention that in docs#algebra.norm_eq_prod_embeddings the assumption is_scalar_tower K L E is not needed, and I realized this just because the linter told me so. (Here $L/K$ is the fields extension we are talking about, and mathematically we take an algebraically closed extension of $L$ , that of course is also an algebraically closed extension of $K$ .)

Riccardo Brasca (Nov 09 2021 at 17:25):

I just realized that E is not even an L-algebra :sweat_smile:

Kevin Buzzard (Nov 10 2021 at 00:04):

Yes, everything is consistent

Kevin Buzzard (Nov 09 2021 at 13:23):

Kevin Buzzard (Nov 09 2021 at 13:33):

How about

for L/K a finite separable extension of fields and E an algebraically closed extension of K, the norm (down to K) of an element x of L is equal to the product of the images of x over all the K-embeddings $latex \sigma$ of L into E.