NYLL
Module

IntegralClosure.lean

Nyll.ValuedFieldTheory.LocalField.Padic.Cyclotomic.TotallyRamified.IntegralClosure
5 declarations indexed from sourceView source ↗

Module documentation

The integral closure in the totally ramified cyclotomic extension

This file identifies ℤ_[p][ζ] with the actual integral closure and proves that it is a discrete valuation ring.

Imports1
Imported by2

Declarations

instance

padicCyclotomicTotallyRamifiedIntegralClosureAlgebraPadicInt

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

padicCyclotomicTotallyRamifiedIntegralClosureScalarTowerPadicInt

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

padicCyclotomicTotallyRamified_isIntegralClosure_adjoin

L41 ↗
AlgebraicNumberTheory.Valuations.padicCyclotomicTotallyRamified_isIntegralClosure_adjoin
Documentation

the totally ramified cyclotomic theorem(iii): ℤ_[p][ζ] is the integral closure of ℤ_[p] in ℚ_[p](ζ). Since the base is complete, the integral closure is the unique valuation ring upstairs.

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 padicCyclotomicTotallyRamifiedIntegralClosureAlgebraPadicInt : Algebra ℤ_[p] L :=
  ((algebraMap ℚ_[p] L).comp (algebraMap ℤ_[p] ℚ_[p])).toAlgebra
local instance padicCyclotomicTotallyRamifiedIntegralClosureScalarTowerPadicInt :
    IsScalarTower ℤ_[p] ℚ_[p] L :=
  IsScalarTower.of_algebraMap_eq' rfl
Lean source · statement
theorem padicCyclotomicTotallyRamified_isIntegralClosure_adjoin
    (ζ : L) (hζ : IsPrimitiveRoot ζ (p ^ (k + 1)))
    (hgen : Algebra.adjoin ℚ_[p] ({ζ} : Set L) = ⊤) :
    IsIntegralClosure (Algebra.adjoin ℤ_[p] ({ζ} : Set L)) ℤ_[p] L
theorem

padicCyclotomicTotallyRamified_integralClosure_eq_adjoin

L122 ↗
AlgebraicNumberTheory.Valuations.padicCyclotomicTotallyRamified_integralClosure_eq_adjoin
Documentation

Literal ring-of-integers equality in the totally ramified cyclotomic theorem(iii).

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 padicCyclotomicTotallyRamifiedIntegralClosureAlgebraPadicInt : Algebra ℤ_[p] L :=
  ((algebraMap ℚ_[p] L).comp (algebraMap ℤ_[p] ℚ_[p])).toAlgebra
local instance padicCyclotomicTotallyRamifiedIntegralClosureScalarTowerPadicInt :
    IsScalarTower ℤ_[p] ℚ_[p] L :=
  IsScalarTower.of_algebraMap_eq' rfl
Lean source · statement
theorem padicCyclotomicTotallyRamified_integralClosure_eq_adjoin
    (ζ : L) (hζ : IsPrimitiveRoot ζ (p ^ (k + 1)))
    (hgen : Algebra.adjoin ℚ_[p] ({ζ} : Set L) = ⊤) :
    integralClosure ℤ_[p] L = Algebra.adjoin ℤ_[p] ({ζ} : Set L)
theorem

padicCyclotomicTotallyRamified_adjoin_isDiscreteValuationRing

L138 ↗
AlgebraicNumberTheory.Valuations.padicCyclotomicTotallyRamified_adjoin_isDiscreteValuationRing
Documentation

The explicit ring ℤ_[p][ζ] is a DVR. This transports the standard finite-integral-closure theorem across the concrete equivalence between ℤ_[p] and the valuation subring of ℚ_[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 padicCyclotomicTotallyRamifiedIntegralClosureAlgebraPadicInt : Algebra ℤ_[p] L :=
  ((algebraMap ℚ_[p] L).comp (algebraMap ℤ_[p] ℚ_[p])).toAlgebra
local instance padicCyclotomicTotallyRamifiedIntegralClosureScalarTowerPadicInt :
    IsScalarTower ℤ_[p] ℚ_[p] L :=
  IsScalarTower.of_algebraMap_eq' rfl
Lean source · statement
theorem padicCyclotomicTotallyRamified_adjoin_isDiscreteValuationRing
    (ζ : L) (hζ : IsPrimitiveRoot ζ (p ^ (k + 1)))
    (hgen : Algebra.adjoin ℚ_[p] ({ζ} : Set L) = ⊤) :
    IsDiscreteValuationRing (Algebra.adjoin ℤ_[p] ({ζ} : Set L))

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