Galois Theory in mathlib

Stream: mathlib4

[Andrew Yang]

TLDR: Is the following the best way to say "$L/K$ is galois with galois group $G$, ring of integers $B/A$ and $M$ is the fixed field of some $H \le G$ with ring of integers $C$"?

variable (G A K L B : Type*)
  [CommRing A] [CommRing B] [Field K] [Field L]
  [Algebra A K] [Algebra A B] [Algebra A L] [Algebra B L] [Algebra K L]
  [IsScalarTower A B L] [IsScalarTower A K L]
  [IsFractionRing A K] [IsFractionRing B L]
  [Group G] [MulSemiringAction G L] [MulSemiringAction G B]
  [IsScalarTower G B L]
  [Algebra.IsInvariant A B G] [Algebra.IsInvariant K L G]
  [SMulCommClass G K L] [SMulCommClass G A B]
  (C : Type*) [CommRing C] [Algebra A C] [Algebra C B] [IsScalarTower A C B]
  (M : Type*) [Field M] [Algebra K M] [Algebra M L] [IsScalarTower K M L]
  [Algebra C M] [IsFractionRing C M]
  [Algebra A M] [IsScalarTower A C M] [IsScalarTower A K M]
  [Algebra C L] [IsScalarTower C B L] [IsScalarTower C M L]
  (H : Subgroup G) [Algebra.IsInvariant M L H] [SMulCommClass H M L]
  [Algebra.IsInvariant C B H] [SMulCommClass H C B]

Problems with less generality:

1. The current spelling of "galois group" is just L ≃ₐ[K] L. But this is inconvenient because when $M$ is the fixed field of some $H \le \mathrm{Gal}(L/K)$, we would want to say that $H$ is the galois group of $L/M$, or that $G/H$ is the galois group of $M/K$ (if galois).
   So I am thinking we should use [MulSemiringAction G L] [FaithfulSMul G L] [SmulCommClass G K L] [Algebra.IsInvariant K L G] to mean "is galois group" and develop API from this.

2. The current approach of galois theory is to consider two Fields. A base field K and a large enough L and everything else is IntermediateField K L. But often we would start with some M/K and construct some field extension L/M, and it is now a pain to identify E with the image of it in L, especially when we have some primes and ring of integers floating around that also needs to be identifed with each other. (For example I'm now considering the inertia field of some cyclic extension and primes in them and it is driving lean (and me) insane) So this leads to the M stuff above. It is tempting to say that we just let H := FixingSubgroup M and not have an extra H : Subgroup, but often the construction goes the other way and it is also tedious to identify H with FixedField (FixingSubgroup H)

3. I think I'm fairly certain (after flt-regular) that we want the whole AKLB thing. Combining with the previous points we get GHABCKLM.

[Johan Commelin]

GHABCKLMFTW!

[Jz Pan]

In my opinion M should be IntermediateField K L, A should be Subring K, B should be Subring L, not sure about C. Of course the typeclass problem for this approach will be horrible...

[Christian Merten]

Can we introduce macros that expand to parts of this? For example [AKLB A K L B] expands to [CommRing A] [CommRing B] [Field K] [Field L] [Algebra A K] [Algebra A B] [Algebra A L] [Algebra B L] [Algebra K L] [IsScalarTower A B L] [IsScalarTower A K L] [IsFractionRing A K] [IsFractionRing B L]. This is of course similar to variable? but could be commited to mathlib and be used both in variable lines and type signatures of declarations.

[Vlad Tsyrklevich]

Perhaps others already know, but since I just learned about it recently, I'll mention that class abbrev (and also plain abbrev) can be used for this instead of a macro.

[Andrew Yang]

Unfortunately this doesn't work for some reason:

class abbrev Test (A B : Type*) := CommRing A, CommRing B, Algebra A B

And I might want it to be more smart, e.g. [AKLB A K L B] [AKLB A K M C] to not duplicate Algebra A K instances.

[Christian Merten]

I think variable? is smart enough to not duplicate instances, so an AKLB macro could do that as well.

[Vlad Tsyrklevich]

Andrew Yang said:

Unfortunately this doesn't work for some reason

Huh, I see. I hadn't considered what happens when the given classes have overlapping fields

[Kevin Buzzard]

Jz Pan said:

In my opinion M should be IntermediateField K L, A should be Subring K, B should be Subring L, not sure about C. Of course the typeclass problem for this approach will be horrible...

I think this is not an ideal approach. The moment we allow a "it's sometimes a ring and sometimes a subring" philosophy then we run into the problem that all of a sudden we need many many more lemmas for everything, because when on paper it says $A\subseteq K\subseteq L$ we need to deal with: A,K,L types, L a type and A,K subtypes, K and L types and A a subtype, and A K L all subtypes, so now we need 4 lemmas every time we have this situation, not one. For example in your situation the relationship $A\subseteq K\subseteq M$ is different to $A\subseteq K\subseteq L$ so lemmas developed for one situation will not apply in the other situation. There is also the problem that typeclass inference hates subtypes which have been promoted to types; if it needs to find an action of \u A on something with A : Subring K then it is very quick to realise that it will suffice to find an action of K on that same thing, but often K does not act (e.g. A acts on B but K does not) and this makes typeclass inference grind to a halt (recall for example all the problems we had with rings of integers when they were terms not types).

Way back in the day we had a very long discussion about this (the thread was called something like "Algebra is not scaling for me" (edit: it's here ). In the odd order theorem paper this problem was solved by letting everything be a subtype; all groups were subgroups of a large abstract ambient "universe group G" (rather like how Weil did algebraic geometry in the 1940s) and this trick worked for groups because if A and B were groups then there was always a large ambient group which contained A and B as subgroups, namely A x B. This trick doesn't work for rings though, because there's no ring which has Z/2 and Z/3 as subrings, and because we wanted to avoid this combinatorial explosion of lemmas we went with "everything is a type"; Kenny invented IsScalarTower to tell typeclass inference that a diagram commutes, and that was it. I think we need to stick with types or else we will end up in all kinds of problems. We maybe need to start to learn how to glue IsScalarTowers together to make more complex commutative diagrams.

[Yakov Pechersky]

This would throw a lot more typeclass arguments into the mix, but perhaps one shouldn't talk about the ring of integers, but _a_ ring that is an integer compatible ring, a la the difference between FractionField and IsFractionField.

[Yakov Pechersky]

But I guess that's how you have it written now anyway

[Yakov Pechersky]

So, let me then reverse the idea -- in this particular situation, maybe it's easier to work with explicit O K or FractionField in this case.

[Jz Pan]

Kevin Buzzard said:

... We maybe need to start to learn how to glue IsScalarTowers together to make more complex commutative diagrams.

☹. At least in this case we need a lot of IsScalarTower to fully describe the relationships of them:

B-L
| |
C-M
| |
A-K

In general if you have n objects then you may need O(n^3) IsScalarTower instances... that's messy.

[Riccardo Brasca]

It's even worse I am afraid, as sometimes it is natural to introduce $\mathrm{Frac}(A)$, that is not $K$. I am adding various instance to work with this setting in #21522.