Module

MaximalEverywhereUnramifiedProPGroup.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Global.MaximalEverywhereUnramifiedProPGroup

2 declarations indexed from sourceView source ↗

Module documentation

The maximal everywhere-unramified pro-p Galois group

For odd p, every open normal quotient of the Galois group of the maximal compositum is a finite p-group. The corresponding fixed field is finite Galois, hence lies in one bundled finite p-extension by cofinality; restriction from that extension supplies the required quotient p-group structure.

Imports4

Imported by3

def

normalAutEquivQuotientWithNormal

L30 ↗

ClassFieldTower.Martinet.normalAutEquivQuotientWithNormal

Documentation

The fixed-field quotient equivalence with a named normality argument.

Source context 4 commands

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

open scoped NumberField
noncomputable section
universe u
namespace ClassFieldTower.Martinet

Lean source · statement

def normalAutEquivQuotientWithNormal
    {k K : Type u} [Field k] [Field K] [Algebra k K] [IsGalois k K]
    (H : ClosedSubgroup (K ≃ₐ[k] K)) [hNormal : H.toSubgroup.Normal] :
    ((K ≃ₐ[k] K) ⧸ H.toSubgroup) ≃*
      (IntermediateField.fixedField H.toSubgroup ≃ₐ[k]
        IntermediateField.fixedField H.toSubgroup)

theorem

maxEverywhereUnramifiedProPGaloisGroup_hasPGroupOpenNormalBasis

L40 ↗

ClassFieldTower.Martinet.maxEverywhereUnramifiedProPGaloisGroup_hasPGroupOpenNormalBasis