Zulip Chat Archive

Stream: new members

Topic: Formalising towers of field extensions


view this post on Zulip Jakob Scholbach (Feb 26 2021 at 19:59):

Another newbie question: What are efficient ways of encoding this common situation in field theory: "Let K \subset E \subset F be a tower of field extensions. If x in K is separable over F, then x is separable over E." When I try to formalise this, I find it cumbersome to use the [algebra K E] [algebra E F] notation since then I need to manually compile the composition of these two algebra maps into a new algebra to express the separability of x over K. I would normally think I should start from the datum of a functor (0 \to 1 \to 2) to the category of commutative rings (or fields). Is this finite category in the library? Or are there other convenient ways? Thanks!

view this post on Zulip Adam Topaz (Feb 26 2021 at 20:01):

This is a can of worms which can be tamed with docs#is_scalar_tower

view this post on Zulip Adam Topaz (Feb 26 2021 at 20:06):

So for example you can declare a tower of fields KLMK \subset L \subset M as follows:

import algebra.algebra.basic

variables {K L M : Type*} [field K] [field L] [field M]
  [algebra K L] [algebra K M] [algebra L M] [is_scalar_tower K L M]

view this post on Zulip Adam Topaz (Feb 26 2021 at 20:09):

Concerning your category 0120 \to 1 \to 2, this is "just" fin 2 with the category instance obtained automatically from its ordered structure.

view this post on Zulip Jakob Scholbach (Feb 26 2021 at 20:10):

Thanks, @Adam Topaz!

view this post on Zulip Johan Commelin (Feb 26 2021 at 20:11):

@Jakob Scholbach It took a while for us to figure this out. I very much agree that it is cumbersome that we need to write two lines of variables just to say "let KLMK \subset L \subset M be a field extension". But once you've done that at the top of your file, it is quite pleasant to use afterwards.

view this post on Zulip Johan Commelin (Feb 26 2021 at 20:11):

Other variants are short to introduce, but painful to use.

view this post on Zulip Adam Topaz (Feb 26 2021 at 20:12):

I would certainly advise against using a functor from fin 3 if you want to do any nontrivial algebra :)

view this post on Zulip Johan Commelin (Feb 26 2021 at 20:12):

There are some ideas how to make the variables line a lot shorter, but they would require modifying lean, and nobody has done that. Now that lean 4 is out, I guess we will wait till mathlib is ported before experimenting with such new features.

view this post on Zulip Jakob Scholbach (Feb 26 2021 at 20:15):

OK, this is at any rate beyond my horizon, so I will use the scalar tower then.


Last updated: May 11 2021 at 23:11 UTC