Formalising towers of field extensions

Stream: new members

[Jakob Scholbach]

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]

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

[Adam Topaz]

So for example you can declare a tower of fields $K \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]

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

[Jakob Scholbach]

Thanks, @Adam Topaz!

[Johan Commelin]

@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 $K \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]

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

[Adam Topaz]

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

[Johan Commelin]

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]

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