Adeles, ideles and class field theory

Places, adeles and ideles, Arakelov divisors, ray class groups, Artin map, Hilbert class fields, Neukirch–Uchida-type Galois characterization.

• Adeles and ideles
• Arakelov divisors
• Hilbert class field
• Places and completions of the rationals
• Places of a number field
• Ray class groups
• Artin map
• Congruence subgroups for a modulus
• Ray class characters

TheoremNeukirch–Uchida theorem#●ready to prove

Let \(K_1\) and \(K_2\) be number fields with separable closures \(\overline{K_1}\) and \(\overline{K_2}\), and let \(\varphi \colon \mathrm{Gal}(\overline{K_1}/K_1) \to \mathrm{Gal}(\overline{K_2}/K_2)\) be a group isomorphism that is a homeomorphism for the Krull topologies. Then there is a unique field isomorphism \(\sigma \colon \overline{K_2} \to \overline{K_1}\) that maps the image of \(K_2\) in \(\overline{K_2}\) onto the image of \(K_1\) in \(\overline{K_1}\) and satisfies \(\varphi(g) = \sigma^{-1} \circ g \circ \sigma\) for every \(g \in \mathrm{Gal}(\overline{K_1}/K_1)\).

public theorem_wanted neukirch_uchida {K₁ K₂ K₁' K₂' : Type*} [Field K₁] [Field K₂] [Field K₁'] [Field K₂']
    [NumberField K₁] [NumberField K₂] [Algebra K₁ K₁'] [Algebra K₂ K₂'] [IsSepClosure K₁ K₁']
    [IsSepClosure K₂ K₂'] (ϕ : Gal(K₁'/K₁) ≃* Gal(K₂'/K₂)) (he : IsHomeomorph ϕ) :
    ∃! σ : K₂' ≃+* K₁', (algebraMap K₂ K₂').range.map σ.toRingHom = (algebraMap K₁ K₁').range ∧
      ∀ g : Gal(K₁'/K₁), ϕ g = σ.trans (g.toRingEquiv.trans σ.symm)

Sources

• Jürgen Neukirch, Alexander Schmidt, Kay Wingberg. Cohomology of Number Fields, Theorem 12.2.1. Problem neukirch_uchida of the lean-eval benchmark.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.