Module

ValuationRingEquiv.lean

Nyll.ValuedFieldTheory.LocalField.Padic.Cyclotomic.TotallyRamified.ValuationRingEquiv

3 declarations indexed from sourceView source ↗

Module documentation

The valuation-ring equivalence for the totally ramified cyclotomic extension

This file constructs the concrete equivalence from ℤ_[p][ζ - 1] to the actual valuation subring.

Imports1

Nyll.ValuedFieldTheory.LocalField.Padic.Cyclotomic.TotallyRamified.IntegralTranslate

Imported by2

instance

padicCyclotomicTotallyRamifiedValuationRingEquivAlgebraPadicInt

L30 ↗

AlgebraicNumberTheory.Valuations.padicCyclotomicTotallyRamifiedValuationRingEquivAlgebraPadicInt

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 padicCyclotomicTotallyRamifiedValuationRingEquivAlgebraPadicInt : Algebra ℤ_[p] L

instance

padicCyclotomicTotallyRamifiedValuationRingEquivScalarTowerPadicInt

L33 ↗

AlgebraicNumberTheory.Valuations.padicCyclotomicTotallyRamifiedValuationRingEquivScalarTowerPadicInt

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 padicCyclotomicTotallyRamifiedValuationRingEquivAlgebraPadicInt : Algebra ℤ_[p] L :=
  ((algebraMap ℚ_[p] L).comp (algebraMap ℤ_[p] ℚ_[p])).toAlgebra

Lean source · statement

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

theorem

padicCyclotomicTotallyRamified_exists_adjoin_sub_one_equiv_valuationSubring

L40 ↗

AlgebraicNumberTheory.Valuations.padicCyclotomicTotallyRamified_exists_adjoin_sub_one_equiv_valuationSubring

Documentation

The concrete ring ℤ_[p][ζ - 1] is canonically equivalent to the valuation subring in the actual-integral-closure complete-DVF model, and the equivalence preserves the represented element of L.

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 padicCyclotomicTotallyRamifiedValuationRingEquivAlgebraPadicInt : Algebra ℤ_[p] L :=
  ((algebraMap ℚ_[p] L).comp (algebraMap ℤ_[p] ℚ_[p])).toAlgebra
local instance padicCyclotomicTotallyRamifiedValuationRingEquivScalarTowerPadicInt :
    IsScalarTower ℤ_[p] ℚ_[p] L :=
  IsScalarTower.of_algebraMap_eq' rfl

Lean source · statement

theorem padicCyclotomicTotallyRamified_exists_adjoin_sub_one_equiv_valuationSubring
    (ζ : L) (hζ : IsPrimitiveRoot ζ (p ^ (k + 1)))
    (hgen : Algebra.adjoin ℚ_[p] ({ζ} : Set L) = ⊤)
    [FiniteDimensional ℚ_[p] L] [Algebra.IsSeparable ℚ_[p] L]
    (target : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, 0} L)
    [hExt :
      (LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicCompleteDVF
        p).valuation.HasExtension
      target.valuation]
    [hTarget : IsIntegralClosure target.valuationSubring
      (LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicCompleteDVF p).valuationSubring L] :
    ∃ q : Algebra.adjoin ℤ_[p] ({ζ - 1} : Set L) ≃+*
        target.valuationSubring,
      ∀ z, algebraMap target.valuationSubring L (q z) =
        algebraMap (Algebra.adjoin ℤ_[p] ({ζ - 1} : Set L)) L z

Module documentation

The valuation-ring equivalence for the totally ramified cyclotomic extension

Declarations

padicCyclotomicTotallyRamifiedValuationRingEquivAlgebraPadicInt

padicCyclotomicTotallyRamifiedValuationRingEquivScalarTowerPadicInt

padicCyclotomicTotallyRamified_exists_adjoin_sub_one_equiv_valuationSubring