Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Global.MaximalEverywhereUnramifiedProPFiniteGeneration

Module documentation

Finite generation of the maximal everywhere-unramified pro-p Galois group

The power--commutator quotient of the maximal everywhere-unramified pro-p Galois group is the finite Galois group of the elementary Hilbert layer. A finite set of lifts of that quotient topologically generates the full group.

theorem

maxEverywhereUnramifiedProPGaloisGroup_topologicallyFinitelyGenerated

L35 ↗

ClassFieldTower.Martinet.maxEverywhereUnramifiedProPGaloisGroup_topologicallyFinitelyGenerated

Documentation

For odd p, the maximal everywhere-unramified pro-p Galois group is topologically finitely generated.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField IsMulCommutative
noncomputable section
open Set
open GlobalClassFieldTheory GlobalClassFieldTheory.GlobalClassFields
namespace ClassFieldTower.Martinet
open ClassFieldTower.ProP
open ProCGroups.Generation
open ProCGroups.FiniteGeneration
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]

Lean source · statement

theorem maxEverywhereUnramifiedProPGaloisGroup_topologicallyFinitelyGenerated
    (hpOdd : Odd p) :
    TopologicallyFinitelyGenerated
      (MaxEverywhereUnramifiedProPGaloisGroup F p)

Module documentation

Finite generation of the maximal everywhere-unramified pro-p Galois group

Declarations

maxEverywhereUnramifiedProPGaloisGroup_topologicallyFinitelyGenerated