Module

FullSUnitKummerExtension.lean

Nyll.ClassFieldTheory.KummerTheory.Concrete.SUnitPreparation.FullSUnitKummerExtension

13 declarations indexed from sourceView source ↗

Module documentation

The full S-unit Kummer extension

Construction, finite generation, Galois structure, cardinality, and coordinates for the Kummer extension generated by all S-unit roots.

Imports2

Imported by3

def

fullSUnitKummerExtension

L31 ↗

KummerTheory.fullSUnitKummerExtension

Documentation

The actual field N = K(√[n]{Kˢ}) in a fixed separable closure.

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]

Lean source · statement

def fullSUnitKummerExtension
    {Omega : Type*} [Field Omega] [Algebra K Omega]
    (n : ℕ+)
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    IntermediateField K Omega

theorem

exists_sUnitRoot_adjoin_eq_of_mem_fullSUnitKummerRootSet

L45 ↗

KummerTheory.exists_sUnitRoot_adjoin_eq_of_mem_fullSUnitKummerRootSet

Documentation

Every root used to generate the full S-unit Kummer extension can be rescaled by an element of Kˣ to become the root of an actual S-unit. The rescaling does not change the simple intermediate field that it generates. This is the source-producing step needed to apply the local unramified Kummer criterion to every generator of the full extension.

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]

Lean source · statement

theorem exists_sUnitRoot_adjoin_eq_of_mem_fullSUnitKummerRootSet
    {Omega : Type*} [Field Omega] [Algebra K Omega]
    (n : ℕ+)
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    {beta : Omega}
    (hbeta :
      beta ∈
        KummerTheory.kummerRootSet
          (K := K) (Omega := Omega) n
          (fullSUnitKummerSubgroup (K := K) n S).1) :
    ∃ (u : SUnitGroup (K := K) S) (alpha : Omegaˣ),
      alpha ^ (n : ℕ) =
          Units.map (algebraMap K Omega).toMonoidHom u.1 ∧
        IntermediateField.adjoin K {(alpha : Omega)} =
          IntermediateField.adjoin K {beta}

theorem

fullSUnitKummerExtension_isGalois

L131 ↗

KummerTheory.fullSUnitKummerExtension_isGalois

Documentation

The field N = K(√[n]{Kˢ}) is Galois over K.

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]

Lean source · statement

theorem fullSUnitKummerExtension_isGalois
    {Omega : Type*} [Field Omega] [Algebra K Omega]
    [IsSepClosure K Omega]
    (n : ℕ+)
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    IsGalois K
      (fullSUnitKummerExtension (K := K) (Omega := Omega) n S)

theorem

finite_fullSUnitKummerExtension_galois

L142 ↗

KummerTheory.finite_fullSUnitKummerExtension_galois

Documentation

The Galois group of N/K is finite.

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]

Lean source · statement

theorem finite_fullSUnitKummerExtension_galois
    {Omega : Type*} [Field Omega] [Algebra K Omega]
    [IsSepClosure K Omega]
    (n : ℕ+) (hn : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    Finite
      Gal(fullSUnitKummerExtension
        (K := K) (Omega := Omega) n S/K)

theorem

fullSUnitKummerExtension_finiteDimensional

L174 ↗

KummerTheory.fullSUnitKummerExtension_finiteDimensional

Documentation

The extension N = K(√[n]{Kˢ}) is finite-dimensional.

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]

Lean source · statement

theorem fullSUnitKummerExtension_finiteDimensional
    {Omega : Type*} [Field Omega] [Algebra K Omega]
    [IsSepClosure K Omega]
    (n : ℕ+) (hn : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    FiniteDimensional K
      (fullSUnitKummerExtension
        (K := K) (Omega := Omega) n S)

theorem

exists_finset_fullSUnitKummerRootSet_adjoin_eq

L197 ↗

KummerTheory.exists_finset_fullSUnitKummerRootSet_adjoin_eq

Documentation

A finite set of the actual Kummer roots generates the full S-unit Kummer extension. Finiteness is obtained from Kummer duality, and the finite root set is extracted from a primitive element of the resulting finite separable extension.

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]

Lean source · statement

theorem exists_finset_fullSUnitKummerRootSet_adjoin_eq
    {Omega : Type*} [Field Omega] [Algebra K Omega]
    [IsSepClosure K Omega]
    (n : ℕ+) (hn : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    ∃ T : Finset Omega,
      (T : Set Omega) ⊆
          KummerTheory.kummerRootSet
            (K := K) (Omega := Omega) n
            (fullSUnitKummerSubgroup (K := K) n S).1 ∧
        IntermediateField.adjoin K (T : Set Omega) =
          fullSUnitKummerExtension
            (K := K) (Omega := Omega) n S

theorem

exists_finset_fullSUnitKummerExtensionRoots_adjoin_eq_top

L262 ↗

KummerTheory.exists_finset_fullSUnitKummerExtensionRoots_adjoin_eq_top

Documentation

The finite generating roots may be regarded as elements of the full Kummer extension itself; internally they adjoin to the top field. This is the form consumed by finite inertia-restriction arguments.

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]

Lean source · full declaration

theorem exists_finset_fullSUnitKummerExtensionRoots_adjoin_eq_top
    {Omega : Type*} [Field Omega] [Algebra K Omega]
    [IsSepClosure K Omega]
    (n : ℕ+) (hn : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    let E :=
      fullSUnitKummerExtension
        (K := K) (Omega := Omega) n S
    ∃ T : Finset E,
      (∀ x : E, x ∈ T →
        (x : Omega) ∈
          KummerTheory.kummerRootSet
            (K := K) (Omega := Omega) n
            (fullSUnitKummerSubgroup (K := K) n S).1) ∧
        IntermediateField.adjoin K (T : Set E) = ⊤ := by
  classical
  dsimp only
  let E :=
    fullSUnitKummerExtension
      (K := K) (Omega := Omega) n S
  let _ : IsGalois K E :=
    fullSUnitKummerExtension_isGalois
      (K := K) (Omega := Omega) n S
  let _ : FiniteDimensional K E :=
    fullSUnitKummerExtension_finiteDimensional
      (K := K) (Omega := Omega) n hn hmu S
  obtain ⟨theta, htheta⟩ :=
    Field.exists_primitive_element K E
  obtain ⟨T₀, hT₀, hthetaT₀⟩ :=
    KummerTheory.exists_finset_kummerRootSet_of_mem_kummerRadicalExtension
      n (fullSUnitKummerSubgroup (K := K) n S).1 theta.property
  have hT₀E :
      IntermediateField.adjoin K (T₀ : Set Omega) ≤ E := by
    apply IntermediateField.adjoin_le_iff.mpr
    intro x hx
    apply IntermediateField.subset_adjoin K
      (KummerTheory.kummerRootSet
        (K := K) (Omega := Omega) n
        (fullSUnitKummerSubgroup (K := K) n S).1)
    exact hT₀ hx
  let toE : ↥T₀ → E :=
    fun x => ⟨x.1,
      IntermediateField.subset_adjoin K
        (KummerTheory.kummerRootSet
          (K := K) (Omega := Omega) n
          (fullSUnitKummerSubgroup (K := K) n S).1)
        (hT₀ x.property)⟩
  let T : Finset E :=
    Finset.univ.image toE
  have hTroot :
      ∀ x : E, x ∈ T →
        (x : Omega) ∈
          KummerTheory.kummerRootSet
            (K := K) (Omega := Omega) n
            (fullSUnitKummerSubgroup (K := K) n S).1 := by
    intro x hx
    obtain ⟨y, _, hy⟩ :=
      Finset.mem_image.mp hx
    rw [← hy]
    exact hT₀ y.property
  refine ⟨T, hTroot, ?_⟩
  let R := IntermediateField.adjoin K (T : Set E)
  have hlift :
      ∀ (x : Omega)
        (hx :
          x ∈ IntermediateField.adjoin K (T₀ : Set Omega)),
        (⟨x, hT₀E hx⟩ : E) ∈ R := by
    intro x hx
    exact IntermediateField.adjoin_induction K
      (p := fun y hy => (⟨y, hT₀E hy⟩ : E) ∈ R)
      (fun y hy => by
        let yT : ↥T₀ := ⟨y, hy⟩
        have hyT : toE yT ∈ T := by
          apply Finset.mem_image.mpr
          exact ⟨yT, Finset.mem_univ yT, rfl⟩
        have hmem : toE yT ∈ R :=
          IntermediateField.subset_adjoin K
            (T : Set E) hyT
        simpa only [toE, yT] using hmem)
      (fun a => by
        exact R.algebraMap_mem a)
      (fun _ _ _ _ ihx ihy => by
        simpa using R.add_mem ihx ihy)
      (fun _ _ ihx => by
        convert R.inv_mem ihx using 1)
      (fun _ _ _ _ ihx ihy => by
        simpa using R.mul_mem ihx ihy)
      hx
  have hthetaR : theta ∈ R := by
    simpa using hlift theta.1 hthetaT₀
  apply top_unique
  rw [← htheta]
  apply IntermediateField.adjoin_le_iff.mpr
  intro x hx
  rw [Set.mem_singleton_iff] at hx
  subst x
  exact hthetaR

theorem

card_fullSUnitKummerExtension_galois

L362 ↗

KummerTheory.card_fullSUnitKummerExtension_galois

Documentation

The Galois group of N/K has cardinality n ^ s.

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]

Lean source · statement

theorem card_fullSUnitKummerExtension_galois
    {Omega : Type*} [Field Omega] [Algebra K Omega]
    [IsSepClosure K Omega]
    (n : ℕ+) (hn : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    Nat.card
        Gal(fullSUnitKummerExtension
          (K := K) (Omega := Omega) n S/K) =
      (n : ℕ) ^ totalPlaceCard (K := K) S

theorem

fullSUnitKummerExtension_galois_pow_eq_one

L398 ↗

KummerTheory.fullSUnitKummerExtension_galois_pow_eq_one

Documentation

Every automorphism of the full S-unit Kummer extension has n-th power one.

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]

Lean source · statement

theorem fullSUnitKummerExtension_galois_pow_eq_one
    {Omega : Type*} [Field Omega] [Algebra K Omega]
    [IsSepClosure K Omega]
    (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (sigma :
      Gal(fullSUnitKummerExtension
        (K := K) (Omega := Omega) n S/K)) :
    sigma ^ (n : ℕ) = 1

def

chosenFullSUnitKummerExtensionGaloisEquivSUnitQuotient

L413 ↗

KummerTheory.chosenFullSUnitKummerExtensionGaloisEquivSUnitQuotient

Documentation

A chosen Kummer-duality equivalence identifies the Galois group of the full S-unit extension with the actual S-unit quotient.

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]

Lean source · statement

def
    chosenFullSUnitKummerExtensionGaloisEquivSUnitQuotient
    {Omega : Type*} [Field Omega] [Algebra K Omega]
    [IsSepClosure K Omega]
    (n : ℕ+) (hn : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    Gal(fullSUnitKummerExtension
        (K := K) (Omega := Omega) n S/K) ≃*
      SUnitGroup (K := K) S ⧸
        (powMonoidHom (n : ℕ) :
          SUnitGroup (K := K) S →*
            SUnitGroup (K := K) S).range

def

fullSUnitKummerExtensionGaloisCoordinates

L450 ↗

KummerTheory.fullSUnitKummerExtensionGaloisCoordinates

Documentation

ZMod n coordinates derived from the chosen duality equivalence on the Galois group of the full S-unit Kummer extension.

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]

Lean source · statement

def fullSUnitKummerExtensionGaloisCoordinates
    {Omega : Type*} [Field Omega] [Algebra K Omega]
    [IsSepClosure K Omega]
    (n : ℕ+) (hn : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    Gal(fullSUnitKummerExtension
        (K := K) (Omega := Omega) n S/K) ≃*
      Multiplicative (ZMod (n : ℕ)) ×
        Multiplicative
          (Fin (SUnitGroup.logRank (K := K) S) →
            ZMod (n : ℕ))

def

fullSUnitKummerExtensionGaloisEquivPiZMod

L471 ↗

KummerTheory.fullSUnitKummerExtensionGaloisEquivPiZMod

Documentation

The Galois group of the full S-unit Kummer extension, with one coordinate for every finite place in S and every infinite place. This chosen coordinate form is consumed by the global norm-index theorem.

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]

Lean source · statement

def fullSUnitKummerExtensionGaloisEquivPiZMod
    {Omega : Type*} [Field Omega] [Algebra K Omega]
    [IsSepClosure K Omega]
    (n : ℕ+) (hn : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    Gal(fullSUnitKummerExtension
        (K := K) (Omega := Omega) n S/K) ≃*
      (Fin (totalPlaceCard (K := K) S) →
        Multiplicative (ZMod (n : ℕ)))

theorem

fullSUnitKummerExtension_galois_moduleFree

L512 ↗

KummerTheory.fullSUnitKummerExtension_galois_moduleFree

Documentation

With its canonical exponent-n module structure, the full S-unit Kummer Galois group is a free ZMod n-module.

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]

Lean source · full declaration

theorem fullSUnitKummerExtension_galois_moduleFree
    {Omega : Type*} [Field Omega] [Algebra K Omega]
    [IsSepClosure K Omega]
    (n : ℕ+) (hn : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    letI : IsMulCommutative
        Gal(fullSUnitKummerExtension
          (K := K) (Omega := Omega) n S/K) :=
      KummerTheory.kummerRadicalExtension_isMulCommutative
        n hmu (fullSUnitKummerSubgroup (K := K) n S).1
    letI : Module (ZMod (n : ℕ))
        (Additive
          Gal(fullSUnitKummerExtension
            (K := K) (Omega := Omega) n S/K)) :=
      additiveZModModuleOfPowEqOne (n : ℕ)
        (fullSUnitKummerExtension_galois_pow_eq_one
          (K := K) (Omega := Omega) n hmu S)
    Module.Free (ZMod (n : ℕ))
      (Additive
        Gal(fullSUnitKummerExtension
          (K := K) (Omega := Omega) n S/K)) := by
  let G :=
    Gal(fullSUnitKummerExtension
      (K := K) (Omega := Omega) n S/K)
  let _ : IsMulCommutative G :=
    KummerTheory.kummerRadicalExtension_isMulCommutative
      n hmu (fullSUnitKummerSubgroup (K := K) n S).1
  let _ : Module (ZMod (n : ℕ)) (Additive G) :=
    additiveZModModuleOfPowEqOne (n : ℕ)
      (fullSUnitKummerExtension_galois_pow_eq_one
        (K := K) (Omega := Omega) n hmu S)
  let e :
      Additive G ≃ₗ[ZMod (n : ℕ)]
        ZMod (n : ℕ) ×
          (Fin (SUnitGroup.logRank (K := K) S) →
            ZMod (n : ℕ)) :=
    additiveCoordinatesLinearEquiv (n : ℕ)
      (fullSUnitKummerExtensionGaloisCoordinates
        (K := K) (Omega := Omega) n hn hmu S)
  exact Module.Free.of_equiv e.symm

Module documentation

The full S-unit Kummer extension

Declarations