ModuleIntegralTranslate.lean
Nyll.ValuedFieldTheory.LocalField.Padic.Cyclotomic.TotallyRamified.IntegralTranslate
3 declarations indexed from sourceView source ↗ Module documentation
Translation of the integral ring in the totally ramified cyclotomic extension
This file records that translating ζ by one preserves the explicit integral closure.
Declarations
AlgebraicNumberTheory.Valuations.padicCyclotomicTotallyRamifiedIntegralTranslateAlgebraPadicInt
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.padicCyclotomicTotallyRamifiedIntegralTranslateScalarTowerPadicInt
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 padicCyclotomicTotallyRamifiedIntegralTranslateAlgebraPadicInt : Algebra ℤ_[p] L :=
((algebraMap ℚ_[p] L).comp (algebraMap ℤ_[p] ℚ_[p])).toAlgebra
AlgebraicNumberTheory.Valuations.padicCyclotomicTotallyRamified_adjoin_sub_one_eq_adjoin
DocumentationTranslating the generator by one does not change the explicit ℤ_[p]-algebra.
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 padicCyclotomicTotallyRamifiedIntegralTranslateAlgebraPadicInt : Algebra ℤ_[p] L :=
((algebraMap ℚ_[p] L).comp (algebraMap ℤ_[p] ℚ_[p])).toAlgebra
local instance padicCyclotomicTotallyRamifiedIntegralTranslateScalarTowerPadicInt :
IsScalarTower ℤ_[p] ℚ_[p] L :=
IsScalarTower.of_algebraMap_eq' rfl