Notation for Galois group

Stream: mathlib4

[Andrew Yang]

Would people be happy in the notation Gal(L|K) for L ≃ₐ[K] L? I think L ≃ₐ[K] L is quite unreadable both for beginners and more experienced users and this issue popped up in the CFT workshop two months ago.

[Kenny Lau]

I always support more notation

[Kenny Lau]

one question that would pop up is whether the delab should happen as well, and whether that would produce "false positives"

[Andrew Yang]

That would be my next question. When do we want this notation? Are we happy to write Gal(L|K) for non galois extensions? Are we happy to write Gal(B|A) for Ba galois algebra over A (e.g. $\mathcal{O}_L/\mathcal{O}_K$ with $L/K$ galois)?

[Kenny Lau]

well are you suggesting that we might want to try to synthesize some instance inside the delaborator

[Andrew Yang]

I am suggesting we should first figure out when we want to use this notation. How to write the delaborator will depend on this.

[Kenny Lau]

well practicality is a concern too, because it seems way easier (and "morally purer" whatever that means) to just elab and delab unconditionally, and assuming that I would not mind delaborating globally

(or maybe we can also scoped the notation to IsGalois)

[Kenny Lau]

so my current suggestion is to scoped the notation to IsGalois and delab unconditionally

[Andrew Yang]

This doesn't answer the question about when we want to use (as in write down) the notation.
Can we figure this out before we jump to implementation details?

[Kenny Lau]

I think mathematically people would prefer Aut(B|A) if it isn't a (finite) galois extension of fields

[Kenny Lau]

we could write Aut(B|A) in general and Gal(L|K) when it is finite galois field-ext

[Kenny Lau]

and the group theory one can be written Aut(G)

[Kevin Buzzard]

Surely Gal(L/K) (not |) and Aut_A(B) are more standard?

[Kenny Lau]

I think we've decided that [] is the lean equivalent of pseudo-tex _?

[Andrew Yang]

I also would prefer Gal(L/K) but the parser doesn't like that and confuses it with division.

[Yaël Dillies]

In @Edison Xie's BrauerGroup repo, I've introduced the notation Gal(L, K) and it's been tremendously useful in terms of readability (although it does trigger for non-Galois extensions)

[Thomas Murrills]

Andrew Yang said:

I also would prefer Gal(L/K) but the parser doesn't like that and confuses it with division.

Just playing around here, but

syntax "Gal(" term:prec "/" term ")" : term

with prec strictly above 70 (division’s precedence) seems to work. :) (If we want Gal(L x / K) to work, we want to keep it below arg (1023)).

(But Gal(L, K) might actually be more readable in Lean source.)

[Thomas Browning]

Slightly unrelated, but I think that in general moving over to docs#IsGaloisGroup will help reduce the pain of L ≃ₐ[K] L everywhere.

[Antoine Chambert-Loir]

Note: in the literature, both traditions exist, either of calling Gal the group of a non-Galois extension, or of having two notations for Aut, namely using Gal when it is Galois. The first one is OK, I believe, and consistent with the fact that in his framework, Galois only considered Galois extensions. (The group he considered was the group of permutations of all roots that preserve algebraic relations.)

[Filippo A. E. Nuccio]

I am slightly agains using Gal for L ≃ₐ[K] L, I must say. My main reasons are

• This goes a little bit agains the general Mathlib philosophy of living with generality even if it makes us depart slightly from math conventions: the typical example is Module instead of Vector Space. Although a bit puzzling at the beginning, I like it very much. Another is IsFractionRing without the need of FractionField.
• The second is that it does not convey any information about the assumptions, unlike the _a in the L ≃ₐ[K] L: yet, if we're going to set this notation generally, we would end up with, for instance, $\mathrm{Gal}(\mathbb{Q}/\mathbb{Z})$ or $\mathrm{Gal}(\mathbb{C}[X,y]/\mathbb{Z}(X))$ without a clear indication of what is meant.

I certainly hear Thomas' point of view, but I would perhaps prefer sticking to local notations instead of global ones.

[Kevin Buzzard]

I guess another way of saying Filippo's point: the argument for using Gal(L|K) instead of L ≃ₐ[K] L is that L ≃ₐ[K] L looks confusing. However Gal(ℂ|ℤ) also looks confusing (for different reasons).

[Andrew Yang]

I don't understand Filippo's first point but I totally agree with the second being potentially a problem. This is why I have been pushing us to have a discussion on when this notation is appropriate. For example Gal(ℚ|ℤ) definitely should not appear.

[Riccardo Brasca]

We can always discourage (i.e. forbidding in mathlib) to use Gal(A|B) unless A and B are fields (or whatever we want). The notation would still work, but in practice it is not used.

[Kevin Buzzard]

Andrew Yang said:

I don't understand the first point

It doesn't look confusing to us, but all these little a's and square brackets are mathlibisms so they look confusing to the general reader.

[Andrew Yang]

Sorry I meant Filippo's first point.

[Andrew Yang]

We can always discourage (i.e. forbidding in mathlib)

Yeah that was the idea. But I am still not sure what to allow. Are we happy with $\mathrm{Gal}(\mathbb{Q}(X)/\mathbb{Q})$ or $\mathrm{Gal}(\mathbb{Z}[i]/\mathbb{Z})$?

[Antoine Chambert-Loir]

Using the notation outside the realm of fields is the reason for which I would prefer Aut.

[Antoine Chambert-Loir]

(If the two notations coexist, one will probably have to rewrite one into the other occasionally.)

[Yaël Dillies]

"rewrite"? This is just notation

[Antoine Chambert-Loir]

OK then.

[Andrew Yang]

The proposal is #30266

[Riccardo Brasca]

Is it possible to have a linter checking this is used only for fields? @Damiano Testa

[Andrew Yang]

I think it is possible to tweak the elaborator to make Gal(S/R) not parse if we want to.

[Jireh Loreaux]

But then it wouldn't be notation, right (i.e., it's not a macro)? Instead it's an elab.

[Kenny Lau]

/poll when should we use the notation Gal(L/K)?
for any rings
for any fields
for any fields with IsGalois

[Andrew Yang]

I think it can still be a macro_rules. But is this an important difference? I don't really know here.

[Jireh Loreaux]

I could be wrong as I'm not an expert here, but I think it can't be a macro_rules because that's still has type Syntax → Syntax, so you're in the wrong monad for elaboration.

[Kenny Lau]

but what difference does this make? i don't see why this is a point for or against the extra elaboration rule

[Andrew Yang]

Yes you are right. macro_rules only allows MacroM which couldn't really do anything. But I'm not sure what the downsides of elab are.

[Kenny Lau]

are we discussing implementation detail here?

[Jireh Loreaux]

Andrew Yang said:

Yes you are right. macro_rules only allows MacroM which couldn't really do anything. But I'm not sure what the downsides of elab are.

maybe nothing, but I thought I would point it out since we were discussing this in the context of notation. The other example I can think of off the top of my head where we do elaboration when parsing the syntax is the Finset notations. This causes some headaches (because you have to decide whether to parse as a Set or a Finset).

[Damiano Testa]

A linter should definitely be able to check whether the arguments to Gal(L|K) are fields. However, if this is what it is desired, why not make already the notation use a definition that has the Field typeclasses present?

[Jireh Loreaux]

Because then you need a separate declaration?

[Aaron Liu]

Then you would have to convert between the new definition and the algequiv

[Damiano Testa]

Ok, so it is possible, but it does require to extract the appropriate instances, since sometimes I imagine that some of these fields are going to be quotients of rings by maximal ideals, and the Field instance will not be explicitly present.

[Kenny Lau]

it will use synthInstance

[Damiano Testa]

Right, but you need to recreate the appropriate context for that to be able to synthesize the instance.

[Andrew Yang]

I guess Damiano's question is whether we should allow

[q.IsMaximal] [p.IsMaximal] : Gal(S ⧸ q / R ⧸ p)

when docs#Ideal.Quotient.field is turned off.

[Damiano Testa]

Yes, I think that naïvely checking that the instances are present as Field F is easy, but will not be what is expected.

[Kenny Lau]

well when it is turned off then they are not fields so we shouldn't use that notation

[Riccardo Brasca]

I think in this case one can just an exception to the linter, as maybe p is prime that in practice is always maximal, but in mathlib we allow p=0 simply because the theorem is still true, even if nobody cares about that case.

[Riccardo Brasca]

similarly, maybe you don't turn the quotient into a field because you don't need it, but morally it is a field

[Kevin Buzzard]

We could make IsField into a class? But presumably there's good reasons for not doing this (because it's not currently)?

[Anne Baanen]

I assume IsField is not a class in order to clearly distinguish with our actual Field class. (And I have encountered IsField more commonly in the form ¬ (IsField R), for which being a class does not help much.)

[Filippo A. E. Nuccio]

Andrew Yang said:

I don't understand Filippo's first point but I totally agree with the second being potentially a problem. This is why I have been pushing us to have a discussion on when this notation is appropriate. For example Gal(ℚ|ℤ) definitely should not appear.

Just to answer Andrew: what I meant is that Gal(L/K) just means Hom_K(L, L) when

• K, L are fields; and
• L/K is normal

This seems pretty much to me as "V is a K-vector space" just means "V is a K-module" when K is a field. In both cases the notation does not contain more information (i. e.: its elements are not a subtype of some more general type), and it seems to me to be more mathlib-ish (and nicer, at the end) to avoid introducing these kind of abreviations just to align with "usual" math jargon.

[Andrew Yang]

I understand your point now and I agree there is a tradeoff being made. To me, readability of a syntax means how much cognitive load would be required to know both what it means mathematically and what it will be parsed into as a Expr tree. I agree that this notation make it harder to know that it is merely a AlgEquiv under the hood, but the benefit on the other side is way larger to me in this case. To see <a long terms> ≃ₐ[K] <another long term> and to parse this as a "galois group", one would need to meticulously check if the two long terms are equal and this has a huge cognitive cost to me.

On the other hand it is extremely easy to see Module and parse it as "vector space" mathematically.

[Damiano Testa]

Having thought a little bit more about this, I am not sure that I am completely onboard that, if Gal is used, that it should require its arguments to be fields.

In the Galois group/deck transformation analogy, I consider it to be pretty standard to talk about the equivalence between "the group of deck transformations acts transitively on the fibers" and "the total space is connected". From the perspective of Galois groups, only allowing fields means that you only always have transitive actions.

[Damiano Testa]

In concrete terms, I would not find it particularly strange to say that the Galois group of $\mathbb{Q} \oplus \mathbb{Q}$ is trivial.

[Kevin Buzzard]

It's not -- you can switch the factors!

[Filippo A. E. Nuccio]

Damiano Testa said:

In concrete terms, I would not find it particularly strange to say that the Galois group of $\mathbb{Q} \oplus \mathbb{Q}$ is trivial.

Well, but this goes against the goal of making all-other-mathematicians-out-there's life simple. Because the situation, now, is that we have things of the form $\mathbb{Q}(i)\cong_{a}[\mathbb{Q}]\mathbb{Q}(i)$ (and hovering over the $\cong_{a}$ tells you these are algebra homomorphisms); while in your setting we'd have $\mathrm{Gal}(\mathbb{C}(X)/\mathbb{C})$ and people might wonder what this beast is. Given the abundance of junk values all over Mathlib, if someone has finally learnt that $7/0=0$ and ζ(1)=1/2 (γ − log 4π) they might equally well believe that $\mathrm{Gal}(\mathbb{C}(X)/\mathbb{C})=\{1\}$ or $\mathrm{Gal}(\mathbb{C}(X)/\mathbb{C})=\mathfrak{S}_{37}$.

[Christian Merten]

You could make it so that hovering over $\mathrm{Gal}(L/K)$ shows that it is algebra isomorphisms.

[Filippo A. E. Nuccio]

That's true.

[Kenny Lau]

but Gal(C(X)/C) is clearly PGL(2,C)

[Kevin Buzzard]

This is true in the sense of differential Galois theory (edit: this might actually be false because those Galois groups I think have to preserve d?)

[Andrew Yang]

I am resurfacing this discussion because the PR #30266 is slightly prone to rot.
To reiterate, the current proposal is that

1. Gal(L/K) always elaborates to L ≃ₐ[K] L (with the hover saying that it is AlgEquiv under the hood)
2. L ≃ₐ[K] L delaborates to Gal(L/K) when Field L and Field K could be synthesized.
3. We only allow the usage of Gal(L/K) in mathlib when we are actually considering them as (not necessarily galois) field extensions, but there are no guardrails and it is up to the reviewers to uphold this.

[Riccardo Brasca]

LGTM, I guess the only question is if we want IsGalois K L in 2

[Adam Topaz]

I'm personally not convinced that the Gal notation should be reserved for fields. I would like to be able to (eventually) write $Gal(X/Y)$ when $X \to Y$ is a Galois etale cover of schemes, for example. Or $Gal(L|K)$ when $L|K$ is a Picard-Vessiot extension of differential fields (in which case Gal might have additional structure). Or in any other context where we have "a Galois theory".

[Adam Topaz]

There is a small annoyance that in field theory we take $L|K$ to be an extension of fields to mean that there is a map $K \to L$ satisfying an assumption, but in topological/geometric contexts the map is in the reverse direction (i.e. a cover as opposed to an extension). On paper we would still write Gal in both contexts.

[Thomas Murrills]

@Adam Topaz, just to clarify, are you okay with merging this PR (which checks for field instances), but would just like to see it potentially generalized in the future?

I just want to make sure I don't ignore your comment by recommending a merge of the current design after review (where we check for field instances during delaboration). :)

[Adam Topaz]

Yes, I’m happy for the PR to get merged if there is a general consensus. We can always generalize later when there is a reason to do so.

[Filippo A. E. Nuccio]

I am slightly sceptical regarding the approach of merging this PR after the poll
#mathlib4 > Notation for Galois group @ 💬
where the outcome was not very clear (and the option "only for Galois extensions" got 0 votes).

[Thomas Murrills]

Ah, perhaps I was a bit too hasty to recommend a merge? I apologize; my impression was that there was general consensus at this point in the thread, and that the poll was too early in the thread for it to be reflective of opinions post-discussion.

This notation will continue to evolve and change, though, so please don’t let the merging of this PR stifle discussion on changes you’d like to see to it (or whether we use it)! :)

[Kenny Lau]

in lemma names do we spell it as gal or as algEquiv?

[Damiano Testa]

This lends itself to an amusing galEquiv misspelling.

[Andrew Yang]

I personally think we should still name it algEquiv since our consensus seems to be to treat it as merely a notation and to not forget that it is L ≃ₐ[K] L under the hood.

[Kenny Lau]

I personally think that since we've introduced Gal and we write Gal and it prints back to Gal then we should have gal in the names

[Kevin Buzzard]

This is in the context of #30738 and given that there will be many misnamed lemmas in mathlib if we go for gal as the name, I think that this is not your problem in the PR and you should just use algEquiv

[Scott Carnahan]

At some point, perhaps far in the future, I would like to see Galois groups incorporate base change, so we would have Gal_A^B(R) for R an A-algebra meaning R-algebra automorphisms of B \otimes_A R. This would let us describe properties of extensions more geometrically, e.g., IsGalois means a constant sheaf, inseparable field extensions have nonreduced Galois groups, something about generic fibers for ramification.