Module

AbsoluteDiscreteKernelField.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Kummer.AbsoluteDiscreteKernelField

8 declarations indexed from sourceView source ↗

Module documentation

The finite Galois field detected by a discrete absolute representation

Continuity gives an open normal kernel. Its actual fixed field is finite Galois, and its Galois group embeds in the target through the quotient by that kernel. In particular a p-group target produces a p-extension; the target itself need not be finite. No new instances are installed.

Imports3

Imported by4

def

absoluteDiscreteKernelOpenNormal

L30 ↗

ClassFieldTower.Martinet.Shafarevich.absoluteDiscreteKernelOpenNormal

Documentation

The open normal kernel, on the literal algebraic-closure automorphism group.

Source context 5 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open RamificationTheory.Field.absoluteGaloisGroup
variable (F : Type) [Field F] [NumberField F]
variable {Q : Type*} [Group Q] [TopologicalSpace Q] [DiscreteTopology Q]

Lean source · statement

def absoluteDiscreteKernelOpenNormal (s : Field.absoluteGaloisGroup F →ₜ* Q) :
    OpenNormalSubgroup Gal(AlgebraicClosure F/F)

abbrev

absoluteDiscreteKernelField

L40 ↗

ClassFieldTower.Martinet.Shafarevich.absoluteDiscreteKernelField

Documentation

The actual finite fixed field of a continuous discrete representation.

Source context 5 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open RamificationTheory.Field.absoluteGaloisGroup
variable (F : Type) [Field F] [NumberField F]
variable {Q : Type*} [Group Q] [TopologicalSpace Q] [DiscreteTopology Q]

Lean source · statement

abbrev absoluteDiscreteKernelField (s : Field.absoluteGaloisGroup F →ₜ* Q) :
    IntermediateField F (AlgebraicClosure F)

theorem

absoluteDiscreteKernelField_isGalois

L45 ↗

ClassFieldTower.Martinet.Shafarevich.absoluteDiscreteKernelField_isGalois

Documentation

The kernel fixed field is Galois by normality of the actual kernel.

Source context 5 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open RamificationTheory.Field.absoluteGaloisGroup
variable (F : Type) [Field F] [NumberField F]
variable {Q : Type*} [Group Q] [TopologicalSpace Q] [DiscreteTopology Q]

Lean source · statement

theorem absoluteDiscreteKernelField_isGalois
    (s : Field.absoluteGaloisGroup F →ₜ* Q) : IsGalois F (absoluteDiscreteKernelField F s)

theorem

absoluteDiscreteKernelField_fixingSubgroup

L52 ↗

ClassFieldTower.Martinet.Shafarevich.absoluteDiscreteKernelField_fixingSubgroup

Documentation

The fixing subgroup is exactly the kernel of the original representation.

Source context 6 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open RamificationTheory.Field.absoluteGaloisGroup
variable (F : Type) [Field F] [NumberField F]
variable {Q : Type*} [Group Q] [TopologicalSpace Q] [DiscreteTopology Q]
variable (s : Field.absoluteGaloisGroup F →ₜ* Q)

Lean source · statement

theorem absoluteDiscreteKernelField_fixingSubgroup :
    (absoluteDiscreteKernelField F s).fixingSubgroup =
      (s.comp (↑(absoluteGaloisGroupContinuousMulEquiv F).symm :
        Gal(AlgebraicClosure F/F) →ₜ* Field.absoluteGaloisGroup F)).toMonoidHom.ker

def

absoluteDiscreteKernelGaloisHom

L60 ↗

ClassFieldTower.Martinet.Shafarevich.absoluteDiscreteKernelGaloisHom

Documentation

The finite Galois group acts faithfully through the target of the representation.

Source context 6 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open RamificationTheory.Field.absoluteGaloisGroup
variable (F : Type) [Field F] [NumberField F]
variable {Q : Type*} [Group Q] [TopologicalSpace Q] [DiscreteTopology Q]
variable (s : Field.absoluteGaloisGroup F →ₜ* Q)

Lean source · statement

def absoluteDiscreteKernelGaloisHom : Gal(absoluteDiscreteKernelField F s/F) →* Q

theorem

absoluteDiscreteKernelGaloisHom_injective

L70 ↗

ClassFieldTower.Martinet.Shafarevich.absoluteDiscreteKernelGaloisHom_injective

Documentation

Faithfulness follows from quotienting by exactly the kernel.

Source context 6 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open RamificationTheory.Field.absoluteGaloisGroup
variable (F : Type) [Field F] [NumberField F]
variable {Q : Type*} [Group Q] [TopologicalSpace Q] [DiscreteTopology Q]
variable (s : Field.absoluteGaloisGroup F →ₜ* Q)

Lean source · statement

theorem absoluteDiscreteKernelGaloisHom_injective :
    Function.Injective (absoluteDiscreteKernelGaloisHom F s)

theorem

absoluteDiscreteKernelField_isPGroup

L77 ↗

ClassFieldTower.Martinet.Shafarevich.absoluteDiscreteKernelField_isPGroup

Documentation

A p-group target gives a genuine finite Galois p-extension.

Source context 6 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open RamificationTheory.Field.absoluteGaloisGroup
variable (F : Type) [Field F] [NumberField F]
variable {Q : Type*} [Group Q] [TopologicalSpace Q] [DiscreteTopology Q]
variable (s : Field.absoluteGaloisGroup F →ₜ* Q)

Lean source · statement

theorem absoluteDiscreteKernelField_isPGroup
    (p : ℕ) (hP : IsPGroup p Q) : IsPGroup p Gal(absoluteDiscreteKernelField F s/F)

theorem

absoluteDiscreteKernelGaloisHom_restrict

L83 ↗

ClassFieldTower.Martinet.Shafarevich.absoluteDiscreteKernelGaloisHom_restrict

Documentation

Restriction to the kernel fixed field recovers the original representation.

Source context 6 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open RamificationTheory.Field.absoluteGaloisGroup
variable (F : Type) [Field F] [NumberField F]
variable {Q : Type*} [Group Q] [TopologicalSpace Q] [DiscreteTopology Q]
variable (s : Field.absoluteGaloisGroup F →ₜ* Q)

Lean source · statement

theorem absoluteDiscreteKernelGaloisHom_restrict
    (sigma : Field.absoluteGaloisGroup F) :
    absoluteDiscreteKernelGaloisHom F s
      (AlgEquiv.restrictNormalHom (absoluteDiscreteKernelField F s)
        (absoluteGaloisGroupContinuousMulEquiv F sigma)) =
        s sigma

Module documentation

The finite Galois field detected by a discrete absolute representation

Declarations