Module

FiniteRadicalSupport.lean

Nyll.ClassFieldTheory.KummerTheory.Concrete.SUnitPreparation.FiniteRadicalSupport

19 declarations indexed from sourceView source ↗

Module documentation

Finite support for Kummer radicals

A chosen finite enlargement of places containing representatives of every class in a finite Kummer radical.

Imports1

Nyll.ClassFieldTheory.KummerTheory.Concrete.SUnitPreparation.SUnitLocalPowerKernel

Imported by6

def

sUnitFiniteKummerRadical

L31 ↗

KummerTheory.sUnitFiniteKummerRadical

Documentation

The finite Kummer radical D ∩ Kˢ, where D = Lˣⁿ ∩ 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

def sUnitFiniteKummerRadical
    {L : Type*} [Field L] [Algebra K L]
    (n : ℕ+)
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    Subgroup Kˣ

theorem

mem_sUnitFiniteKummerRadical_iff

L43 ↗

KummerTheory.mem_sUnitFiniteKummerRadical_iff

Documentation

An S-unit belongs to the finite Kummer radical exactly when it has an n-th root in L.

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 mem_sUnitFiniteKummerRadical_iff
    {L : Type*} [Field L] [Algebra K L]
    (n : ℕ+)
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (x : Kˣ) :
    x ∈ sUnitFiniteKummerRadical (K := K) (L := L) n S ↔
      x ∈ SUnitGroup (K := K) S ∧
        ∃ beta : Lˣ,
          beta ^ (n : ℕ) =
            Units.map (algebraMap K L).toMonoidHom x

def

sUnitKummerSubgroup

L57 ↗

KummerTheory.sUnitKummerSubgroup

Documentation

Adjoin the ambient n-th powers to D ∩ Kˢ, producing an admissible object on the subgroup side of Kummer theory.

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 sUnitKummerSubgroup
    {L : Type*} [Field L] [Algebra K L]
    (n : ℕ+)
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    KummerTheory.KummerSubgroup K n

theorem

sUnitKummerSubgroup_le_finiteKummerRadicalSubgroup

L67 ↗

KummerTheory.sUnitKummerSubgroup_le_finiteKummerRadicalSubgroup

Documentation

The S-unit Kummer subgroup lies in the actual radical of L / 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 sUnitKummerSubgroup_le_finiteKummerRadicalSubgroup
    {L : Type*} [Field L] [Algebra K L]
    (n : ℕ+)
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    (sUnitKummerSubgroup (K := K) (L := L) n S).1 ≤
      KummerTheory.finiteKummerRadicalSubgroup
        (K := K) (L := L) n

theorem

sUnitGroup_mono

L84 ↗

KummerTheory.sUnitGroup_mono

Documentation

Enlarging the finite set of places enlarges the S-unit group.

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 sUnitGroup_mono
    {S T : Finset (HeightOneSpectrum (𝓞 K))}
    (hST : S ⊆ T) :
    SUnitGroup (K := K) S ≤ SUnitGroup (K := K) T

def

chosenUnitFiniteSupport

L95 ↗

KummerTheory.chosenUnitFiniteSupport

Documentation

A chosen finite set of places outside which a given global unit is an integral unit.

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 chosenUnitFiniteSupport (x : Kˣ) :
    Finset (HeightOneSpectrum (𝓞 K))

theorem

mem_sUnitGroup_chosenUnitFiniteSupport

L102 ↗

KummerTheory.mem_sUnitGroup_chosenUnitFiniteSupport

Documentation

A global unit is an S-unit for its chosen finite support.

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 mem_sUnitGroup_chosenUnitFiniteSupport (x : Kˣ) :
    x ∈ SUnitGroup (K := K) (chosenUnitFiniteSupport (K := K) x)

theorem

finite_chosenFiniteKummerRadicalQuotient

L133 ↗

KummerTheory.finite_chosenFiniteKummerRadicalQuotient

Documentation

The actual radical quotient of a finite Galois extension is finite. This is obtained from the concrete finite Kummer character equivalence, not supplied as a finiteness hypothesis.

Source context 7 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]
omit numberFieldK in

Lean source · statement

theorem finite_chosenFiniteKummerRadicalQuotient
    {L : Type*} [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
    Finite
      ((KummerTheory.chosenFiniteKummerRadicalDatum
        (K := K) (L := L) n).RadicalQuotient)

def

chosenFiniteKummerRadicalRepresentative

L164 ↗

KummerTheory.chosenFiniteKummerRadicalRepresentative

Documentation

A chosen representative of a class in the actual finite Kummer radical 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 chosenFiniteKummerRadicalRepresentative
    {L : Type*} [Field L] [Algebra K L]
    (n : ℕ+)
    (q :
      (KummerTheory.chosenFiniteKummerRadicalDatum
        (K := K) (L := L) n).RadicalQuotient) :
    (KummerTheory.chosenFiniteKummerRadicalDatum
      (K := K) (L := L) n).carrier

theorem

chosenFiniteKummerRadicalRepresentative_spec

L179 ↗

KummerTheory.chosenFiniteKummerRadicalRepresentative_spec

Documentation

The chosen representative maps back to the prescribed radical class.

Source context 7 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]
omit numberFieldK in

Lean source · statement

theorem chosenFiniteKummerRadicalRepresentative_spec
    {L : Type*} [Field L] [Algebra K L]
    (n : ℕ+)
    (q :
      (KummerTheory.chosenFiniteKummerRadicalDatum
        (K := K) (L := L) n).RadicalQuotient) :
    (KummerTheory.chosenFiniteKummerRadicalDatum
        (K := K) (L := L) n).radicalQuotientMk
      (chosenFiniteKummerRadicalRepresentative
        (K := K) (L := L) n q) = q

def

finiteKummerRadicalSupport

L195 ↗

KummerTheory.finiteKummerRadicalSupport

Documentation

The union of the supports of one representative of every actual Kummer radical class.

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 finiteKummerRadicalSupport
    {L : Type*} [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
    Finset (HeightOneSpectrum (𝓞 K))

def

enlargeByFiniteKummerRadicalSupport

L219 ↗

KummerTheory.enlargeByFiniteKummerRadicalSupport

Documentation

Enlarge any prescribed finite set by the finite supports needed to represent all actual Kummer radical classes by S-units.

Source context 7 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]
open scoped Classical in

Lean source · statement

def enlargeByFiniteKummerRadicalSupport
    {L : Type*} [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    Finset (HeightOneSpectrum (𝓞 K))

theorem

subset_enlargeByFiniteKummerRadicalSupport

L230 ↗

KummerTheory.subset_enlargeByFiniteKummerRadicalSupport

Documentation

The radical-support enlargement contains its starting set.

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 subset_enlargeByFiniteKummerRadicalSupport
    {L : Type*} [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    S ⊆ enlargeByFiniteKummerRadicalSupport
      (K := K) (L := L) n hmu S

theorem

chosenFiniteKummerRadicalRepresentative_mem_enlargedSUnitGroup

L243 ↗

KummerTheory.chosenFiniteKummerRadicalRepresentative_mem_enlargedSUnitGroup

Documentation

Each chosen radical representative is an S-unit after the chosen finite enlargement.

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 chosenFiniteKummerRadicalRepresentative_mem_enlargedSUnitGroup
    {L : Type*} [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (q :
      (KummerTheory.chosenFiniteKummerRadicalDatum
        (K := K) (L := L) n).RadicalQuotient) :
    (chosenFiniteKummerRadicalRepresentative
        (K := K) (L := L) n q).1 ∈
      SUnitGroup (K := K)
        (enlargeByFiniteKummerRadicalSupport
          (K := K) (L := L) n hmu S)

theorem

finiteKummerRadicalSubgroup_le_enlargedSUnitKummerSubgroup

L284 ↗

KummerTheory.finiteKummerRadicalSubgroup_le_enlargedSUnitKummerSubgroup

Documentation

After the chosen finite enlargement, the actual radical of L/K is generated by its S-unit part and the ambient n-th powers.

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 finiteKummerRadicalSubgroup_le_enlargedSUnitKummerSubgroup
    {L : Type*} [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    KummerTheory.finiteKummerRadicalSubgroup
        (K := K) (L := L) n ≤
      (sUnitKummerSubgroup
        (K := K) (L := L) n
        (enlargeByFiniteKummerRadicalSupport
          (K := K) (L := L) n hmu S)).1

theorem

enlargedSUnitKummerSubgroup_eq_finiteKummerRadicalSubgroup

L329 ↗

KummerTheory.enlargedSUnitKummerSubgroup_eq_finiteKummerRadicalSubgroup

Documentation

Exact radical identification after the chosen finite enlargement.

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 enlargedSUnitKummerSubgroup_eq_finiteKummerRadicalSubgroup
    {L : Type*} [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    (sUnitKummerSubgroup
        (K := K) (L := L) n
        (enlargeByFiniteKummerRadicalSupport
          (K := K) (L := L) n hmu S)).1 =
      KummerTheory.finiteKummerRadicalSubgroup
        (K := K) (L := L) n

theorem

sUnitKummerSubgroup_le_fullSUnitKummerSubgroup

L351 ↗

KummerTheory.sUnitKummerSubgroup_le_fullSUnitKummerSubgroup

Documentation

The S-unit radical subgroup belonging to an extension is contained in the full S-unit Kummer subgroup.

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 sUnitKummerSubgroup_le_fullSUnitKummerSubgroup
    {L : Type*} [Field L] [Algebra K L]
    (n : ℕ+)
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    (sUnitKummerSubgroup (K := K) (L := L) n S).1 ≤
      (fullSUnitKummerSubgroup (K := K) n S).1

theorem

kummerRadicalExtension_mono

L363 ↗

KummerTheory.kummerRadicalExtension_mono

Documentation

Monotonicity of the concrete radical-extension construction.

Source context 7 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]
omit numberFieldK in

Lean source · statement

theorem kummerRadicalExtension_mono
    {Omega : Type*} [Field Omega] [Algebra K Omega]
    (n : ℕ+)
    {Delta Gamma : Subgroup Kˣ}
    (h : Delta ≤ Gamma) :
    KummerTheory.kummerRadicalExtension
        (K := K) (Omega := Omega) n Delta ≤
      KummerTheory.kummerRadicalExtension
        (K := K) (Omega := Omega) n Gamma

theorem

kummerRadicalExtension_enlargedSUnitKummerSubgroup_eq

L381 ↗

KummerTheory.kummerRadicalExtension_enlargedSUnitKummerSubgroup_eq

Documentation

Kummer generation of an abelian exponent-n extension from the S-unit radical supplied by the chosen finite enlargement.

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 kummerRadicalExtension_enlargedSUnitKummerSubgroup_eq
    {Omega : Type*} [Field Omega] [Algebra K Omega]
    [IsSepClosure K Omega]
    (E : IntermediateField K Omega)
    [FiniteDimensional K E] [IsGalois K E]
    [IsMulCommutative Gal(E/K)]
    (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (hexponent : ∀ sigma : Gal(E/K), sigma ^ (n : ℕ) = 1)
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    KummerTheory.kummerRadicalExtension
        (K := K) (Omega := Omega) n
        (sUnitKummerSubgroup
          (K := K) (L := E) n
          (enlargeByFiniteKummerRadicalSupport
            (K := K) (L := E) n hmu S)).1 =
      E

Module documentation

Finite support for Kummer radicals

Declarations