Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.KummerAdjoinRoot

Module documentation

A cyclic Kummer extension from an Eisenstein parameter

The extension is the actual AdjoinRoot (X ^ r - C π) over the fraction field. Eisenstein irreducibility supplies its field structure and power basis; a primitive root of unity supplies the splitting field and Galois property. Its integral minimal polynomial is identified before any valuation is chosen, so the basis is ready for EisensteinResidue.

theorem

exists_cyclic_kummer_extension_of_prime_parameter

L37 ↗

ValuationTheory.DiscreteValuationField.exists_cyclic_kummer_extension_of_prime_parameter

Documentation

A prime parameter and a primitive r-th root of unity produce an actual cyclic degree-r extension with the displayed integral minimal polynomial. The coefficient-ring algebra and its tower are outputs of the construction, alongside the fraction-field power basis.

Source context 4 commands

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

namespace ValuationTheory.DiscreteValuationField
open Polynomial
open scoped Polynomial
universe u v

Lean source · statement

theorem exists_cyclic_kummer_extension_of_prime_parameter
    (R : Type u) (K : Type v)
    [CommRing R] [IsDomain R] [IsIntegrallyClosed R]
    [Field K] [Algebra R K] [IsFractionRing R K]
    (π : R) (hπ : Prime π) (r : ℕ) [Fact r.Prime]
    (ζ : K) (hζ : IsPrimitiveRoot ζ r) :
    ∃ (L : Type v) (_ : Field L) (_ : Algebra K L)
      (_ : Algebra R L) (_ : IsScalarTower R K L) (B : PowerBasis K L),
      Module.finrank K L = r ∧
      B.gen ^ r = algebraMap R L π ∧
      minpoly K B.gen = X ^ r - C (algebraMap R K π) ∧
      minpoly R B.gen = X ^ r - C π ∧
      IsGalois K L ∧ IsCyclic (L ≃ₐ[K] L)

Module documentation

A cyclic Kummer extension from an Eisenstein parameter

Declarations

exists_cyclic_kummer_extension_of_prime_parameter