NYLL
Module

FinitePlaceDecomposition.lean

Nyll.ClassFieldTheory.KummerTheory.Concrete.FinitePlaceDecomposition
2 declarations indexed from sourceView source ↗

Module documentation

Kummer radicals and finite-place decomposition fields

For a finite Galois extension containing an n-th root β of a base-field unit a, this file identifies the local n-th-power condition on a with membership of β in the decomposition field.

The proof uses the canonical comparison between the two models of the finite-place completion and the algebraic localization realization of the decomposition field. The only Kummer input is the usual fact that two roots with the same n-th power differ by an n-th root of unity.

Imports4
Imported by3

Declarations

theorem

kummerRadicand_root_mem_decompositionFixedField_of_mem_nthPowerSubgroup

L47 ↗
KummerTheory.kummerRadicand_root_mem_decompositionFixedField_of_mem_nthPowerSubgroup
Documentation

If a Kummer radicand is an n-th power in an absolute-value completion, its chosen root lies in the corresponding decomposition field. This is the completion-level source behind both the finite and archimedean localization arguments.

Source context 9 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
noncomputable section
namespace KummerTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [NumberField K] [FiniteDimensional K L] in
Lean source · statement
theorem
    kummerRadicand_root_mem_decompositionFixedField_of_mem_nthPowerSubgroup
    (vK : AbsoluteValue K ℝ)
    (hvK : vK.IsNontrivial)
    (w : AbsoluteValueExtension vK L)
    (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (a : Kˣ) (beta : Lˣ)
    (hbeta :
      beta ^ (n : ℕ) =
        Units.map (algebraMap K L).toMonoidHom a)
    (ha :
      Units.map
            (algebraMap K vK.Completion).toMonoidHom a ∈
        (powMonoidHom (n : ℕ) :
          vK.Completionˣ →* vK.Completionˣ).range) :
    (beta : L) ∈
      IntermediateField.fixedField
        (absoluteValueDecompositionGroup K w.1)
theorem

finitePlaceKummerRadicand_mem_nthPowerSubgroup_iff_root_mem_decompositionFixedField

L174 ↗
KummerTheory.finitePlaceKummerRadicand_mem_nthPowerSubgroup_iff_root_mem_decompositionFixedField
Documentation

A Kummer radicand is an n-th power in the finite-place completion exactly when its chosen root belongs to the decomposition field at the chosen extension of that place.

Source context 9 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
noncomputable section
namespace KummerTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [FiniteDimensional K L] in
Lean source · statement
theorem
    finitePlaceKummerRadicand_mem_nthPowerSubgroup_iff_root_mem_decompositionFixedField
    (v : HeightOneSpectrum (𝓞 K))
    (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (a : Kˣ) (beta : Lˣ)
    (hbeta :
      beta ^ (n : ℕ) =
        Units.map (algebraMap K L).toMonoidHom a) :
    Units.map
          (algebraMap K (v.adicCompletion K)).toMonoidHom a ∈
        (powMonoidHom (n : ℕ) :
          (v.adicCompletion K)ˣ →*
            (v.adicCompletion K)ˣ).range ↔
      (beta : L) ∈
        IntermediateField.fixedField
          (absoluteValueDecompositionGroup K
            (chosenFinitePlaceExtension (L := L) v).1)

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