Module

RamificationIndex.lean

Nyll.ValuedFieldTheory.LocalField.Padic.Cyclotomic.TotallyRamified.RamificationIndex

3 declarations indexed from sourceView source ↗

Module documentation

The ramification index of the totally ramified cyclotomic extension

This file maps the Eisenstein unit relation into the target valuation ring and proves e = [L : ℚ_[p]], together with the uniformizer statement.

Imports2

Imported by2

instance

padicCyclotomicTotallyRamifiedRamificationIndexAlgebraPadicInt

L34 ↗

AlgebraicNumberTheory.Valuations.padicCyclotomicTotallyRamifiedRamificationIndexAlgebraPadicInt

Source context 11 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open Polynomial
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
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 padicCyclotomicTotallyRamifiedRamificationIndexAlgebraPadicInt : Algebra ℤ_[p] L

instance

padicCyclotomicTotallyRamifiedRamificationIndexScalarTowerPadicInt

L37 ↗

AlgebraicNumberTheory.Valuations.padicCyclotomicTotallyRamifiedRamificationIndexScalarTowerPadicInt

Source context 12 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open Polynomial
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open scoped Polynomial
universe u
section CyclotomicExtension
variable {p k : ℕ} [Fact p.Prime]
variable {L : Type u} [Field L] [Algebra ℚ_[p] L]
local instance padicCyclotomicTotallyRamifiedRamificationIndexAlgebraPadicInt : Algebra ℤ_[p] L :=
  ((algebraMap ℚ_[p] L).comp (algebraMap ℤ_[p] ℚ_[p])).toAlgebra

Lean source · statement

instance padicCyclotomicTotallyRamifiedRamificationIndexScalarTowerPadicInt :
    IsScalarTower ℤ_[p] ℚ_[p] L

theorem

padicCyclotomicTotallyRamified_uniformizer_and_ramificationIndex_eq_degree

L44 ↗

AlgebraicNumberTheory.Valuations.padicCyclotomicTotallyRamified_uniformizer_and_ramificationIndex_eq_degree

Documentation

The ideal-theoretic core of the totally ramified cyclotomic theorem(i): for the actual integral-closure valuation, 1 - ζ is a uniformizer and the Eisenstein relation forces the ramification index to equal the field degree.

Source context 13 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open Polynomial
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open scoped Polynomial
universe u
section CyclotomicExtension
variable {p k : ℕ} [Fact p.Prime]
variable {L : Type u} [Field L] [Algebra ℚ_[p] L]
local instance padicCyclotomicTotallyRamifiedRamificationIndexAlgebraPadicInt : Algebra ℤ_[p] L :=
  ((algebraMap ℚ_[p] L).comp (algebraMap ℤ_[p] ℚ_[p])).toAlgebra
local instance padicCyclotomicTotallyRamifiedRamificationIndexScalarTowerPadicInt :
    IsScalarTower ℤ_[p] ℚ_[p] L :=
  IsScalarTower.of_algebraMap_eq' rfl

Lean source · statement

theorem padicCyclotomicTotallyRamified_uniformizer_and_ramificationIndex_eq_degree
    (ζ : L) (hζ : IsPrimitiveRoot ζ (p ^ (k + 1)))
    (hgen : Algebra.adjoin ℚ_[p] ({ζ} : Set L) = ⊤)
    [FiniteDimensional ℚ_[p] L] [Algebra.IsSeparable ℚ_[p] L]
    (target : CompleteDVF.{u, 0} L)
    [hExt : (padicCompleteDVF p).valuation.HasExtension
      target.valuation]
    [hTarget : IsIntegralClosure target.valuationSubring
      (padicCompleteDVF p).valuationSubring L] :
    target.valuation.IsUniformizer (1 - ζ) ∧
      ValuedExtension.ramificationIndex
          (padicCompleteDVF p).toDVF target.toDVF =
        ValuedExtension.degree
          (padicCompleteDVF p).toDVF target.toDVF

Module documentation

The ramification index of the totally ramified cyclotomic extension

Declarations

padicCyclotomicTotallyRamifiedRamificationIndexAlgebraPadicInt

padicCyclotomicTotallyRamifiedRamificationIndexScalarTowerPadicInt

padicCyclotomicTotallyRamified_uniformizer_and_ramificationIndex_eq_degree