Module

SmallHilbertTowerUnramified.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.IdealClassFieldTheory.SmallHilbertTowerUnramified

15 declarations indexed from sourceView source ↗

Module documentation

Unramifiedness of the two-stage small Hilbert tower

The second-stage class field is selected in the rational absolute class formation. This file transports its exact abstract norm subgroup back to the ordinary idele class group of the actual middle fixed field. The intrinsic small-Hilbert characterization then proves genuine unramifiedness at both finite and infinite places.

Imports4

Imported by3

theorem

smallHilbertTowerAbsoluteFiniteDimensionalOfRelative

L38 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertTowerAbsoluteFiniteDimensionalOfRelative

Documentation

Transitivity over a number field, with the relative module fixed by the given algebra before the concrete fixed-field carriers are inserted.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation
open KummerTheory
open LocalClassFieldTheory
open GlobalClassFields

Lean source · statement

theorem smallHilbertTowerAbsoluteFiniteDimensionalOfRelative
    (F N : Type) [Field F] [NumberField F] [Field N]
    [Algebra ℚ N] [Algebra F N] [IsScalarTower ℚ F N]
    [FiniteDimensional F N] :
    FiniteDimensional ℚ N

abbrev

smallHilbertTowerTopField

L51 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertTowerTopField

Documentation

The actual top field in the selected two-stage small Hilbert tower, viewed over the selected first small Hilbert class field.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation
open KummerTheory
open LocalClassFieldTheory
open GlobalClassFields
section SelectedTower
variable (K : Type) [Field K] [NumberField K]

Lean source · statement

abbrev smallHilbertTowerTopField

abbrev

smallHilbertTowerFirstStageFiniteAbstractField

L55 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertTowerFirstStageFiniteAbstractField

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation
open KummerTheory
open LocalClassFieldTheory
open GlobalClassFields
section SelectedTower
variable (K : Type) [Field K] [NumberField K]

Lean source · statement

abbrev smallHilbertTowerFirstStageFiniteAbstractField :
    FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)

instance

smallHilbertTowerFirstStageAbsoluteQuotientFinite

L81 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertTowerFirstStageAbsoluteQuotientFinite

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation
open KummerTheory
open LocalClassFieldTheory
open GlobalClassFields
section SelectedTower
variable (K : Type) [Field K] [NumberField K]

Lean source · statement

instance
    smallHilbertTowerFirstStageAbsoluteQuotientFinite :
    Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          (smallHilbertClassFieldSubextension K).field
          (le_baseField
            (smallHilbertClassFieldSubextension K).field))

instance

smallHilbertTowerTopAlgebra

L97 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertTowerTopAlgebra

Documentation

The relative algebra is the canonical algebra carried by the intermediate-field presentation of the selected top field.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation
open KummerTheory
open LocalClassFieldTheory
open GlobalClassFields
section SelectedTower
variable (K : Type) [Field K] [NumberField K]

Lean source · statement

instance
    smallHilbertTowerTopAlgebra :
    Algebra
      (smallHilbertClassField K)
      (smallHilbertTowerTopField K)

def

smallHilbertTowerTopSMul

L107 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertTowerTopSMul

Documentation

Freeze the scalar-action owner induced by the canonical relative algebra.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation
open KummerTheory
open LocalClassFieldTheory
open GlobalClassFields
section SelectedTower
variable (K : Type) [Field K] [NumberField K]

Lean source · statement

def
    smallHilbertTowerTopSMul :
    SMul
      (smallHilbertClassField K)
      (smallHilbertTowerTopField K)

def

smallHilbertTowerTopModule

L117 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertTowerTopModule

Documentation

Freeze the module owner induced by the same canonical relative algebra.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation
open KummerTheory
open LocalClassFieldTheory
open GlobalClassFields
section SelectedTower
variable (K : Type) [Field K] [NumberField K]

Lean source · statement

def
    smallHilbertTowerTopModule :
    Module
      (smallHilbertClassField K)
      (smallHilbertTowerTopField K)

instance

smallHilbertTowerTopFiniteDimensional

L134 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertTowerTopFiniteDimensional

Documentation

The second selected stage is finite-dimensional over the first small Hilbert class field.

Source context 12 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation
open KummerTheory
open LocalClassFieldTheory
open GlobalClassFields
section SelectedTower
variable (K : Type) [Field K] [NumberField K]
section
attribute [local instance] smallHilbertTowerTopModule

Lean source · statement

instance smallHilbertTowerTopFiniteDimensional :
    FiniteDimensional
      (smallHilbertClassField K)
      (smallHilbertTowerTopField K)

instance

smallHilbertTowerTopScalarTower

L145 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertTowerTopScalarTower

Documentation

The rational base, first small Hilbert class field, and second selected stage form the actual scalar tower.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation
open KummerTheory
open LocalClassFieldTheory
open GlobalClassFields
section SelectedTower
variable (K : Type) [Field K] [NumberField K]

Lean source · statement

instance smallHilbertTowerTopScalarTower :
    IsScalarTower ℚ
      (smallHilbertClassField K)
      (smallHilbertTowerTopField K)

instance

smallHilbertTowerTopAbsoluteFiniteDimensional

L153 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertTowerTopAbsoluteFiniteDimensional

Documentation

The selected second stage is a finite extension of the rational field.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation
open KummerTheory
open LocalClassFieldTheory
open GlobalClassFields
section SelectedTower
variable (K : Type) [Field K] [NumberField K]

Lean source · statement

instance smallHilbertTowerTopAbsoluteFiniteDimensional :
    FiniteDimensional ℚ (smallHilbertTowerTopField K)

instance

smallHilbertTowerTopNumberField

L160 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertTowerTopNumberField

Documentation

The selected second-stage fixed field is a number field.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation
open KummerTheory
open LocalClassFieldTheory
open GlobalClassFields
section SelectedTower
variable (K : Type) [Field K] [NumberField K]

Lean source · statement

instance smallHilbertTowerTopNumberField :
    NumberField (smallHilbertTowerTopField K)

instance

smallHilbertTowerTopIsAbelianGalois

L166 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertTowerTopIsAbelianGalois

Documentation

The selected second stage is an abelian Galois extension of the first small Hilbert class field.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation
open KummerTheory
open LocalClassFieldTheory
open GlobalClassFields
section SelectedTower
variable (K : Type) [Field K] [NumberField K]

Lean source · statement

instance smallHilbertTowerTopIsAbelianGalois :
    IsAbelianGalois
      (smallHilbertClassField K)
      (smallHilbertTowerTopField K)

theorem

smallHilbertTowerSecondStage_ideleClassNorm_range

L178 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertTowerSecondStage_ideleClassNorm_range

Documentation

The actual norm range from the selected second stage is exactly the intrinsic small-Hilbert subgroup of the first stage.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation
open KummerTheory
open LocalClassFieldTheory
open GlobalClassFields

Lean source · statement

theorem smallHilbertTowerSecondStage_ideleClassNorm_range
    (K : Type) [Field K] [NumberField K] :
    (_root_.ideleClassNorm
      (smallHilbertClassField K)
      (smallHilbertTowerTopField K)).range =
        smallHilbertClassFieldNormSubgroup
          (K := smallHilbertClassField K)

theorem

smallHilbertTowerSecondStage_isEverywhereUnramified

L203 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertTowerSecondStage_isEverywhereUnramified

Documentation

The actual second stage in the selected two-stage small Hilbert tower is everywhere unramified over the first stage.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation
open KummerTheory
open LocalClassFieldTheory
open GlobalClassFields

Lean source · statement

theorem smallHilbertTowerSecondStage_isEverywhereUnramified
    (K : Type) [Field K] [NumberField K] :
    IsEverywhereUnramified
      (smallHilbertClassField K)
      (smallHilbertTowerTopField K)

theorem

smallHilbertTower_maximalAbelianSubextension_eq_firstStage

L214 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertTower_maximalAbelianSubextension_eq_firstStage

Documentation

In the selected two-stage small Hilbert tower, the maximal abelian intermediate extension of the top over the original base is exactly the first small Hilbert class field.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation
open KummerTheory
open LocalClassFieldTheory
open GlobalClassFields

Lean source · statement

theorem smallHilbertTower_maximalAbelianSubextension_eq_firstStage
    (K : Type) [Field K] [NumberField K] :
    maximalAbelianSubextension
        (smallHilbertTowerGaloisRealization K) =
      smallHilbertClassFieldSubextension K

Module documentation

Unramifiedness of the two-stage small Hilbert tower

Declarations