Zulip Chat Archive

Stream: new members

Topic: Formalising towers of field extensions

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!

Adam Topaz (Feb 26 2021 at 20:01):

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

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]

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.

Jakob Scholbach (Feb 26 2021 at 20:10):

Thanks, @Adam Topaz!

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.

Johan Commelin (Feb 26 2021 at 20:11):

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

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

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.

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: Dec 20 2023 at 11:08 UTC