Module

FiniteIndexNormClassField.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.FiniteIndexNormClassField

24 declarations indexed from sourceView source ↗

Module documentation

Class fields of closed finite-index idele-class subgroups

For a closed finite-index subgroup H of the idele class group, the canonical ray modulus inside H supplies the finite seed for the full S-unit Kummer construction. When H is proper, the Kummer exponent is the index of H; when H is the whole group, exponent two gives a uniform finite Galois norm neighbourhood and the required containment is automatic.

The finite normal closure of the cyclotomic full S-unit Kummer extension therefore has ordinary idele-class norm range contained in H. Finite-abelian classification applied to that actual norm neighbourhood then realizes H, transported to the canonical embedded copy of the base field, as an exact determinant-norm subgroup.

Imports3

Imported by2

def

closedFiniteIndexNormExponent

L47 ↗

GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexNormExponent

Documentation

The Kummer exponent attached to a closed finite-index idele-class subgroup. A proper subgroup uses its exact index. The top subgroup uses exponent two, so the same concrete finite Galois construction also covers the trivial class field case.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain
open GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]
open scoped Classical in

Lean source · statement

def closedFiniteIndexNormExponent
    (H : Subgroup (IdeleClassGroup K))
    [H.FiniteIndex] :
    ℕ+

theorem

closedFiniteIndexNormExponent_eq_index

L57 ↗

GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexNormExponent_eq_index

Documentation

For a proper finite-index subgroup, its norm exponent is its index.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain
open GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem closedFiniteIndexNormExponent_eq_index
    (H : Subgroup (IdeleClassGroup K))
    [H.FiniteIndex]
    (hH : H ≠ ⊤) :
    closedFiniteIndexNormExponent (K := K) H =
      ⟨H.index,
        Nat.pos_of_ne_zero Subgroup.FiniteIndex.index_ne_zero⟩

theorem

one_lt_closedFiniteIndexNormExponent

L73 ↗

GlobalClassFieldTheory.GlobalClassFields.one_lt_closedFiniteIndexNormExponent

Documentation

The Kummer exponent attached to a finite-index subgroup is always strictly larger than one.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain
open GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem one_lt_closedFiniteIndexNormExponent
    (H : Subgroup (IdeleClassGroup K))
    [H.FiniteIndex] :
    1 < (closedFiniteIndexNormExponent (K := K) H : ℕ)

def

closedFiniteIndexNormSeed

L97 ↗

GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexNormSeed

Documentation

The finite seed used in the norm-neighbourhood construction is the support of the canonical ray modulus whose congruence subgroup lies in H.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain
open GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

def closedFiniteIndexNormSeed
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex] :
    Finset (HeightOneSpectrum (𝓞 K))

abbrev

closedFiniteIndexNormCyclotomicField

L105 ↗

GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexNormCyclotomicField

Documentation

The cyclotomic layer used by the finite-index norm construction.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain
open GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

abbrev closedFiniteIndexNormCyclotomicField
    (H : Subgroup (IdeleClassGroup K))
    [H.FiniteIndex] : Type

instance

closedFiniteIndexNormExponentNeZero

L111 ↗

GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexNormExponentNeZero

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain
open GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

instance closedFiniteIndexNormExponentNeZero
    (H : Subgroup (IdeleClassGroup K))
    [H.FiniteIndex] :
    NeZero (closedFiniteIndexNormExponent (K := K) H : ℕ)

instance

closedFiniteIndexNormCyclotomicFieldIsCyclotomicExtension

L117 ↗

GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexNormCyclotomicFieldIsCyclotomicExtension

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain
open GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

instance
    closedFiniteIndexNormCyclotomicFieldIsCyclotomicExtension
    (H : Subgroup (IdeleClassGroup K)) [H.FiniteIndex] :
    IsCyclotomicExtension
      {(closedFiniteIndexNormExponent (K := K) H : ℕ)} K
      (closedFiniteIndexNormCyclotomicField (K := K) H)

instance

closedFiniteIndexNormCyclotomicFieldFiniteDimensional

L128 ↗

GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexNormCyclotomicFieldFiniteDimensional

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain
open GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

instance
    closedFiniteIndexNormCyclotomicFieldFiniteDimensional
    (H : Subgroup (IdeleClassGroup K)) [H.FiniteIndex] :
    FiniteDimensional K
      (closedFiniteIndexNormCyclotomicField (K := K) H)

instance

closedFiniteIndexNormCyclotomicFieldNumberField

L137 ↗

GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexNormCyclotomicFieldNumberField

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain
open GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

instance closedFiniteIndexNormCyclotomicFieldNumberField
    (H : Subgroup (IdeleClassGroup K)) [H.FiniteIndex] :
    NumberField
      (closedFiniteIndexNormCyclotomicField (K := K) H)

instance

closedFiniteIndexNormCyclotomicFieldIsGalois

L144 ↗

GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexNormCyclotomicFieldIsGalois

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain
open GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

instance closedFiniteIndexNormCyclotomicFieldIsGalois
    (H : Subgroup (IdeleClassGroup K)) [H.FiniteIndex] :
    IsGalois K
      (closedFiniteIndexNormCyclotomicField (K := K) H)

abbrev

closedFiniteIndexNormKummerField

L154 ↗

GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexNormKummerField

Documentation

The full S-unit Kummer layer used by the finite-index norm construction.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain
open GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

abbrev closedFiniteIndexNormKummerField
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex] : Type

instance

closedFiniteIndexNormKummerFieldFiniteDimensional

L162 ↗

GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexNormKummerFieldFiniteDimensional

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain
open GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

instance closedFiniteIndexNormKummerFieldFiniteDimensional
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex] :
    FiniteDimensional
      (closedFiniteIndexNormCyclotomicField (K := K) H)
      (closedFiniteIndexNormKummerField (K := K) H hclosed)

instance

closedFiniteIndexNormKummerFieldIsGalois

L176 ↗

GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexNormKummerFieldIsGalois

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain
open GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

instance closedFiniteIndexNormKummerFieldIsGalois
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex] :
    IsGalois (closedFiniteIndexNormCyclotomicField (K := K) H)
      (closedFiniteIndexNormKummerField (K := K) H hclosed)

instance

closedFiniteIndexNormKummerFieldNumberField

L189 ↗

GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexNormKummerFieldNumberField

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain
open GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

instance closedFiniteIndexNormKummerFieldNumberField
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex] :
    NumberField (closedFiniteIndexNormKummerField (K := K) H hclosed)

instance

closedFiniteIndexNormKummerFieldAlgebraOverBase

L199 ↗

GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexNormKummerFieldAlgebraOverBase

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain
open GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

instance closedFiniteIndexNormKummerFieldAlgebraOverBase
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex] :
    Algebra K (closedFiniteIndexNormKummerField (K := K) H hclosed)

instance

closedFiniteIndexNormKummerFieldSMulOverBase

L211 ↗

GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexNormKummerFieldSMulOverBase

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain
open GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

instance closedFiniteIndexNormKummerFieldSMulOverBase
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex] :
    SMul K (closedFiniteIndexNormKummerField (K := K) H hclosed)

instance

closedFiniteIndexNormKummerFieldModuleOverBase

L220 ↗

GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexNormKummerFieldModuleOverBase

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain
open GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

instance closedFiniteIndexNormKummerFieldModuleOverBase
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex] :
    Module K (closedFiniteIndexNormKummerField (K := K) H hclosed)

instance

closedFiniteIndexNormKummerFieldScalarTower

L227 ↗

GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexNormKummerFieldScalarTower

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain
open GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

instance closedFiniteIndexNormKummerFieldScalarTower
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex] :
    IsScalarTower K
      (closedFiniteIndexNormCyclotomicField (K := K) H)
      (closedFiniteIndexNormKummerField (K := K) H hclosed)

instance

closedFiniteIndexNormKummerFieldFiniteDimensionalOverBase

L236 ↗

GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexNormKummerFieldFiniteDimensionalOverBase

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain
open GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

instance
    closedFiniteIndexNormKummerFieldFiniteDimensionalOverBase
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex] :
    FiniteDimensional K
      (closedFiniteIndexNormKummerField (K := K) H hclosed)

abbrev

closedFiniteIndexNormAmbient

L249 ↗

GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexNormAmbient

Documentation

The finite normal closure which is the actual Galois norm neighbourhood attached to H.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain
open GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

abbrev closedFiniteIndexNormAmbient
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex] : Type

instance

closedFiniteIndexNormAmbientFiniteDimensional

L256 ↗

GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexNormAmbientFiniteDimensional

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain
open GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

instance closedFiniteIndexNormAmbientFiniteDimensional
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex] :
    FiniteDimensional K
      (closedFiniteIndexNormAmbient (K := K) H hclosed)

instance

closedFiniteIndexNormAmbientNumberField

L265 ↗

GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexNormAmbientNumberField

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain
open GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

instance closedFiniteIndexNormAmbientNumberField
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex] :
    NumberField (closedFiniteIndexNormAmbient (K := K) H hclosed)

instance

closedFiniteIndexNormAmbientIsGalois

L275 ↗

GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexNormAmbientIsGalois

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain
open GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

instance closedFiniteIndexNormAmbientIsGalois
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex] :
    IsGalois K (closedFiniteIndexNormAmbient (K := K) H hclosed)

theorem

closedFiniteIndexSubgroup_has_finiteGaloisNormNeighborhood

L288 ↗

GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexSubgroup_has_finiteGaloisNormNeighborhood

Documentation

The finite normal closure of the cyclotomic full S-unit Kummer extension attached to a closed finite-index subgroup is an actual finite Galois norm neighbourhood contained in that subgroup.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain
open GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem closedFiniteIndexSubgroup_has_finiteGaloisNormNeighborhood
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex] :
    (_root_.ideleClassNorm K
      (closedFiniteIndexNormAmbient (K := K) H hclosed)).range ≤ H

Module documentation

Class fields of closed finite-index idele-class subgroups

Declarations