NYLL
Module

EisensteinPolynomial.lean

Nyll.ValuedFieldTheory.LocalField.Padic.Cyclotomic.TotallyRamified.EisensteinPolynomial
16 declarations indexed from sourceView source ↗

Module documentation

The Eisenstein polynomial of the p-power cyclotomic extension

For a primitive p ^ m-th root of unity ζ, with m > 0, the local cyclotomic calculation proves that ℚ_[p](ζ) / ℚ_[p] is totally ramified of degree φ (p ^ m), identifies its Galois group with (ZMod (p ^ m))ˣ, identifies its valuation ring with ℤ_[p][ζ], and shows that 1 - ζ is a prime element of norm p.

The source is the translated cyclotomic Eisenstein polynomial Φ_{p^(k+1)}(X + 1). We first transport its integral Eisenstein criterion to the actual p-adic integer ring; no irreducibility or ramification conclusion is assumed.

Imports6
Imported by3

Declarations

theorem

padicCyclotomicTotallyRamified_norm_isUnit_iff

L41 ↗
AlgebraicNumberTheory.Valuations.padicCyclotomicTotallyRamified_norm_isUnit_iff
Source context 6 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open Polynomial
open scoped Polynomial
universe u
Lean source · statement
theorem padicCyclotomicTotallyRamified_norm_isUnit_iff
    {R A : Type*} [CommRing R] [CommRing A] [Algebra R A]
    [Module.Finite R A] [Module.Free R A] (x : A) :
    IsUnit (Algebra.norm R x) ↔ IsUnit x
def

padicCyclotomicTotallyRamifiedShiftedCyclotomicPadicInt

L50 ↗
AlgebraicNumberTheory.Valuations.padicCyclotomicTotallyRamifiedShiftedCyclotomicPadicInt
Documentation

The translated prime-power cyclotomic polynomial over the actual p-adic integer ring.

Source context 6 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open Polynomial
open scoped Polynomial
universe u
Lean source · statement
def padicCyclotomicTotallyRamifiedShiftedCyclotomicPadicInt
    (p k : ℕ) [Fact p.Prime] : ℤ_[p][X]
theorem

padicCyclotomicTotallyRamifiedShiftedCyclotomicPadicInt_eq_map

L54 ↗
AlgebraicNumberTheory.Valuations.padicCyclotomicTotallyRamifiedShiftedCyclotomicPadicInt_eq_map
Source context 6 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open Polynomial
open scoped Polynomial
universe u
Lean source · statement
theorem padicCyclotomicTotallyRamifiedShiftedCyclotomicPadicInt_eq_map
    (p k : ℕ) [Fact p.Prime] :
    padicCyclotomicTotallyRamifiedShiftedCyclotomicPadicInt p k =
      (((cyclotomic (p ^ (k + 1)) ℤ).comp (X + 1)).map
        (algebraMap ℤ ℤ_[p]))
theorem

padicCyclotomicTotallyRamifiedShiftedCyclotomicPadicInt_isEisensteinAt

L63 ↗
AlgebraicNumberTheory.Valuations.padicCyclotomicTotallyRamifiedShiftedCyclotomicPadicInt_isEisensteinAt
Documentation

The translated cyclotomic polynomial remains Eisenstein after completion from ℤ to ℤ_[p].

Source context 6 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open Polynomial
open scoped Polynomial
universe u
Lean source · statement
theorem padicCyclotomicTotallyRamifiedShiftedCyclotomicPadicInt_isEisensteinAt
    (p k : ℕ) [Fact p.Prime] :
    (padicCyclotomicTotallyRamifiedShiftedCyclotomicPadicInt p k).IsEisensteinAt
      (Ideal.span ({(p : ℤ_[p])} : Set ℤ_[p]))
theorem

padicCyclotomicTotallyRamifiedShiftedCyclotomicPadicInt_irreducible

L104 ↗
AlgebraicNumberTheory.Valuations.padicCyclotomicTotallyRamifiedShiftedCyclotomicPadicInt_irreducible
Documentation

The translated polynomial is irreducible over ℤ_[p] by Eisenstein.

Source context 6 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open Polynomial
open scoped Polynomial
universe u
Lean source · statement
theorem padicCyclotomicTotallyRamifiedShiftedCyclotomicPadicInt_irreducible
    (p k : ℕ) [Fact p.Prime] :
    Irreducible (padicCyclotomicTotallyRamifiedShiftedCyclotomicPadicInt p k)
theorem

padicCyclotomicTotallyRamifiedShiftedCyclotomicPadic_irreducible

L120 ↗
AlgebraicNumberTheory.Valuations.padicCyclotomicTotallyRamifiedShiftedCyclotomicPadic_irreducible
Documentation

The translated polynomial is irreducible over the p-adic field.

Source context 6 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open Polynomial
open scoped Polynomial
universe u
Lean source · statement
theorem padicCyclotomicTotallyRamifiedShiftedCyclotomicPadic_irreducible
    (p k : ℕ) [Fact p.Prime] :
    Irreducible
      ((cyclotomic (p ^ (k + 1)) ℚ_[p]).comp (X + 1))
theorem

padicCyclotomicPolynomial_irreducible_prime_pow_succ

L135 ↗
AlgebraicNumberTheory.Valuations.padicCyclotomicPolynomial_irreducible_prime_pow_succ
Documentation

The prime-power cyclotomic polynomial is irreducible over ℚ_[p]. This supplies the local irreducibility input for the ramification analysis.

Source context 6 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open Polynomial
open scoped Polynomial
universe u
Lean source · statement
theorem padicCyclotomicPolynomial_irreducible_prime_pow_succ
    (p k : ℕ) [Fact p.Prime] :
    Irreducible (cyclotomic (p ^ (k + 1)) ℚ_[p])
instance

padicCyclotomicTotallyRamifiedAlgebraPadicInt

L150 ↗
AlgebraicNumberTheory.Valuations.padicCyclotomicTotallyRamifiedAlgebraPadicInt
Source context 9 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open Polynomial
open scoped Polynomial
universe u
section CyclotomicExtension
variable {p k : ℕ} [Fact p.Prime]
variable {L : Type u} [Field L] [Algebra ℚ_[p] L]
Lean source · statement
instance padicCyclotomicTotallyRamifiedAlgebraPadicInt : Algebra ℤ_[p] L
instance

padicCyclotomicTotallyRamifiedScalarTowerPadicInt

L153 ↗
AlgebraicNumberTheory.Valuations.padicCyclotomicTotallyRamifiedScalarTowerPadicInt
Source context 10 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open Polynomial
open scoped Polynomial
universe u
section CyclotomicExtension
variable {p k : ℕ} [Fact p.Prime]
variable {L : Type u} [Field L] [Algebra ℚ_[p] L]
local instance padicCyclotomicTotallyRamifiedAlgebraPadicInt : Algebra ℤ_[p] L :=
  ((algebraMap ℚ_[p] L).comp (algebraMap ℤ_[p] ℚ_[p])).toAlgebra
Lean source · statement
instance padicCyclotomicTotallyRamifiedScalarTowerPadicInt :
    IsScalarTower ℤ_[p] ℚ_[p] L
theorem

padic_isCyclotomicExtension_of_primitiveRoot_adjoin_eq_top

L161 ↗
AlgebraicNumberTheory.Valuations.padic_isCyclotomicExtension_of_primitiveRoot_adjoin_eq_top
Documentation

A field generated over ℚ_[p] by the displayed primitive root is the corresponding cyclotomic extension. The generation hypothesis only spells out the notation ℚ_[p](ζ); none of the totally ramified cyclotomic theorem's conclusions is assumed.

Source context 11 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open Polynomial
open scoped Polynomial
universe u
section CyclotomicExtension
variable {p k : ℕ} [Fact p.Prime]
variable {L : Type u} [Field L] [Algebra ℚ_[p] L]
local instance padicCyclotomicTotallyRamifiedAlgebraPadicInt : Algebra ℤ_[p] L :=
  ((algebraMap ℚ_[p] L).comp (algebraMap ℤ_[p] ℚ_[p])).toAlgebra
local instance padicCyclotomicTotallyRamifiedScalarTowerPadicInt :
    IsScalarTower ℤ_[p] ℚ_[p] L :=
  IsScalarTower.of_algebraMap_eq' rfl
Lean source · statement
theorem padic_isCyclotomicExtension_of_primitiveRoot_adjoin_eq_top
    (ζ : L) (hζ : IsPrimitiveRoot ζ (p ^ (k + 1)))
    (hgen : Algebra.adjoin ℚ_[p] ({ζ} : Set L) = ⊤) :
    IsCyclotomicExtension {p ^ (k + 1)} ℚ_[p] L
theorem

padicCyclotomicTotallyRamified_finrank_eq_totient

L174 ↗
AlgebraicNumberTheory.Valuations.padicCyclotomicTotallyRamified_finrank_eq_totient
Documentation

the totally ramified cyclotomic theorem(i), degree in Euler-totient form.

Source context 11 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open Polynomial
open scoped Polynomial
universe u
section CyclotomicExtension
variable {p k : ℕ} [Fact p.Prime]
variable {L : Type u} [Field L] [Algebra ℚ_[p] L]
local instance padicCyclotomicTotallyRamifiedAlgebraPadicInt : Algebra ℤ_[p] L :=
  ((algebraMap ℚ_[p] L).comp (algebraMap ℤ_[p] ℚ_[p])).toAlgebra
local instance padicCyclotomicTotallyRamifiedScalarTowerPadicInt :
    IsScalarTower ℤ_[p] ℚ_[p] L :=
  IsScalarTower.of_algebraMap_eq' rfl
Lean source · statement
theorem padicCyclotomicTotallyRamified_finrank_eq_totient
    (ζ : L) (hζ : IsPrimitiveRoot ζ (p ^ (k + 1)))
    (hgen : Algebra.adjoin ℚ_[p] ({ζ} : Set L) = ⊤) :
    Module.finrank ℚ_[p] L = Nat.totient (p ^ (k + 1))
theorem

padicCyclotomic_finrank_eq_prime_sub_one_mul_pow

L186 ↗
AlgebraicNumberTheory.Valuations.padicCyclotomic_finrank_eq_prime_sub_one_mul_pow
Documentation

The explicit degree of the totally ramified cyclotomic extension (p - 1) * p ^ k.

Source context 11 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open Polynomial
open scoped Polynomial
universe u
section CyclotomicExtension
variable {p k : ℕ} [Fact p.Prime]
variable {L : Type u} [Field L] [Algebra ℚ_[p] L]
local instance padicCyclotomicTotallyRamifiedAlgebraPadicInt : Algebra ℤ_[p] L :=
  ((algebraMap ℚ_[p] L).comp (algebraMap ℤ_[p] ℚ_[p])).toAlgebra
local instance padicCyclotomicTotallyRamifiedScalarTowerPadicInt :
    IsScalarTower ℤ_[p] ℚ_[p] L :=
  IsScalarTower.of_algebraMap_eq' rfl
Lean source · statement
theorem padicCyclotomic_finrank_eq_prime_sub_one_mul_pow
    (ζ : L) (hζ : IsPrimitiveRoot ζ (p ^ (k + 1)))
    (hgen : Algebra.adjoin ℚ_[p] ({ζ} : Set L) = ⊤) :
    Module.finrank ℚ_[p] L = (p - 1) * p ^ k
def

padicCyclotomicTotallyRamified_galoisGroupEquivUnits

L196 ↗
AlgebraicNumberTheory.Valuations.padicCyclotomicTotallyRamified_galoisGroupEquivUnits
Documentation

the totally ramified cyclotomic theorem(ii): the full Galois group is the unit group modulo p ^ (k + 1).

Source context 11 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open Polynomial
open scoped Polynomial
universe u
section CyclotomicExtension
variable {p k : ℕ} [Fact p.Prime]
variable {L : Type u} [Field L] [Algebra ℚ_[p] L]
local instance padicCyclotomicTotallyRamifiedAlgebraPadicInt : Algebra ℤ_[p] L :=
  ((algebraMap ℚ_[p] L).comp (algebraMap ℤ_[p] ℚ_[p])).toAlgebra
local instance padicCyclotomicTotallyRamifiedScalarTowerPadicInt :
    IsScalarTower ℤ_[p] ℚ_[p] L :=
  IsScalarTower.of_algebraMap_eq' rfl
Lean source · statement
def padicCyclotomicTotallyRamified_galoisGroupEquivUnits
    (ζ : L) (hζ : IsPrimitiveRoot ζ (p ^ (k + 1)))
    (hgen : Algebra.adjoin ℚ_[p] ({ζ} : Set L) = ⊤) :
    (L ≃ₐ[ℚ_[p]] L) ≃* (ZMod (p ^ (k + 1)))ˣ
theorem

padicCyclotomic_norm_one_sub_primitiveRoot_eq_prime

L208 ↗
AlgebraicNumberTheory.Valuations.padicCyclotomic_norm_one_sub_primitiveRoot_eq_prime
Documentation

the totally ramified cyclotomic theorem(iv), including the exceptional order-two case: the field norm of 1 - ζ is exactly the rational prime p.

Source context 11 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open Polynomial
open scoped Polynomial
universe u
section CyclotomicExtension
variable {p k : ℕ} [Fact p.Prime]
variable {L : Type u} [Field L] [Algebra ℚ_[p] L]
local instance padicCyclotomicTotallyRamifiedAlgebraPadicInt : Algebra ℤ_[p] L :=
  ((algebraMap ℚ_[p] L).comp (algebraMap ℤ_[p] ℚ_[p])).toAlgebra
local instance padicCyclotomicTotallyRamifiedScalarTowerPadicInt :
    IsScalarTower ℤ_[p] ℚ_[p] L :=
  IsScalarTower.of_algebraMap_eq' rfl
Lean source · statement
theorem padicCyclotomic_norm_one_sub_primitiveRoot_eq_prime
    (ζ : L) (hζ : IsPrimitiveRoot ζ (p ^ (k + 1)))
    (hgen : Algebra.adjoin ℚ_[p] ({ζ} : Set L) = ⊤) :
    Algebra.norm ℚ_[p] (1 - ζ) = (p : ℚ_[p])
theorem

padicCyclotomicTotallyRamified_primitiveRoot_isIntegral_padicInt

L265 ↗
AlgebraicNumberTheory.Valuations.padicCyclotomicTotallyRamified_primitiveRoot_isIntegral_padicInt
Documentation

The primitive root is integral over the actual p-adic integer ring.

Source context 11 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open Polynomial
open scoped Polynomial
universe u
section CyclotomicExtension
variable {p k : ℕ} [Fact p.Prime]
variable {L : Type u} [Field L] [Algebra ℚ_[p] L]
local instance padicCyclotomicTotallyRamifiedAlgebraPadicInt : Algebra ℤ_[p] L :=
  ((algebraMap ℚ_[p] L).comp (algebraMap ℤ_[p] ℚ_[p])).toAlgebra
local instance padicCyclotomicTotallyRamifiedScalarTowerPadicInt :
    IsScalarTower ℤ_[p] ℚ_[p] L :=
  IsScalarTower.of_algebraMap_eq' rfl
Lean source · statement
theorem padicCyclotomicTotallyRamified_primitiveRoot_isIntegral_padicInt
    (ζ : L) (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) :
    IsIntegral ℤ_[p] ζ
theorem

padicCyclotomicTotallyRamified_minpoly_sub_one_padicInt

L274 ↗
AlgebraicNumberTheory.Valuations.padicCyclotomicTotallyRamified_minpoly_sub_one_padicInt
Documentation

The p-adic-integer minimal polynomial of ζ - 1 is the Eisenstein translate Φ_{p^(k+1)}(X+1).

Source context 11 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open Polynomial
open scoped Polynomial
universe u
section CyclotomicExtension
variable {p k : ℕ} [Fact p.Prime]
variable {L : Type u} [Field L] [Algebra ℚ_[p] L]
local instance padicCyclotomicTotallyRamifiedAlgebraPadicInt : Algebra ℤ_[p] L :=
  ((algebraMap ℚ_[p] L).comp (algebraMap ℤ_[p] ℚ_[p])).toAlgebra
local instance padicCyclotomicTotallyRamifiedScalarTowerPadicInt :
    IsScalarTower ℤ_[p] ℚ_[p] L :=
  IsScalarTower.of_algebraMap_eq' rfl
Lean source · statement
theorem padicCyclotomicTotallyRamified_minpoly_sub_one_padicInt
    (ζ : L) (hζ : IsPrimitiveRoot ζ (p ^ (k + 1)))
    (hgen : Algebra.adjoin ℚ_[p] ({ζ} : Set L) = ⊤) :
    minpoly ℤ_[p] (ζ - 1) =
      padicCyclotomicTotallyRamifiedShiftedCyclotomicPadicInt p k

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