NYLL
Module

CyclotomicKummerNormDescent.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.CyclotomicKummerNormDescent
24 declarations indexed from sourceView source ↗

Module documentation

Cyclotomic descent for full S-unit Kummer norms

This file implements the roots-of-unity descent in the existence proof of global class field theory. Starting from a finite seed of finite places of K, it enlarges the seed just enough that its full inverse image in CyclotomicField n K is a chosen Kummer norm support. Thus the full S-unit Kummer extension over the cyclotomic field has its concrete norm subgroup described by Kummer theory, while the support is still exactly a full inverse image and hence descends through the cyclotomic norm.

The final normal-closure step turns the resulting finite extension of K into a genuine finite Galois extension without enlarging its norm subgroup.

Imports5
Imported by2

Declarations

instance

cyclotomicKummerNormDescent_neZero

L43 ↗
GlobalClassFieldTheory.GlobalClassFields.cyclotomicKummerNormDescent_neZero
Source context 8 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
open KummerTheory
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]
Lean source · statement
instance cyclotomicKummerNormDescent_neZero
    (n : ℕ+) : NeZero (n : ℕ)
instance

cyclotomicKummerNormDescent_cyclotomicFiniteDimensional

L47 ↗
GlobalClassFieldTheory.GlobalClassFields.cyclotomicKummerNormDescent_cyclotomicFiniteDimensional
Source context 9 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
open KummerTheory
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]
local instance cyclotomicKummerNormDescent_neZero
    (n : ℕ+) : NeZero (n : ℕ) :=
  ⟨n.ne_zero⟩
Lean source · statement
instance
    cyclotomicKummerNormDescent_cyclotomicFiniteDimensional
    (n : ℕ+) :
    FiniteDimensional K (CyclotomicField (n : ℕ) K)
instance

cyclotomicKummerNormDescent_cyclotomicIsGalois

L54 ↗
GlobalClassFieldTheory.GlobalClassFields.cyclotomicKummerNormDescent_cyclotomicIsGalois
Source context 10 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
open KummerTheory
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]
local instance cyclotomicKummerNormDescent_neZero
    (n : ℕ+) : NeZero (n : ℕ) :=
  ⟨n.ne_zero⟩
noncomputable local instance
    cyclotomicKummerNormDescent_cyclotomicFiniteDimensional
    (n : ℕ+) :
    FiniteDimensional K (CyclotomicField (n : ℕ) K) :=
  IsCyclotomicExtension.finiteDimensional
    {(n : ℕ)} K (CyclotomicField (n : ℕ) K)
Lean source · statement
instance
    cyclotomicKummerNormDescent_cyclotomicIsGalois
    (n : ℕ+) :
    IsGalois K (CyclotomicField (n : ℕ) K)
theorem

cyclotomicKummerNormDescent_primitiveRoots_nonempty

L61 ↗
GlobalClassFieldTheory.GlobalClassFields.cyclotomicKummerNormDescent_primitiveRoots_nonempty
Source context 11 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
open KummerTheory
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]
local instance cyclotomicKummerNormDescent_neZero
    (n : ℕ+) : NeZero (n : ℕ) :=
  ⟨n.ne_zero⟩
noncomputable local instance
    cyclotomicKummerNormDescent_cyclotomicFiniteDimensional
    (n : ℕ+) :
    FiniteDimensional K (CyclotomicField (n : ℕ) K) :=
  IsCyclotomicExtension.finiteDimensional
    {(n : ℕ)} K (CyclotomicField (n : ℕ) K)
noncomputable local instance
    cyclotomicKummerNormDescent_cyclotomicIsGalois
    (n : ℕ+) :
    IsGalois K (CyclotomicField (n : ℕ) K) :=
  IsCyclotomicExtension.isGalois
    {(n : ℕ)} K (CyclotomicField (n : ℕ) K)
Lean source · statement
theorem cyclotomicKummerNormDescent_primitiveRoots_nonempty
    (n : ℕ+) :
    (primitiveRoots (n : ℕ)
      (CyclotomicField (n : ℕ) K)).Nonempty
theorem

cyclotomicKummerNormDescent_natCast_ne_zero

L70 ↗
GlobalClassFieldTheory.GlobalClassFields.cyclotomicKummerNormDescent_natCast_ne_zero
Source context 11 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
open KummerTheory
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]
local instance cyclotomicKummerNormDescent_neZero
    (n : ℕ+) : NeZero (n : ℕ) :=
  ⟨n.ne_zero⟩
noncomputable local instance
    cyclotomicKummerNormDescent_cyclotomicFiniteDimensional
    (n : ℕ+) :
    FiniteDimensional K (CyclotomicField (n : ℕ) K) :=
  IsCyclotomicExtension.finiteDimensional
    {(n : ℕ)} K (CyclotomicField (n : ℕ) K)
noncomputable local instance
    cyclotomicKummerNormDescent_cyclotomicIsGalois
    (n : ℕ+) :
    IsGalois K (CyclotomicField (n : ℕ) K) :=
  IsCyclotomicExtension.isGalois
    {(n : ℕ)} K (CyclotomicField (n : ℕ) K)
Lean source · statement
theorem cyclotomicKummerNormDescent_natCast_ne_zero
    (n : ℕ+) :
    ((n : ℕ) : CyclotomicField (n : ℕ) K) ≠ 0
def

cyclotomicKummerNormSupport

L82 ↗
GlobalClassFieldTheory.GlobalClassFields.cyclotomicKummerNormSupport
Documentation

A finite support on K whose full inverse image in CyclotomicField n K contains the chosen Kummer norm support upstairs.

The construction first forms the chosen support above the prescribed seed and then adds the places below it. Taking all places above this enlarged base support saturates every fibre without losing the largeness and exponent support required by the full S-unit Kummer calculation.

Source context 11 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
open KummerTheory
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]
local instance cyclotomicKummerNormDescent_neZero
    (n : ℕ+) : NeZero (n : ℕ) :=
  ⟨n.ne_zero⟩
noncomputable local instance
    cyclotomicKummerNormDescent_cyclotomicFiniteDimensional
    (n : ℕ+) :
    FiniteDimensional K (CyclotomicField (n : ℕ) K) :=
  IsCyclotomicExtension.finiteDimensional
    {(n : ℕ)} K (CyclotomicField (n : ℕ) K)
noncomputable local instance
    cyclotomicKummerNormDescent_cyclotomicIsGalois
    (n : ℕ+) :
    IsGalois K (CyclotomicField (n : ℕ) K) :=
  IsCyclotomicExtension.isGalois
    {(n : ℕ)} K (CyclotomicField (n : ℕ) K)
Lean source · statement
def cyclotomicKummerNormSupport
    (n : ℕ+)
    (seed : Finset (HeightOneSpectrum (𝓞 K))) :
    Finset (HeightOneSpectrum (𝓞 K))
theorem

subset_cyclotomicKummerNormSupport

L97 ↗
GlobalClassFieldTheory.GlobalClassFields.subset_cyclotomicKummerNormSupport
Documentation

The prescribed finite seed is contained in its cyclotomic Kummer norm support.

Source context 11 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
open KummerTheory
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]
local instance cyclotomicKummerNormDescent_neZero
    (n : ℕ+) : NeZero (n : ℕ) :=
  ⟨n.ne_zero⟩
noncomputable local instance
    cyclotomicKummerNormDescent_cyclotomicFiniteDimensional
    (n : ℕ+) :
    FiniteDimensional K (CyclotomicField (n : ℕ) K) :=
  IsCyclotomicExtension.finiteDimensional
    {(n : ℕ)} K (CyclotomicField (n : ℕ) K)
noncomputable local instance
    cyclotomicKummerNormDescent_cyclotomicIsGalois
    (n : ℕ+) :
    IsGalois K (CyclotomicField (n : ℕ) K) :=
  IsCyclotomicExtension.isGalois
    {(n : ℕ)} K (CyclotomicField (n : ℕ) K)
Lean source · statement
theorem subset_cyclotomicKummerNormSupport
    (n : ℕ+)
    (seed : Finset (HeightOneSpectrum (𝓞 K))) :
    seed ⊆ cyclotomicKummerNormSupport (K := K) n seed
def

cyclotomicKummerNormSupportAbove

L108 ↗
GlobalClassFieldTheory.GlobalClassFields.cyclotomicKummerNormSupportAbove
Documentation

All finite places of the cyclotomic field above the enlarged base support. This is the fibre-saturated support used by norm descent.

Source context 11 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
open KummerTheory
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]
local instance cyclotomicKummerNormDescent_neZero
    (n : ℕ+) : NeZero (n : ℕ) :=
  ⟨n.ne_zero⟩
noncomputable local instance
    cyclotomicKummerNormDescent_cyclotomicFiniteDimensional
    (n : ℕ+) :
    FiniteDimensional K (CyclotomicField (n : ℕ) K) :=
  IsCyclotomicExtension.finiteDimensional
    {(n : ℕ)} K (CyclotomicField (n : ℕ) K)
noncomputable local instance
    cyclotomicKummerNormDescent_cyclotomicIsGalois
    (n : ℕ+) :
    IsGalois K (CyclotomicField (n : ℕ) K) :=
  IsCyclotomicExtension.isGalois
    {(n : ℕ)} K (CyclotomicField (n : ℕ) K)
Lean source · statement
def cyclotomicKummerNormSupportAbove
    (n : ℕ+)
    (seed : Finset (HeightOneSpectrum (𝓞 K))) :
    Finset
      (HeightOneSpectrum
        (𝓞 (CyclotomicField (n : ℕ) K)))
theorem

mem_cyclotomicKummerNormSupportAbove_iff

L121 ↗
GlobalClassFieldTheory.GlobalClassFields.mem_cyclotomicKummerNormSupportAbove_iff
Documentation

Membership in the upstairs support is exactly membership of the place below in the enlarged base support.

Source context 11 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
open KummerTheory
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]
local instance cyclotomicKummerNormDescent_neZero
    (n : ℕ+) : NeZero (n : ℕ) :=
  ⟨n.ne_zero⟩
noncomputable local instance
    cyclotomicKummerNormDescent_cyclotomicFiniteDimensional
    (n : ℕ+) :
    FiniteDimensional K (CyclotomicField (n : ℕ) K) :=
  IsCyclotomicExtension.finiteDimensional
    {(n : ℕ)} K (CyclotomicField (n : ℕ) K)
noncomputable local instance
    cyclotomicKummerNormDescent_cyclotomicIsGalois
    (n : ℕ+) :
    IsGalois K (CyclotomicField (n : ℕ) K) :=
  IsCyclotomicExtension.isGalois
    {(n : ℕ)} K (CyclotomicField (n : ℕ) K)
Lean source · statement
theorem mem_cyclotomicKummerNormSupportAbove_iff
    (n : ℕ+)
    (seed : Finset (HeightOneSpectrum (𝓞 K)))
    (W :
      HeightOneSpectrum
        (𝓞 (CyclotomicField (n : ℕ) K))) :
    W ∈ cyclotomicKummerNormSupportAbove (K := K) n seed ↔
      finitePlaceBelow (K := K) W ∈
        cyclotomicKummerNormSupport (K := K) n seed
theorem

sUnitKummerNormSupport_cyclotomicKummerNormSupportAbove

L138 ↗
GlobalClassFieldTheory.GlobalClassFields.sUnitKummerNormSupport_cyclotomicKummerNormSupportAbove
Documentation

The fibre-saturated support upstairs is already fixed by the chosen Kummer-support enlargement.

Source context 11 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
open KummerTheory
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]
local instance cyclotomicKummerNormDescent_neZero
    (n : ℕ+) : NeZero (n : ℕ) :=
  ⟨n.ne_zero⟩
noncomputable local instance
    cyclotomicKummerNormDescent_cyclotomicFiniteDimensional
    (n : ℕ+) :
    FiniteDimensional K (CyclotomicField (n : ℕ) K) :=
  IsCyclotomicExtension.finiteDimensional
    {(n : ℕ)} K (CyclotomicField (n : ℕ) K)
noncomputable local instance
    cyclotomicKummerNormDescent_cyclotomicIsGalois
    (n : ℕ+) :
    IsGalois K (CyclotomicField (n : ℕ) K) :=
  IsCyclotomicExtension.isGalois
    {(n : ℕ)} K (CyclotomicField (n : ℕ) K)
Lean source · statement
theorem sUnitKummerNormSupport_cyclotomicKummerNormSupportAbove
    (n : ℕ+)
    (seed : Finset (HeightOneSpectrum (𝓞 K))) :
    sUnitKummerNormSupport
        (K := CyclotomicField (n : ℕ) K) n
        (cyclotomicKummerNormSupportAbove (K := K) n seed) =
      cyclotomicKummerNormSupportAbove (K := K) n seed
theorem

cyclotomicKummerNormSupport_idem

L196 ↗
GlobalClassFieldTheory.GlobalClassFields.cyclotomicKummerNormSupport_idem
Documentation

Enlarging a support by the cyclotomic Kummer requirements is idempotent. In particular, downstream neighbourhood arguments may choose a support containing these requirements from the outset without a second change of support.

Source context 11 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
open KummerTheory
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]
local instance cyclotomicKummerNormDescent_neZero
    (n : ℕ+) : NeZero (n : ℕ) :=
  ⟨n.ne_zero⟩
noncomputable local instance
    cyclotomicKummerNormDescent_cyclotomicFiniteDimensional
    (n : ℕ+) :
    FiniteDimensional K (CyclotomicField (n : ℕ) K) :=
  IsCyclotomicExtension.finiteDimensional
    {(n : ℕ)} K (CyclotomicField (n : ℕ) K)
noncomputable local instance
    cyclotomicKummerNormDescent_cyclotomicIsGalois
    (n : ℕ+) :
    IsGalois K (CyclotomicField (n : ℕ) K) :=
  IsCyclotomicExtension.isGalois
    {(n : ℕ)} K (CyclotomicField (n : ℕ) K)
Lean source · statement
theorem cyclotomicKummerNormSupport_idem
    (n : ℕ+)
    (seed : Finset (HeightOneSpectrum (𝓞 K))) :
    cyclotomicKummerNormSupport (K := K) n
        (cyclotomicKummerNormSupport (K := K) n seed) =
      cyclotomicKummerNormSupport (K := K) n seed
abbrev

cyclotomicFullSUnitKummerExtension

L233 ↗
GlobalClassFieldTheory.GlobalClassFields.cyclotomicFullSUnitKummerExtension
Documentation

The actual full S-unit Kummer extension over the cyclotomic base, formed inside its fixed separable closure and using the chosen enlargement of the fibre-saturated support above K. The preceding stability theorem shows that this enlargement is equal to the fibre-saturated support; retaining it in the definition keeps the extension definitionally aligned with the exact Kummer norm-realization theorem.

Source context 11 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
open KummerTheory
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]
local instance cyclotomicKummerNormDescent_neZero
    (n : ℕ+) : NeZero (n : ℕ) :=
  ⟨n.ne_zero⟩
noncomputable local instance
    cyclotomicKummerNormDescent_cyclotomicFiniteDimensional
    (n : ℕ+) :
    FiniteDimensional K (CyclotomicField (n : ℕ) K) :=
  IsCyclotomicExtension.finiteDimensional
    {(n : ℕ)} K (CyclotomicField (n : ℕ) K)
noncomputable local instance
    cyclotomicKummerNormDescent_cyclotomicIsGalois
    (n : ℕ+) :
    IsGalois K (CyclotomicField (n : ℕ) K) :=
  IsCyclotomicExtension.isGalois
    {(n : ℕ)} K (CyclotomicField (n : ℕ) K)
Lean source · statement
abbrev cyclotomicFullSUnitKummerExtension
    (n : ℕ+)
    (seed : Finset (HeightOneSpectrum (𝓞 K))) :
    IntermediateField
      (CyclotomicField (n : ℕ) K)
      (SeparableClosure (CyclotomicField (n : ℕ) K))
theorem

cyclotomicFullSUnitKummerExtension_isGalois

L248 ↗
GlobalClassFieldTheory.GlobalClassFields.cyclotomicFullSUnitKummerExtension_isGalois
Documentation

The cyclotomic full S-unit Kummer extension is Galois over the cyclotomic base.

Source context 11 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
open KummerTheory
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]
local instance cyclotomicKummerNormDescent_neZero
    (n : ℕ+) : NeZero (n : ℕ) :=
  ⟨n.ne_zero⟩
noncomputable local instance
    cyclotomicKummerNormDescent_cyclotomicFiniteDimensional
    (n : ℕ+) :
    FiniteDimensional K (CyclotomicField (n : ℕ) K) :=
  IsCyclotomicExtension.finiteDimensional
    {(n : ℕ)} K (CyclotomicField (n : ℕ) K)
noncomputable local instance
    cyclotomicKummerNormDescent_cyclotomicIsGalois
    (n : ℕ+) :
    IsGalois K (CyclotomicField (n : ℕ) K) :=
  IsCyclotomicExtension.isGalois
    {(n : ℕ)} K (CyclotomicField (n : ℕ) K)
Lean source · statement
theorem cyclotomicFullSUnitKummerExtension_isGalois
    (n : ℕ+)
    (seed : Finset (HeightOneSpectrum (𝓞 K))) :
    IsGalois
      (CyclotomicField (n : ℕ) K)
      (cyclotomicFullSUnitKummerExtension (K := K) n seed)
theorem

cyclotomicFullSUnitKummerExtension_finiteDimensional

L264 ↗
GlobalClassFieldTheory.GlobalClassFields.cyclotomicFullSUnitKummerExtension_finiteDimensional
Documentation

The cyclotomic full S-unit Kummer extension is finite over the cyclotomic base.

Source context 11 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
open KummerTheory
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]
local instance cyclotomicKummerNormDescent_neZero
    (n : ℕ+) : NeZero (n : ℕ) :=
  ⟨n.ne_zero⟩
noncomputable local instance
    cyclotomicKummerNormDescent_cyclotomicFiniteDimensional
    (n : ℕ+) :
    FiniteDimensional K (CyclotomicField (n : ℕ) K) :=
  IsCyclotomicExtension.finiteDimensional
    {(n : ℕ)} K (CyclotomicField (n : ℕ) K)
noncomputable local instance
    cyclotomicKummerNormDescent_cyclotomicIsGalois
    (n : ℕ+) :
    IsGalois K (CyclotomicField (n : ℕ) K) :=
  IsCyclotomicExtension.isGalois
    {(n : ℕ)} K (CyclotomicField (n : ℕ) K)
Lean source · statement
theorem cyclotomicFullSUnitKummerExtension_finiteDimensional
    (n : ℕ+)
    (seed : Finset (HeightOneSpectrum (𝓞 K))) :
    FiniteDimensional
      (CyclotomicField (n : ℕ) K)
      (cyclotomicFullSUnitKummerExtension (K := K) n seed)
instance

cyclotomicKummerNormDescent_kummerFiniteDimensional

L284 ↗
GlobalClassFieldTheory.GlobalClassFields.cyclotomicKummerNormDescent_kummerFiniteDimensional
Source context 11 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
open KummerTheory
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]
local instance cyclotomicKummerNormDescent_neZero
    (n : ℕ+) : NeZero (n : ℕ) :=
  ⟨n.ne_zero⟩
noncomputable local instance
    cyclotomicKummerNormDescent_cyclotomicFiniteDimensional
    (n : ℕ+) :
    FiniteDimensional K (CyclotomicField (n : ℕ) K) :=
  IsCyclotomicExtension.finiteDimensional
    {(n : ℕ)} K (CyclotomicField (n : ℕ) K)
noncomputable local instance
    cyclotomicKummerNormDescent_cyclotomicIsGalois
    (n : ℕ+) :
    IsGalois K (CyclotomicField (n : ℕ) K) :=
  IsCyclotomicExtension.isGalois
    {(n : ℕ)} K (CyclotomicField (n : ℕ) K)
Lean source · statement
instance
    cyclotomicKummerNormDescent_kummerFiniteDimensional
    (n : ℕ+)
    (seed : Finset (HeightOneSpectrum (𝓞 K))) :
    FiniteDimensional
      (CyclotomicField (n : ℕ) K)
      (cyclotomicFullSUnitKummerExtension (K := K) n seed)
theorem

cyclotomicKummerNormDescent_kummerNumberField

L298 ↗
GlobalClassFieldTheory.GlobalClassFields.cyclotomicKummerNormDescent_kummerNumberField
Documentation

The Kummer layer is a number field via its finite extension of the cyclotomic number field. This is deliberately a named, non-instance boundary: downstream base-tower instances must not make every NumberField search unfold the full S-unit Kummer construction.

Source context 12 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
open KummerTheory
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]
local instance cyclotomicKummerNormDescent_neZero
    (n : ℕ+) : NeZero (n : ℕ) :=
  ⟨n.ne_zero⟩
noncomputable local instance
    cyclotomicKummerNormDescent_cyclotomicFiniteDimensional
    (n : ℕ+) :
    FiniteDimensional K (CyclotomicField (n : ℕ) K) :=
  IsCyclotomicExtension.finiteDimensional
    {(n : ℕ)} K (CyclotomicField (n : ℕ) K)
noncomputable local instance
    cyclotomicKummerNormDescent_cyclotomicIsGalois
    (n : ℕ+) :
    IsGalois K (CyclotomicField (n : ℕ) K) :=
  IsCyclotomicExtension.isGalois
    {(n : ℕ)} K (CyclotomicField (n : ℕ) K)
noncomputable local instance
    cyclotomicKummerNormDescent_kummerFiniteDimensional
    (n : ℕ+)
    (seed : Finset (HeightOneSpectrum (𝓞 K))) :
    FiniteDimensional
      (CyclotomicField (n : ℕ) K)
      (cyclotomicFullSUnitKummerExtension (K := K) n seed) :=
  cyclotomicFullSUnitKummerExtension_finiteDimensional
    (K := K) n seed
Lean source · statement
theorem cyclotomicKummerNormDescent_kummerNumberField
    (n : ℕ+)
    (seed : Finset (HeightOneSpectrum (𝓞 K))) :
    NumberField
      (cyclotomicFullSUnitKummerExtension (K := K) n seed)
theorem

cyclotomicFullSUnitKummerExtension_cyclotomicNormRange

L309 ↗
GlobalClassFieldTheory.GlobalClassFields.cyclotomicFullSUnitKummerExtension_cyclotomicNormRange
Documentation

The expensive Kummer norm computation over the cyclotomic base, isolated before the K-to-Kummer-field instance tower is introduced.

Source context 12 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
open KummerTheory
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]
local instance cyclotomicKummerNormDescent_neZero
    (n : ℕ+) : NeZero (n : ℕ) :=
  ⟨n.ne_zero⟩
noncomputable local instance
    cyclotomicKummerNormDescent_cyclotomicFiniteDimensional
    (n : ℕ+) :
    FiniteDimensional K (CyclotomicField (n : ℕ) K) :=
  IsCyclotomicExtension.finiteDimensional
    {(n : ℕ)} K (CyclotomicField (n : ℕ) K)
noncomputable local instance
    cyclotomicKummerNormDescent_cyclotomicIsGalois
    (n : ℕ+) :
    IsGalois K (CyclotomicField (n : ℕ) K) :=
  IsCyclotomicExtension.isGalois
    {(n : ℕ)} K (CyclotomicField (n : ℕ) K)
noncomputable local instance
    cyclotomicKummerNormDescent_kummerFiniteDimensional
    (n : ℕ+)
    (seed : Finset (HeightOneSpectrum (𝓞 K))) :
    FiniteDimensional
      (CyclotomicField (n : ℕ) K)
      (cyclotomicFullSUnitKummerExtension (K := K) n seed) :=
  cyclotomicFullSUnitKummerExtension_finiteDimensional
    (K := K) n seed
Lean source · full declaration
theorem
    cyclotomicFullSUnitKummerExtension_cyclotomicNormRange
    (n : ℕ+)
    (hn : 1 < (n : ℕ))
    (seed : Finset (HeightOneSpectrum (𝓞 K))) :
    let C := CyclotomicField (n : ℕ) K
    let S' := cyclotomicKummerNormSupportAbove (K := K) n seed
    let E := cyclotomicFullSUnitKummerExtension (K := K) n seed
    letI : NumberField E :=
      cyclotomicKummerNormDescent_kummerNumberField (K := K) n seed
    (_root_.ideleClassNorm C E).range =
      ideleClassPowerLocalUnitSubgroup (K := C) n S' ∅ := by
  classical
  dsimp only
  let C := CyclotomicField (n : ℕ) K
  let S' := cyclotomicKummerNormSupportAbove (K := K) n seed
  let E := cyclotomicFullSUnitKummerExtension (K := K) n seed
  let : NumberField E :=
    cyclotomicKummerNormDescent_kummerNumberField (K := K) n seed
  have hmu : (primitiveRoots (n : ℕ) C).Nonempty :=
    cyclotomicKummerNormDescent_primitiveRoots_nonempty
      (K := K) n
  have hstable :
      sUnitKummerNormSupport (K := C) n S' = S' := by
    simpa only [C, S'] using
      sUnitKummerNormSupport_cyclotomicKummerNormSupportAbove
        (K := K) n seed
  have hNormCanonical :
      (_root_.ideleClassNorm C E).range =
        ideleClassPowerLocalUnitSubgroup (K := C) n
          (sUnitKummerNormSupport (K := C) n S') ∅ := by
    simpa only [C, S', E, cyclotomicFullSUnitKummerExtension] using
      (fullSUnitKummerExtension_ideleClassNormRange_eq_powerLocalUnit
        (K := C) (Omega := SeparableClosure C)
        n hn hmu S')
  exact hNormCanonical.trans
    (congrArg
      (fun T => ideleClassPowerLocalUnitSubgroup (K := C) n T ∅)
      hstable)
instance

cyclotomicKummerNormDescent_kummerAlgebraOverBase

L350 ↗
GlobalClassFieldTheory.GlobalClassFields.cyclotomicKummerNormDescent_kummerAlgebraOverBase
Source context 12 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
open KummerTheory
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]
local instance cyclotomicKummerNormDescent_neZero
    (n : ℕ+) : NeZero (n : ℕ) :=
  ⟨n.ne_zero⟩
noncomputable local instance
    cyclotomicKummerNormDescent_cyclotomicFiniteDimensional
    (n : ℕ+) :
    FiniteDimensional K (CyclotomicField (n : ℕ) K) :=
  IsCyclotomicExtension.finiteDimensional
    {(n : ℕ)} K (CyclotomicField (n : ℕ) K)
noncomputable local instance
    cyclotomicKummerNormDescent_cyclotomicIsGalois
    (n : ℕ+) :
    IsGalois K (CyclotomicField (n : ℕ) K) :=
  IsCyclotomicExtension.isGalois
    {(n : ℕ)} K (CyclotomicField (n : ℕ) K)
noncomputable local instance
    cyclotomicKummerNormDescent_kummerFiniteDimensional
    (n : ℕ+)
    (seed : Finset (HeightOneSpectrum (𝓞 K))) :
    FiniteDimensional
      (CyclotomicField (n : ℕ) K)
      (cyclotomicFullSUnitKummerExtension (K := K) n seed) :=
  cyclotomicFullSUnitKummerExtension_finiteDimensional
    (K := K) n seed
Lean source · statement
instance
    cyclotomicKummerNormDescent_kummerAlgebraOverBase
    (n : ℕ+)
    (seed : Finset (HeightOneSpectrum (𝓞 K))) :
    Algebra K
      (cyclotomicFullSUnitKummerExtension (K := K) n seed)
def

cyclotomicKummerNormDescent_kummerSMulOverBase

L362 ↗
GlobalClassFieldTheory.GlobalClassFields.cyclotomicKummerNormDescent_kummerSMulOverBase
Source context 13 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
open KummerTheory
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]
local instance cyclotomicKummerNormDescent_neZero
    (n : ℕ+) : NeZero (n : ℕ) :=
  ⟨n.ne_zero⟩
noncomputable local instance
    cyclotomicKummerNormDescent_cyclotomicFiniteDimensional
    (n : ℕ+) :
    FiniteDimensional K (CyclotomicField (n : ℕ) K) :=
  IsCyclotomicExtension.finiteDimensional
    {(n : ℕ)} K (CyclotomicField (n : ℕ) K)
noncomputable local instance
    cyclotomicKummerNormDescent_cyclotomicIsGalois
    (n : ℕ+) :
    IsGalois K (CyclotomicField (n : ℕ) K) :=
  IsCyclotomicExtension.isGalois
    {(n : ℕ)} K (CyclotomicField (n : ℕ) K)
noncomputable local instance
    cyclotomicKummerNormDescent_kummerFiniteDimensional
    (n : ℕ+)
    (seed : Finset (HeightOneSpectrum (𝓞 K))) :
    FiniteDimensional
      (CyclotomicField (n : ℕ) K)
      (cyclotomicFullSUnitKummerExtension (K := K) n seed) :=
  cyclotomicFullSUnitKummerExtension_finiteDimensional
    (K := K) n seed
@[reducible]
noncomputable local instance
    cyclotomicKummerNormDescent_kummerAlgebraOverBase
    (n : ℕ+)
    (seed : Finset (HeightOneSpectrum (𝓞 K))) :
    Algebra K
      (cyclotomicFullSUnitKummerExtension (K := K) n seed) :=
  ((algebraMap
      (CyclotomicField (n : ℕ) K)
      (cyclotomicFullSUnitKummerExtension (K := K) n seed)).comp
    (algebraMap K (CyclotomicField (n : ℕ) K))).toAlgebra
Lean source · statement
def
    cyclotomicKummerNormDescent_kummerSMulOverBase
    (n : ℕ+)
    (seed : Finset (HeightOneSpectrum (𝓞 K))) :
    SMul K
      (cyclotomicFullSUnitKummerExtension (K := K) n seed)
def

cyclotomicKummerNormDescent_kummerModuleOverBase

L373 ↗
GlobalClassFieldTheory.GlobalClassFields.cyclotomicKummerNormDescent_kummerModuleOverBase
Source context 13 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
open KummerTheory
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]
local instance cyclotomicKummerNormDescent_neZero
    (n : ℕ+) : NeZero (n : ℕ) :=
  ⟨n.ne_zero⟩
noncomputable local instance
    cyclotomicKummerNormDescent_cyclotomicFiniteDimensional
    (n : ℕ+) :
    FiniteDimensional K (CyclotomicField (n : ℕ) K) :=
  IsCyclotomicExtension.finiteDimensional
    {(n : ℕ)} K (CyclotomicField (n : ℕ) K)
noncomputable local instance
    cyclotomicKummerNormDescent_cyclotomicIsGalois
    (n : ℕ+) :
    IsGalois K (CyclotomicField (n : ℕ) K) :=
  IsCyclotomicExtension.isGalois
    {(n : ℕ)} K (CyclotomicField (n : ℕ) K)
noncomputable local instance
    cyclotomicKummerNormDescent_kummerFiniteDimensional
    (n : ℕ+)
    (seed : Finset (HeightOneSpectrum (𝓞 K))) :
    FiniteDimensional
      (CyclotomicField (n : ℕ) K)
      (cyclotomicFullSUnitKummerExtension (K := K) n seed) :=
  cyclotomicFullSUnitKummerExtension_finiteDimensional
    (K := K) n seed
@[reducible]
noncomputable local instance
    cyclotomicKummerNormDescent_kummerAlgebraOverBase
    (n : ℕ+)
    (seed : Finset (HeightOneSpectrum (𝓞 K))) :
    Algebra K
      (cyclotomicFullSUnitKummerExtension (K := K) n seed) :=
  ((algebraMap
      (CyclotomicField (n : ℕ) K)
      (cyclotomicFullSUnitKummerExtension (K := K) n seed)).comp
    (algebraMap K (CyclotomicField (n : ℕ) K))).toAlgebra
Lean source · statement
def
    cyclotomicKummerNormDescent_kummerModuleOverBase
    (n : ℕ+)
    (seed : Finset (HeightOneSpectrum (𝓞 K))) :
    Module K
      (cyclotomicFullSUnitKummerExtension (K := K) n seed)
theorem

cyclotomicKummerNormDescent_kummerScalarTower

L381 ↗
GlobalClassFieldTheory.GlobalClassFields.cyclotomicKummerNormDescent_kummerScalarTower
Source context 13 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
open KummerTheory
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]
local instance cyclotomicKummerNormDescent_neZero
    (n : ℕ+) : NeZero (n : ℕ) :=
  ⟨n.ne_zero⟩
noncomputable local instance
    cyclotomicKummerNormDescent_cyclotomicFiniteDimensional
    (n : ℕ+) :
    FiniteDimensional K (CyclotomicField (n : ℕ) K) :=
  IsCyclotomicExtension.finiteDimensional
    {(n : ℕ)} K (CyclotomicField (n : ℕ) K)
noncomputable local instance
    cyclotomicKummerNormDescent_cyclotomicIsGalois
    (n : ℕ+) :
    IsGalois K (CyclotomicField (n : ℕ) K) :=
  IsCyclotomicExtension.isGalois
    {(n : ℕ)} K (CyclotomicField (n : ℕ) K)
noncomputable local instance
    cyclotomicKummerNormDescent_kummerFiniteDimensional
    (n : ℕ+)
    (seed : Finset (HeightOneSpectrum (𝓞 K))) :
    FiniteDimensional
      (CyclotomicField (n : ℕ) K)
      (cyclotomicFullSUnitKummerExtension (K := K) n seed) :=
  cyclotomicFullSUnitKummerExtension_finiteDimensional
    (K := K) n seed
@[reducible]
noncomputable local instance
    cyclotomicKummerNormDescent_kummerAlgebraOverBase
    (n : ℕ+)
    (seed : Finset (HeightOneSpectrum (𝓞 K))) :
    Algebra K
      (cyclotomicFullSUnitKummerExtension (K := K) n seed) :=
  ((algebraMap
      (CyclotomicField (n : ℕ) K)
      (cyclotomicFullSUnitKummerExtension (K := K) n seed)).comp
    (algebraMap K (CyclotomicField (n : ℕ) K))).toAlgebra
Lean source · statement
theorem
    cyclotomicKummerNormDescent_kummerScalarTower
    (n : ℕ+)
    (seed : Finset (HeightOneSpectrum (𝓞 K))) :
    IsScalarTower K
      (CyclotomicField (n : ℕ) K)
      (cyclotomicFullSUnitKummerExtension (K := K) n seed)
instance

cyclotomicKummerNormDescent_kummerFiniteDimensionalOverBase

L390 ↗
GlobalClassFieldTheory.GlobalClassFields.cyclotomicKummerNormDescent_kummerFiniteDimensionalOverBase
Source context 13 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
open KummerTheory
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]
local instance cyclotomicKummerNormDescent_neZero
    (n : ℕ+) : NeZero (n : ℕ) :=
  ⟨n.ne_zero⟩
noncomputable local instance
    cyclotomicKummerNormDescent_cyclotomicFiniteDimensional
    (n : ℕ+) :
    FiniteDimensional K (CyclotomicField (n : ℕ) K) :=
  IsCyclotomicExtension.finiteDimensional
    {(n : ℕ)} K (CyclotomicField (n : ℕ) K)
noncomputable local instance
    cyclotomicKummerNormDescent_cyclotomicIsGalois
    (n : ℕ+) :
    IsGalois K (CyclotomicField (n : ℕ) K) :=
  IsCyclotomicExtension.isGalois
    {(n : ℕ)} K (CyclotomicField (n : ℕ) K)
noncomputable local instance
    cyclotomicKummerNormDescent_kummerFiniteDimensional
    (n : ℕ+)
    (seed : Finset (HeightOneSpectrum (𝓞 K))) :
    FiniteDimensional
      (CyclotomicField (n : ℕ) K)
      (cyclotomicFullSUnitKummerExtension (K := K) n seed) :=
  cyclotomicFullSUnitKummerExtension_finiteDimensional
    (K := K) n seed
@[reducible]
noncomputable local instance
    cyclotomicKummerNormDescent_kummerAlgebraOverBase
    (n : ℕ+)
    (seed : Finset (HeightOneSpectrum (𝓞 K))) :
    Algebra K
      (cyclotomicFullSUnitKummerExtension (K := K) n seed) :=
  ((algebraMap
      (CyclotomicField (n : ℕ) K)
      (cyclotomicFullSUnitKummerExtension (K := K) n seed)).comp
    (algebraMap K (CyclotomicField (n : ℕ) K))).toAlgebra
Lean source · statement
instance
    cyclotomicKummerNormDescent_kummerFiniteDimensionalOverBase
    (n : ℕ+)
    (seed : Finset (HeightOneSpectrum (𝓞 K))) :
    FiniteDimensional K
      (cyclotomicFullSUnitKummerExtension (K := K) n seed)
theorem

cyclotomicFullSUnitKummerExtension_ideleClassNormRange_le_powerLocalUnit

L409 ↗
GlobalClassFieldTheory.GlobalClassFields.cyclotomicFullSUnitKummerExtension_ideleClassNormRange_le_powerLocalUnit
Documentation

The norm range of the actual cyclotomic full S-unit Kummer extension, viewed as a finite extension of K, lies in the power-local-unit subgroup on the enlarged base support. This is the pointwise tower-norm step in the roots-of-unity descent.

Source context 14 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
open KummerTheory
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]
local instance cyclotomicKummerNormDescent_neZero
    (n : ℕ+) : NeZero (n : ℕ) :=
  ⟨n.ne_zero⟩
noncomputable local instance
    cyclotomicKummerNormDescent_cyclotomicFiniteDimensional
    (n : ℕ+) :
    FiniteDimensional K (CyclotomicField (n : ℕ) K) :=
  IsCyclotomicExtension.finiteDimensional
    {(n : ℕ)} K (CyclotomicField (n : ℕ) K)
noncomputable local instance
    cyclotomicKummerNormDescent_cyclotomicIsGalois
    (n : ℕ+) :
    IsGalois K (CyclotomicField (n : ℕ) K) :=
  IsCyclotomicExtension.isGalois
    {(n : ℕ)} K (CyclotomicField (n : ℕ) K)
noncomputable local instance
    cyclotomicKummerNormDescent_kummerFiniteDimensional
    (n : ℕ+)
    (seed : Finset (HeightOneSpectrum (𝓞 K))) :
    FiniteDimensional
      (CyclotomicField (n : ℕ) K)
      (cyclotomicFullSUnitKummerExtension (K := K) n seed) :=
  cyclotomicFullSUnitKummerExtension_finiteDimensional
    (K := K) n seed
@[reducible]
noncomputable local instance
    cyclotomicKummerNormDescent_kummerAlgebraOverBase
    (n : ℕ+)
    (seed : Finset (HeightOneSpectrum (𝓞 K))) :
    Algebra K
      (cyclotomicFullSUnitKummerExtension (K := K) n seed) :=
  ((algebraMap
      (CyclotomicField (n : ℕ) K)
      (cyclotomicFullSUnitKummerExtension (K := K) n seed)).comp
    (algebraMap K (CyclotomicField (n : ℕ) K))).toAlgebra
noncomputable local instance
    cyclotomicKummerNormDescent_kummerFiniteDimensionalOverBase
    (n : ℕ+)
    (seed : Finset (HeightOneSpectrum (𝓞 K))) :
    FiniteDimensional K
      (cyclotomicFullSUnitKummerExtension (K := K) n seed) :=
  by
    let : IsScalarTower K
        (CyclotomicField (n : ℕ) K)
        (cyclotomicFullSUnitKummerExtension (K := K) n seed) :=
      cyclotomicKummerNormDescent_kummerScalarTower (K := K) n seed
    exact FiniteDimensional.trans K
      (CyclotomicField (n : ℕ) K)
      (cyclotomicFullSUnitKummerExtension (K := K) n seed)
Lean source · full declaration
theorem
    cyclotomicFullSUnitKummerExtension_ideleClassNormRange_le_powerLocalUnit
    (n : ℕ+)
    (hn : 1 < (n : ℕ))
    (seed : Finset (HeightOneSpectrum (𝓞 K))) :
    let E := cyclotomicFullSUnitKummerExtension (K := K) n seed
    letI : NumberField E :=
      cyclotomicKummerNormDescent_kummerNumberField (K := K) n seed
    (_root_.ideleClassNorm K E).range ≤
      ideleClassPowerLocalUnitSubgroup
        (K := K) n
        (cyclotomicKummerNormSupport (K := K) n seed) ∅ := by
  classical
  dsimp only
  let C := CyclotomicField (n : ℕ) K
  let S := cyclotomicKummerNormSupport (K := K) n seed
  let S' := cyclotomicKummerNormSupportAbove (K := K) n seed
  let E := cyclotomicFullSUnitKummerExtension (K := K) n seed
  let : IsScalarTower K C E :=
    cyclotomicKummerNormDescent_kummerScalarTower (K := K) n seed
  let : NumberField E :=
    cyclotomicKummerNormDescent_kummerNumberField (K := K) n seed
  have hNormC :
      (_root_.ideleClassNorm C E).range =
        ideleClassPowerLocalUnitSubgroup (K := C) n S' ∅ :=
    cyclotomicFullSUnitKummerExtension_cyclotomicNormRange
      (K := K) n hn seed
  have hSupport :
      ∀ W : HeightOneSpectrum (𝓞 C),
        W ∈ S' ↔ finitePlaceBelow (K := K) W ∈ S := by
    intro W
    simpa only [C, S, S'] using
      (mem_cyclotomicKummerNormSupportAbove_iff
        (K := K) n seed W)
  rintro _ ⟨c, rfl⟩
  rw [← ordinaryIdeleClassNorm_tower
    (K := K) (M := C) (L := E) c]
  apply
    (ideleClassNorm_map_powerLocalUnitSubgroup_le_of_supports_above
      (K := K) (L := C) n S S' hSupport)
  refine ⟨_root_.ideleClassNorm C E c, ?_, rfl⟩
  rw [← hNormC]
  exact ⟨c, rfl⟩
theorem

cyclotomicFullSUnitKummerFiniteNormalClosure_ideleClassNormRange_le_powerLocalUnit

L457 ↗
GlobalClassFieldTheory.GlobalClassFields.cyclotomicFullSUnitKummerFiniteNormalClosure_ideleClassNormRange_le_powerLocalUnit
Documentation

Passing to the finite normal closure produces an actual finite Galois extension of K whose norm range is still contained in the prescribed power-local-unit subgroup. This is the finite Galois norm neighbourhood constructed in the roots-of-unity-free case.

Source context 14 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
open KummerTheory
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type} [Field K] [NumberField K]
local instance cyclotomicKummerNormDescent_neZero
    (n : ℕ+) : NeZero (n : ℕ) :=
  ⟨n.ne_zero⟩
noncomputable local instance
    cyclotomicKummerNormDescent_cyclotomicFiniteDimensional
    (n : ℕ+) :
    FiniteDimensional K (CyclotomicField (n : ℕ) K) :=
  IsCyclotomicExtension.finiteDimensional
    {(n : ℕ)} K (CyclotomicField (n : ℕ) K)
noncomputable local instance
    cyclotomicKummerNormDescent_cyclotomicIsGalois
    (n : ℕ+) :
    IsGalois K (CyclotomicField (n : ℕ) K) :=
  IsCyclotomicExtension.isGalois
    {(n : ℕ)} K (CyclotomicField (n : ℕ) K)
noncomputable local instance
    cyclotomicKummerNormDescent_kummerFiniteDimensional
    (n : ℕ+)
    (seed : Finset (HeightOneSpectrum (𝓞 K))) :
    FiniteDimensional
      (CyclotomicField (n : ℕ) K)
      (cyclotomicFullSUnitKummerExtension (K := K) n seed) :=
  cyclotomicFullSUnitKummerExtension_finiteDimensional
    (K := K) n seed
@[reducible]
noncomputable local instance
    cyclotomicKummerNormDescent_kummerAlgebraOverBase
    (n : ℕ+)
    (seed : Finset (HeightOneSpectrum (𝓞 K))) :
    Algebra K
      (cyclotomicFullSUnitKummerExtension (K := K) n seed) :=
  ((algebraMap
      (CyclotomicField (n : ℕ) K)
      (cyclotomicFullSUnitKummerExtension (K := K) n seed)).comp
    (algebraMap K (CyclotomicField (n : ℕ) K))).toAlgebra
noncomputable local instance
    cyclotomicKummerNormDescent_kummerFiniteDimensionalOverBase
    (n : ℕ+)
    (seed : Finset (HeightOneSpectrum (𝓞 K))) :
    FiniteDimensional K
      (cyclotomicFullSUnitKummerExtension (K := K) n seed) :=
  by
    let : IsScalarTower K
        (CyclotomicField (n : ℕ) K)
        (cyclotomicFullSUnitKummerExtension (K := K) n seed) :=
      cyclotomicKummerNormDescent_kummerScalarTower (K := K) n seed
    exact FiniteDimensional.trans K
      (CyclotomicField (n : ℕ) K)
      (cyclotomicFullSUnitKummerExtension (K := K) n seed)
Lean source · full declaration
theorem
    cyclotomicFullSUnitKummerFiniteNormalClosure_ideleClassNormRange_le_powerLocalUnit
    (n : ℕ+)
    (hn : 1 < (n : ℕ))
    (seed : Finset (HeightOneSpectrum (𝓞 K))) :
    let E := cyclotomicFullSUnitKummerExtension (K := K) n seed
    letI : NumberField E :=
      cyclotomicKummerNormDescent_kummerNumberField (K := K) n seed
    let F := finiteNormalClosure K E
    (_root_.ideleClassNorm K F).range ≤
      ideleClassPowerLocalUnitSubgroup
        (K := K) n
        (cyclotomicKummerNormSupport (K := K) n seed) ∅ := by
  classical
  dsimp only
  let E := cyclotomicFullSUnitKummerExtension (K := K) n seed
  let : NumberField E :=
    cyclotomicKummerNormDescent_kummerNumberField (K := K) n seed
  let F := finiteNormalClosure K E
  calc
    (_root_.ideleClassNorm K F).range ≤
        (_root_.ideleClassNorm K E).range := by
      simpa only [F] using
        (finiteNormalClosure_ideleClassNorm_range_le_source
          (K := K) (L := E))
    _ ≤ ideleClassPowerLocalUnitSubgroup
          (K := K) n
          (cyclotomicKummerNormSupport (K := K) n seed) ∅ := by
      simpa only [E] using
        (cyclotomicFullSUnitKummerExtension_ideleClassNormRange_le_powerLocalUnit
          (K := K) n hn seed)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.