Module

GlobalMaximalAbelianRestriction.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Global.GlobalMaximalAbelianRestriction

3 declarations indexed from sourceView source ↗

Module documentation

Restriction to the actual maximal abelian subextension

Imports2

Imported by5

def

globalMaximalAbelianRestriction

L20 ↗

ClassFieldTower.Martinet.Shafarevich.globalMaximalAbelianRestriction

Documentation

Restrict the standard absolute Galois group to the maximal abelian subextension of the fixed separable closure.

Source context 3 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
variable (F : Type) [Field F]

Lean source · statement

def globalMaximalAbelianRestriction :
    Field.absoluteGaloisGroup F →ₜ* Gal(_root_.maximalAbelianExtension F / F)

theorem

globalMaximalAbelianRestriction_apply

L30 ↗

ClassFieldTower.Martinet.Shafarevich.globalMaximalAbelianRestriction_apply

Source context 3 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
variable (F : Type) [Field F]

Lean source · statement

theorem globalMaximalAbelianRestriction_apply (sigma : Field.absoluteGaloisGroup F) :
    globalMaximalAbelianRestriction F sigma =
      AlgEquiv.restrictNormalHom (_root_.maximalAbelianExtension F)
        (RamificationTheory.Field.absoluteGaloisGroup.separableClosureContinuousMulEquiv F sigma)

theorem

globalMaximalAbelianRestriction_surjective

L37 ↗

ClassFieldTower.Martinet.Shafarevich.globalMaximalAbelianRestriction_surjective

Documentation

Absolute automorphisms surject onto the maximal abelian Galois group.

Source context 3 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
variable (F : Type) [Field F]

Lean source · statement

theorem globalMaximalAbelianRestriction_surjective :
    Function.Surjective (globalMaximalAbelianRestriction F)

Module documentation

Restriction to the actual maximal abelian subextension

Declarations

globalMaximalAbelianRestriction

globalMaximalAbelianRestriction_apply

globalMaximalAbelianRestriction_surjective