Global Class Field Theory

Stream: new members

[Dean Young]

Local Class Field Theory has been done here. Is there any work in progress on global class field theory?

[Adam Topaz]

I'm quite sure that local class field theory is not "done" (and probably quite far from it). @Filippo A. E. Nuccio @María Inés de Frutos Fernández . There has been some discussions about stating the theorems from global class field theory elsewhere in this zulip server. Note that even writing down the statements is a very nontrivial task!

[Dean Young]

@María Inés de Frutos Fernández @Filippo A. E. Nuccio will you be making a global class field theory repository? If so I would be very excited to contribute.

[Kevin Buzzard]

Global class field theory is a neccessary prerequisite for FLT so we'll have to do it at some point. Right now some examples of things needed are: Kummer theory, Galois cohomology, and statements (not proofs!) of local and global duality theorems.

AFAIK there is nobody working on Kummer theory (people at Imperial are thinking about the other things).

[Dean Young]

@Kevin Buzzard Would it be possible to start a repo for this, keeping it fairly light for now?

Here is one thing that could be interesting to keep parallel between the local and global developments (and which is related to the theorem that the Adeles are the tensor product of ℤ̂ and ℚ):

𝖶e first form the complete monoidal small category Λ by adding in a terminal and initial objects ∞ and -∞, to the category ℤ whose objects are integers and where Hom n m is a singleton if n ≤ m and empty otherwise. We get ∀(n:ℤ),(-∞ ≤ n) ∧ (n ≤ ∞), and a monoidal structure + in which -∞ * n = - ∞ for each integer.

Theorem: Let A be a commutative unitial ring. There is a correspondence between

(1) Functors Φ : A-mod ⟶ such that
(a) There is Ψ : {-∞}∪ℤ∪{∞} ⟶ A-mod) and p:Φ⊣Ψ
(b) Φ is strong (only Φ(X⊗Y)≅Φ(X)⊗Φ(Y) is needed)

(2) Functions φ : A → {-∞}∪ℤ∪{∞} such that
(a) φ(x+ y) ≤ φ(x) + φ(y) for each x, y in A
(b) φ(xy) = φ(x)φ(y) for each x, y in A
(c) φ(1) = 0
(d) φ(0) = -∞

In this way one can understand norms and ring homomorphisms as being unified in the setup of Tannakian formalism (or complete monoidal closed categories).

[Riccardo Brasca]

A bit of kummer theory is already in mathlib. And we have stuff in the flt-regular. @Andrew Yang knows the all story

[Ruben Van de Velde]

Would be nice to have some kind of roadmap

[Adam Topaz]

"Kummer Theory" is a very overloaded term!

[Kevin Buzzard]

Why start a repo? Just start PRing to mathlib.

[Dean Young]

Just out of curiosity, are the contents of the local repo not PRd as of yet?

[Andrew Yang]

All we have at flt-regular is in file#FieldTheory/KummerExtension already. Basically the statement cyclic <=> splitting field of some irreducible $X^n - a$

[Kevin Buzzard]

Actually maybe this is all I need

[Riccardo Brasca]

We also have the usual form of hilbert 90 (with units and norm) and the somehow more exotic hilbert 92 and 94