Krull topology on Galois groups

Stream: maths

[Adam Topaz]

I just noticed that @Sebastian Monnet 's PR on the Krull topology for Galois groups was merged! This is a great result!

If I understand correctly, this definition defines the topology on $Gal(L|K)$ for arbitrary extensions $L|K$ by specifying that the nhds of the identity should be $Gal(L|E)$ where $E$ varies over the subextensions of $L|K$ which are finite over $K$. Is that right?
If so, I wonder why this was chosen as opposed to using finitely generated extensions over $K$.

[Adam Topaz]

Let me also ping the usual suspects @Kevin Buzzard @Johan Commelin

[Riccardo Brasca]

For example what happens in the very simple case of $\mathbb{C}(X)/\mathbb{R}$? Let me think

[Adam Topaz]

Even better: $\mathbb{C}(X)|\mathbb{C}$

[Filippo A. E. Nuccio]

(deleted)

[Riccardo Brasca]

I wanted to add a (tiny) algebraic extension just to see what happens

[Filippo A. E. Nuccio]

AH no, I see now what you are speaking about.

[Riccardo Brasca]

The group is the Cremona group, right?

[Adam Topaz]

Maybe I should clarify that the topology has been defined for arbitrary extensions $L|K$. In the algebraic case, it doesn't matter because f.g. and finite are equivalent

[Adam Topaz]

Riccardo Brasca said:

The group is the Cremona group, right?

Yeah, exactly. I suppose there is a natural topology on the Cremona group?

[Riccardo Brasca]

Well, in this case it's just PGL

[Adam Topaz]

Okay, but maybe we should consider $k(X)|k$ for arbitrary algebraically closed $k$..

[Adam Topaz]

We could put the algebraic topology on this.

[Riccardo Brasca]

Yes, sure, I wasn't proposing to get the complex topology

[Adam Topaz]

https://annals.math.princeton.edu/wp-content/uploads/annals-v178-n3-p08-p.pdf

[Riccardo Brasca]

In any case the point of the Krull topology is that Galois theory works if we consider intermediate extension and closed subgroups.

[Riccardo Brasca]

Transcendental Galois theory is a thing, right?

[Adam Topaz]

Riccardo Brasca said:

Transcendental Galois theory is a thing, right?

Yes, but it's of a different flavor, I think.

[Riccardo Brasca]

In any case for $\mathbb{C}(x)/\mathbb{C}$ we get the trivial topology, that suggests the definition is really for algebraic extensions.

[Adam Topaz]

http://alpha.math.uga.edu/~pete/transgal.pdf

[Adam Topaz]

It seems to me that using f.g. extensions should correspond to the so-called $\mathcal{J}$-topology in this paper.

[Adam Topaz]

And if you look at lemma 47 on page 22, that suggests (at least in my opinion) that this is the right topology.

[Kevin Buzzard]

I proposed the definition to Sebastian Monnet. It sort of came about for the following reason: I told him to topologise Galois groups of algebraic extensions because Maria needed it to state the main theorem of global class field theory in Lean , and I suggested that he show that Gal(L/E) were a group_filter_basis for Gal(L/K) as E/K ranged over finite extensions. He did this, but he never put the assumptions of algebraic normal and separable on the extension, because he was just waiting for the theory to demand them. And then a couple of weeks later he got back to me saying that the definition had worked and that he'd never needed to use any of algebraic, normal or separable! So it was kind of an accident that these things ended up as the topology.

[Kevin Buzzard]

Sebastian has also proved, IIRC, that in the case where the extension is algebraic and normal (he never needed separability IIRC) that the topology is profinite.

[Riccardo Brasca]

In any case theorem 46 says that the Galois correspondence will work only for algebraic extensions

[Adam Topaz]

Kevin Buzzard said:

... Maria needed it to state the main theorem of global class field theory in Lean ,...

Amazing!

[Kevin Buzzard]

yeah we've been having some fun at Imperial ;-) I have moved my attention from undergraduates to PhD students...

[Adam Topaz]

Did you and/or Maria do LCFT too?

[Kevin Buzzard]

I don't think we have an adequate definition of local fields yet. Me? Me, I don't do anything! I would love to be writing hard Lean code e.g. helping you with LTE instead of just watching and being impressed. I now seem to have moved into management :-(

[Adam Topaz]

Kevin Buzzard said:

I don't think we have an adequate definition of local fields yet.

This should be reasonably low hanging fruit IMO.

[Kevin Buzzard]

The literature is quite flexible about what is allowed. Are the reals a local field? Is a power series ring over an infinite field a local field? Should we just say "finite extension of Q_p or Z/pZ((t))" or should we give some more abstract definition e.g. field of fractions of a complete DVR with finite residue field? (is that right?)

[Adam Topaz]

Just do whatever Serre says (<-- general philosophy for life)

[Kevin Buzzard]

Now you come to mention it. I don't know why I suggested to poor Maria to do global CFT -- local was probably a far easier problem!

[Kevin Buzzard]

One question that came up at Imperial was how far one could get towards the proof of the Mordell-Weil theorem without proving that the addition on an elliptic curve was associative ;-) (because right now we're blocked by this to a certain extent, but people are just assuming it and moving on)

[Kevin Buzzard]

Anyway, back to the original question, if you're saying that we should be ranging over the f.g. extensions in general then this might be a nice refactor for someone -- a good first project? Hopefully it won't go the same way as Pierre-Alexandre Bazin's good first project: he's an MSc student visiting Imperial for 4 months and was working on #11472 but now tells me that he has a counterexample to the claim on Wikipedia that it's a distributive lattice!

[Riccardo Brasca]

Well, if they discover that something believed true is actually false it would be a fantastic first project!

[Adam Topaz]

I don't know whether the change to f.g. is actually worth it. The reasons I see to do this change as now twofold:

1. by using f.g. extensions, the construction can be generalized. For example, if we have some algebraic structure $X$ and a substructure $B$, we can define a topology on $Aut(X|B)$ by taking a basis for the nhds of the identity to fix some finite subset $S$ of $X$ pointwise, and let $S$ vary. By using finite extensions we are restricting ourselves to, essentially, fields (maybe rings).
2. That paper by Pete Clark suggests that the topology with f.g. extensions is actually useful for something...

[Adam Topaz]

OTOH, if the only case we really care about is where $L|K$ is algebraic, then one could argue that it doesn't really matter.

[Junyan Xu]

we can define a topology on Aut(X∣B) by taking a basis for the nhds of the identity to fix some finite subset S of X pointwise, and let SSS vary

It's the same as the topology generated by point stabilizers, which is a simpler definition. We then know that the finite intersections serve as a basis.

[Adam Topaz]

Yeah, thats how that paper defined the so-called J-topology, IIRC.

[Kevin Buzzard]

It's not the topology generated by the point stabilisers as this isn't a group topology. And there was an extensive discussion about "the group topology generated by..." here earlier and the conclusion was that this notion is less well behaved than you might expect. However this problem can be solved using the notion of a group filter basis. I'm just noting that this whole thing is slightly more subtle than you might think. This is the issue that Monnet solved.

[Adam Topaz]

Oh, what I had in mind is, more precisely, to take the coarsest group topology for which those stabilizers are neighborhoods of the identity. Is that not the right thing?

[Kevin Buzzard]

It is the right thing, but the problem with this definition is that (perhaps surprisingly) "coarsest group topology such that..." is difficult to prove things about.

[Adam Topaz]

Ah I see.

[Kevin Buzzard]

If I weren't on mobile I'd dig up the thread.

[Kevin Buzzard]

Group filter bases solve all this.

[María Inés de Frutos Fernández]

I think this is the thread: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Trying.20to.20prove.20a.20lemma.20about.20group.20topologies