ModulePrimeElement.lean
Nyll.ValuedFieldTheory.LocalField.Padic.Cyclotomic.TotallyRamified.PrimeElement
4 declarations indexed from sourceView source ↗ Module documentation
A prime element for the totally ramified cyclotomic extension
This file proves directly from its norm that 1 - ζ is prime in the explicit DVR ℤ_[p][ζ].
Declarations
AlgebraicNumberTheory.Valuations.padicCyclotomicTotallyRamifiedPrimeElementAlgebraPadicInt
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]
AlgebraicNumberTheory.Valuations.padicCyclotomicTotallyRamifiedPrimeElementScalarTowerPadicInt
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 padicCyclotomicTotallyRamifiedPrimeElementAlgebraPadicInt : Algebra ℤ_[p] L :=
((algebraMap ℚ_[p] L).comp (algebraMap ℤ_[p] ℚ_[p])).toAlgebra
AlgebraicNumberTheory.Valuations.padicCyclotomicTotallyRamifiedOneSubPrimitiveRootInteger
DocumentationThe element 1 - ζ, viewed in the explicit integer ring ℤ_[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 padicCyclotomicTotallyRamifiedPrimeElementAlgebraPadicInt : Algebra ℤ_[p] L :=
((algebraMap ℚ_[p] L).comp (algebraMap ℤ_[p] ℚ_[p])).toAlgebra
local instance padicCyclotomicTotallyRamifiedPrimeElementScalarTowerPadicInt :
IsScalarTower ℤ_[p] ℚ_[p] L :=
IsScalarTower.of_algebraMap_eq' rfl
AlgebraicNumberTheory.Valuations.padicCyclotomicTotallyRamified_one_sub_primitiveRoot_prime
Documentationthe totally ramified cyclotomic theorem(iv): 1 - ζ is a prime element 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 padicCyclotomicTotallyRamifiedPrimeElementAlgebraPadicInt : Algebra ℤ_[p] L :=
((algebraMap ℚ_[p] L).comp (algebraMap ℤ_[p] ℚ_[p])).toAlgebra
local instance padicCyclotomicTotallyRamifiedPrimeElementScalarTowerPadicInt :
IsScalarTower ℤ_[p] ℚ_[p] L :=
IsScalarTower.of_algebraMap_eq' rfl