NYLL
Module

Existence.lean

Nyll.ValuedFieldTheory.LocalField.Padic.Cyclotomic.TotallyRamified.Existence
3 declarations indexed from sourceView source ↗

Module documentation

The totally ramified cyclotomic endpoint

This file packages the actual integral-closure complete-DVF model as a totally ramified extension.

Imports1
Imported by2

Declarations

instance

padicCyclotomicTotallyRamifiedRamificationEndpointAlgebraPadicInt

L32 ↗
AlgebraicNumberTheory.Valuations.padicCyclotomicTotallyRamifiedRamificationEndpointAlgebraPadicInt
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 padicCyclotomicTotallyRamifiedRamificationEndpointAlgebraPadicInt :
    Algebra ℤ_[p] L
instance

padicCyclotomicTotallyRamifiedRamificationEndpointScalarTowerPadicInt

L36 ↗
AlgebraicNumberTheory.Valuations.padicCyclotomicTotallyRamifiedRamificationEndpointScalarTowerPadicInt
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 padicCyclotomicTotallyRamifiedRamificationEndpointAlgebraPadicInt :
    Algebra ℤ_[p] L :=
  ((algebraMap ℚ_[p] L).comp (algebraMap ℤ_[p] ℚ_[p])).toAlgebra
Lean source · statement
instance padicCyclotomicTotallyRamifiedRamificationEndpointScalarTowerPadicInt :
    IsScalarTower ℤ_[p] ℚ_[p] L
theorem

padicCyclotomicTotallyRamified_exists_totallyRamified_extension

L44 ↗
AlgebraicNumberTheory.Valuations.padicCyclotomicTotallyRamified_exists_totallyRamified_extension
Documentation

the totally ramified cyclotomic theorem(i), valuative conclusion: the extension ℚ_[p](ζ) / ℚ_[p] is totally ramified. The target valuation is the canonical complete discrete valuation supplied by the actual integral closure of ℤ_[p] in L.

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 padicCyclotomicTotallyRamifiedRamificationEndpointAlgebraPadicInt :
    Algebra ℤ_[p] L :=
  ((algebraMap ℚ_[p] L).comp (algebraMap ℤ_[p] ℚ_[p])).toAlgebra
local instance padicCyclotomicTotallyRamifiedRamificationEndpointScalarTowerPadicInt :
    IsScalarTower ℤ_[p] ℚ_[p] L :=
  IsScalarTower.of_algebraMap_eq' rfl
Lean source · full declaration
theorem padicCyclotomicTotallyRamified_exists_totallyRamified_extension
    (ζ : L) (hζ : IsPrimitiveRoot ζ (p ^ (k + 1)))
    (hgen : Algebra.adjoin ℚ_[p] ({ζ} : Set L) = ⊤) :
    ∃ hfd : FiniteDimensional ℚ_[p] L,
      letI : FiniteDimensional ℚ_[p] L := hfd
      ∃ target : CompleteDVF.{u, 0} L,
        ∃ hExt :
          (padicCompleteDVF p).valuation.HasExtension
            target.valuation,
          letI :
            (padicCompleteDVF p).valuation.HasExtension
              target.valuation := hExt
          target.valuation.IsUniformizer (1 - ζ) ∧
            ValuedExtension.IsTotallyRamified
              (padicCompleteDVF p).toDVF target.toDVF := by
  let : NeZero (p ^ (k + 1)) :=
    ⟨pow_ne_zero _ (Fact.out : Nat.Prime p).ne_zero⟩
  let : IsCyclotomicExtension {p ^ (k + 1)} ℚ_[p] L :=
    padic_isCyclotomicExtension_of_primitiveRoot_adjoin_eq_top ζ hζ hgen
  let hfd : FiniteDimensional ℚ_[p] L :=
    IsCyclotomicExtension.finiteDimensional {p ^ (k + 1)} ℚ_[p] L
  let : FiniteDimensional ℚ_[p] L := hfd
  let : Algebra.IsSeparable ℚ_[p] L := by infer_instance
  let base := padicCompleteDVF p
  obtain ⟨target, hExt, hTarget, _⟩ :=
    ValuedExtension.exists_integralClosure_standard_fundamental_identity
      (K := ℚ_[p]) (L := L) base
  let : base.valuation.HasExtension target.valuation := hExt
  let : IsIntegralClosure target.valuationSubring base.valuationSubring L := hTarget
  let : IsScalarTower base.valuationSubring target.valuationSubring L := by
    apply IsScalarTower.of_algebraMap_eq
    intro x
    rfl
  have hsource :=
    padicCyclotomicTotallyRamified_uniformizer_and_ramificationIndex_eq_degree
      ζ hζ hgen target
  exact ⟨hfd, target, hExt, hsource.1,
    (open _root_.LocalFieldTheory.DiscreteValuationField.ValuedExtension in
      isTotallyRamified_iff_ramificationIndex_eq_degree_of_finite_separable
        base target).2 hsource.2⟩

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