The maximal ideal of a local field as a height-one prime

Let L be a nonarchimedean local field. Its valuation ring 𝒪[L], packaged as the valuation subring of L, is a discrete valuation ring, so its maximal ideal is a height-one prime TauCeti.maximalPrime L of a Dedekind domain with fraction field L. Statements about the fraction field of a Dedekind domain at a height-one prime u, phrased with the adic valuation of u, therefore apply to L at maximalPrime L. This file records the facts needed to read them back in terms of the valuation of L: the adic valuation of maximalPrime L is equivalent to the valuation of L and has valuation ring 𝒪[L] again, the valuation ring of K maps into it for an extension L/K, and an integer that is nonzero in the residue field of K lies outside maximalPrime L.

Main definitions

• TauCeti.maximalPrime L: the maximal ideal of 𝒪[L], as a height-one prime.
• TauCeti.algebraValuationSubringMaximalPrime: the map from 𝒪[K] to the valuation ring of the adic valuation of maximalPrime L, a local homomorphism (TauCeti.isLocalHom_algebraMap_valuationSubringMaximalPrime) compatible with K → L (TauCeti.coe_algebraMap_valuationSubringMaximalPrime).

Main results

• TauCeti.valuationSubring_valuation_maximalPrime: the valuation ring of the adic valuation of maximalPrime L is 𝒪[L].
• TauCeti.isEquiv_valuation_maximalPrime: that adic valuation is equivalent to the valuation of L.
• TauCeti.natCast_notMem_maximalPrime: an integer nonzero in the residue field of K lies outside maximalPrime L.

instance TauCeti.isDiscreteValuationRing_valuationSubring {L : Type u_2} [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] : IsDiscreteValuationRing ↥(ValuativeRel.valuation L).valuationSubring

𝒪[L], packaged as a valuation subring, is a discrete valuation ring.

@[reducible, inline]

noncomputable abbrev TauCeti.maximalPrime (L : Type u_2) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] : IsDedekindDomain.HeightOneSpectrum ↥(ValuativeRel.valuation L).valuationSubring

The maximal ideal of 𝒪[L], as a height-one prime.

theorem TauCeti.valuationSubring_valuation_maximalPrime (L : Type u_2) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] : (IsDedekindDomain.HeightOneSpectrum.valuation L (maximalPrime L)).valuationSubring = (ValuativeRel.valuation L).valuationSubring

The valuation ring of the adic valuation of the maximal ideal of 𝒪[L] is 𝒪[L].

theorem TauCeti.isEquiv_valuation_maximalPrime (L : Type u_2) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] : (IsDedekindDomain.HeightOneSpectrum.valuation L (maximalPrime L)).IsEquiv (ValuativeRel.valuation L)

The adic valuation of the maximal ideal of 𝒪[L] is equivalent to the valuation of L.

@[instance_reducible]

noncomputable instance TauCeti.algebraValuationSubringMaximalPrime (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] : Algebra ↥(ValuativeRel.valuation K).integer ↥(IsDedekindDomain.HeightOneSpectrum.valuation L (maximalPrime L)).valuationSubring

𝒪[K] maps into the valuation ring of the adic valuation of the maximal ideal of 𝒪[L], which is 𝒪[L].

@[simp]

theorem TauCeti.coe_algebraMap_valuationSubringMaximalPrime {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] (r : ↥(ValuativeRel.valuation K).integer) : ↑((algebraMap ↥(ValuativeRel.valuation K).integer ↥(IsDedekindDomain.HeightOneSpectrum.valuation L (maximalPrime L)).valuationSubring) r) = (algebraMap K L) ↑r

The map from 𝒪[K] to the valuation ring of the adic valuation of the maximal ideal of 𝒪[L] is the map K → L on elements.

instance TauCeti.isScalarTower_valuationSubringMaximalPrime {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] : IsScalarTower (↥(ValuativeRel.valuation K).integer) (↥(IsDedekindDomain.HeightOneSpectrum.valuation L (maximalPrime L)).valuationSubring) L

instance TauCeti.isLocalHom_algebraMap_valuationSubringMaximalPrime {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] : IsLocalHom (algebraMap ↥(ValuativeRel.valuation K).integer ↥(IsDedekindDomain.HeightOneSpectrum.valuation L (maximalPrime L)).valuationSubring)

The map from 𝒪[K] to the valuation ring of the adic valuation of the maximal ideal of 𝒪[L] is local.

theorem TauCeti.natCast_notMem_maximalPrime {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] {n : ℕ} (hn : ↑n ≠ 0) : ↑n ∉ (maximalPrime L).asIdeal

An integer nonzero in the residue field of K is a unit of 𝒪[L], so it lies outside the maximal ideal of 𝒪[L] (TauCeti.valuation_natCast_eq_one_of_residueField_natCast_ne_zero, read in 𝒪[L]).