Module

MaximalRealProPGroup.lean

Nyll.SawinTotallyRealTowers.MaximalRealProPGroup

2 declarations indexed from sourceView source ↗

Module documentation

The Galois group of the maximal real pro-p compositum

Every finite normal subextension of the constructed compositum is contained in an admissible finite layer. Restriction therefore makes its Galois group a quotient of a p-group. Applying this to fixed fields of open normal subgroups gives a basis of open normal subgroups with finite p-group quotients. The argument applies to p = 2 as well as odd primes.

Imports6

Nyll.SawinTotallyRealTowers.FiniteRealPExtensionSupport
Nyll.SawinTotallyRealTowers.MaximalRealProPOutside
Nyll.ProCGroups.ProC.InverseLimits.Predicates
Nyll.ProCGroups.Profinite.OpenSubgroups
Mathlib.FieldTheory.Galois.Infinite
Mathlib.FieldTheory.Galois.Profinite

Imported by8

theorem

isPGroup_galois_of_le_maximalRealProPOutside

L33 ↗

ClassFieldTower.Sawin.isPGroup_galois_of_le_maximalRealProPOutside

Documentation

A finite normal subextension of the maximal real compositum has a p-group Galois group, by restriction from one admissible finite layer.

Source context 4 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Sawin

Lean source · statement

theorem isPGroup_galois_of_le_maximalRealProPOutside
    (p : ℕ) (T : Set (HeightOneSpectrum (𝓞 ℚ)))
    (L : IntermediateField ℚ (AlgebraicClosure ℚ))
    [FiniteDimensional ℚ L] [Normal ℚ L]
    (hL : L ≤ maximalRealProPOutside p T) :
    IsPGroup p (L ≃ₐ[ℚ] L)

theorem

maximalRealProPOutside_galoisGroup_hasPGroupOpenNormalBasis

L51 ↗

ClassFieldTower.Sawin.maximalRealProPOutside_galoisGroup_hasPGroupOpenNormalBasis