Refactor `krullTopology`?

Stream: maths

[Jz Pan]

:cross_mark::cross_mark::cross_mark: Seems that we should redefine krullTopology, which should not only on L ≃ₐ[K] L, but should be a GroupFilterBasis.topology on any group G by declaring all the normal subgroups of finite index be the neighborhood basis of 1. :cross_mark::cross_mark::cross_mark:

[EDIT] Oops this is not correct, for example, the Galois group of compositum of all quadratic fields of Q over Q has a proper (hence has an index 2 normal) subgroup whose fixing field is Q :exploding_head:

And maybe we can prove that under some suitable conditions it is compact.

[Jz Pan]

Here we go:

import Mathlib.GroupTheory.Index
import Mathlib.Topology.Algebra.FilterBasis

universe u

variable (G : Type u) [Group G]

/-- The profinite neighborhood basis for a group, which consists of all normal subgroups of
finite index. -/
def GroupFilterBasis.profinite : GroupFilterBasis G where
  sets := { S : Set G | ∃ H : Subgroup G, H.Normal ∧ H.index ≠ 0 ∧ S = H }
  nonempty := ⟨⊤, ⟨⊤, inferInstance, by simp, rfl⟩⟩
  inter_sets {S} {T} := by
    rintro ⟨H, h1, h2, rfl⟩ ⟨K, h3, h4, rfl⟩
    exact ⟨H ⊓ K, ⟨H ⊓ K, inferInstance, Subgroup.index_inf_ne_zero h2 h4, rfl⟩, by simp⟩
  one' {S} := by
    rintro ⟨H, h1, h2, rfl⟩
    exact one_mem H
  mul' {S} := by
    rintro ⟨H, h1, h2, rfl⟩
    exact ⟨H, ⟨H, h1, h2, rfl⟩, by simp⟩
  inv' {S} := by
    rintro ⟨H, h1, h2, rfl⟩
    exact ⟨H, ⟨H, h1, h2, rfl⟩, by simp⟩
  conj' x {S} := by
    rintro ⟨H, h1, h2, rfl⟩
    exact ⟨H, ⟨H, h1, h2, rfl⟩, fun y hy ↦ by simp [h1.conj_mem y hy x]⟩

[Jz Pan]

And this:

def GroupFilterBasis.proP (p : ℕ) : GroupFilterBasis G where
  sets := { S : Set G | ∃ (H : Subgroup G) (m : ℕ),
    H.Normal ∧ H.index ≠ 0 ∧ H.index = p ^ m ∧ S = H }
  nonempty := ⟨⊤, ⟨⊤, 0, inferInstance, by simp, by simp, rfl⟩⟩
  inter_sets {S} {T} := by
    rintro ⟨H, m, h1, h2, h3, rfl⟩ ⟨K, n, h4, h5, h6, rfl⟩
    -- I suspect this is incorrect, we need some more assumptions
    sorry
  one' {S} := by
    rintro ⟨H, m, h1, h2, h3, rfl⟩
    exact one_mem H
  mul' {S} := by
    rintro ⟨H, m, h1, h2, h3, rfl⟩
    exact ⟨H, ⟨H, m, h1, h2, h3, rfl⟩, by simp⟩
  inv' {S} := by
    rintro ⟨H, m, h1, h2, h3, rfl⟩
    exact ⟨H, ⟨H, m, h1, h2, h3, rfl⟩, by simp⟩
  conj' x {S} := by
    rintro ⟨H, m, h1, h2, h3, rfl⟩
    exact ⟨H, ⟨H, m, h1, h2, h3, rfl⟩, fun y hy ↦ by simp [h1.conj_mem y hy x]⟩

[Jz Pan]

The condition H.index ≠ 0 in proP is to prevent someone who wants to define pro-0 topology :joy:

[Junyan Xu]

Jz Pan said:

Seems that we should redefine krullTopology, which should not only on L ≃ₐ[K] L, but should be a GroupFilterBasis.topology on any group G by declaring all the normal subgroups of finite index be the neighborhood basis of 1.

Not all finite index subgroups (e.g. of the absolute Galois group of $\mathbb{Q}$) are open: https://mathoverflow.net/questions/82177/a-profinite-group-which-is-not-its-own-profinite-completion

[Adam Topaz]

There is a famous theorem saying this is true for topologically finitely generated profinite groups

[Adam Topaz]

https://annals.math.princeton.edu/2007/165-1/p05

[Kevin Buzzard]

Conversely, for an infinite product $\prod_i\Z/2\Z$ it's pretty clear that there will be finite index subgroups that aren't open. Open subgroups are closed so it suffices to find a finite index subgroup that isn't closed. Thinking of everything as a vector space over $\Z/2\Z$ we just need to find a non-closed subspace of finite index, so we start with the dense subspace $\oplus_i\Z/2\Z$ (whose closure is already the whole thing), extend a basis of this to a basis for the full space and then throw away one of the new basis elements. To see this group showing up in Galois theory you can use the extension $\mathbb{Q}(\sqrt2,\sqrt3,\sqrt5,\ldots,\sqrt{p},\ldots)$. A Galois element being in the direct sum means that it fixes all $\sqrt{p}$, where the product is indexed by the primes.

[Junyan Xu]

I have recently written a proof that the prime (or maximal) spectrum of an infinite product of nontrivial comm. semirings have more points than the disjoint union of the spectra of the individual semirings, and it's similarly by considering the ideal of finitely supported elements in the product.

Now this argument seems to show a topologically non-f.g. profinite group G should be expected to contain finite-index subgroups that are not open, so G is properly contained in its profinite completion, and the completion should still be topologically non-f.g. So it seems we can continue doing profinite completion and it never terminates; is that really the case?

[Adam Topaz]

I can think of a proof for pro-p groups essentially using Kevin’s argument above.

[Adam Topaz]

Namely, if you take a pro-p group G and mod out by the p-th powers and commutators, you get something isomorphic to a product of Z/p indexed by the dimension of H1 with Z/p coeffs, which is the minimal number of generators. Now you can proceed with what Kevin does above.

[Adam Topaz]

I’m not sure about arbitrary profinite groups, but it’s possible Nikolov-Segal mention something in the paper I linked above

[Adam Topaz]

I guess a similar proof would work for pro-nilpotent profinite groups?

[Kevin Buzzard]

It would not surprise me at all that the completion process went on forever. This is exactly what happens for local rings too. The completion of a local ring is not in general complete. More precisely, if R is local with max ideal m then the m-adic completion of R will be local, and complete with respect to the (ideal generated by image of m)-adic topology, but if m is not finitely generated then it can happen (and indeed might always happen? I think Lenstra told this in the 90s?) that the ideal generated by the image of this maximal ideal is not the maximal ideal of the completion (for the same sort of silly reasons as above). So if we say a local ring is complete if it's complete wrt the maximal ideal-adic topology then the completion of a local ring might not be complete and I think that in the non-Noeth case you basically always get an infinite tower if you continue completing.

[Jz Pan]

Kevin Buzzard said:

if R is local with max ideal m then the m-adic completion of R will be local, and complete with respect to the (ideal generated by image of m)-adic topology, but if m is not finitely generated then it can happen (and indeed might always happen? I think Lenstra told this in the 90s?) that the ideal generated by the image of this maximal ideal is not the maximal ideal of the completion (for the same sort of silly reasons as above).

I'm thinking m^2=m case, e.g. $R=\mathcal{O}_{\mathbb{C}_p}$.

Oh by the way, do we have almost mathematics in mathlib? Which concerns exactly for m^2=m case. Do perfectoid field, perfectoid ring and perfectoid spaces merged to mathlib? And do we have tilting equivalence in Scholze's 2012 paper formalized in Lean? I think we only have definition of perfectoid spaces (but not any important results) formalized in Lean 3 and then it got abandoned.

[Kevin Buzzard]

Aah yes, that example indicates that some of what I've said must be wrong, because there the image of the maximal ideal is the maximal ideal, so you complete once and then you stabilise. No, we have very little almost mathematics. We don't have anything like the tilting equivalence.

[Christian Merten]

Jz Pan said:

Oh by the way, do we have almost mathematics in mathlib? Which concerns exactly for m^2=m case. Do perfectoid field, perfectoid ring and perfectoid spaces merged to mathlib? And do we have tilting equivalence in Scholze's 2012 paper formalized in Lean?

cc @Jiang Jiedong

[Jiang Jiedong]

The Scholze’s 2012 paper is still too far away, since it requires too much framework of adic spaces. But I am currently working on the formalization of very basic almost mathematics and a pure field version of tilting equivalence.

[Jiang Jiedong]

For the current status:

1. The definition of tilting functor (on the level of rings) is in Mathlib with only very basic properties.
2. There is no almost mathematics in Mathlib. And the Scholze’s paper uses a different approach to almost mathematics comparing with Gabber-Romero’s book. In the paper, everything is more concrete and less general than in the book.

[Jiang Jiedong]

And I believe the definition of perfectoid ring and perfectoid field will be merged into mathlib in the near future. It is almost done on a local branch on my computer.

[Filippo A. E. Nuccio]

That this version is almost done on a local branch is pure beauty.

[Filippo A. E. Nuccio]

A pity that it is not almost complete on your local branch...