Extensions of valuations above a prime

DefinitionValuations extending a prime-adic valuation#✓fully proved

Let \(A\) be a Dedekind domain with fraction field \(K\), let \(L\) be a field extension of \(K\), and let \(\mathfrak{p}\) be a height-one prime of \(A\). A valuation \(w\) on \(L\) with values in the multiplicative group \(\mathbb{Z}\) with a zero adjoined extends the \(\mathfrak{p}\)-adic valuation of \(K\) when its restriction to \(K\) is equivalent to the \(\mathfrak{p}\)-adic valuation of \(K\).

This relation does not record an extension index or a normalization.

def extendsValuation
    (A : Type*) [CommRing A] [IsDedekindDomain A]
    (K : Type*) [Field K] [Algebra A K] [IsFractionRing A K]
    (L : Type*) [Field L] [Algebra K L]
    (𝔭 : HeightOneSpectrum A)
    (w : Valuation L (WithZero (Multiplicative ℤ))) : Prop :=
  (w.comap (algebraMap K L)).IsEquiv (𝔭.valuation K)

Used by 3

Used byEach extension of a prime-adic valuation comes from exactly one prime above · The adic valuation of a prime lying over extends the adic valuation below · Each extension of a prime-adic valuation comes from some prime above

DefinitionHeight-one primes above a prime#✓fully proved

Let \(A\) and \(B\) be Dedekind domains with \(B\) an \(A\)-algebra, and let \(\mathfrak{p}\) be a height-one prime of \(A\). The primes above \(\mathfrak{p}\) form the set of height-one primes \(\mathfrak{q}\) of \(B\) lying over \(\mathfrak{p}\), that is, whose preimage in \(A\) is \(\mathfrak{p}\).

def primesAbove (𝔭 : HeightOneSpectrum A) : Set (HeightOneSpectrum B) :=
  {𝔮 : HeightOneSpectrum B | 𝔮.asIdeal.LiesOver 𝔭.asIdeal}

Used by 2

Used byEach extension of a prime-adic valuation comes from exactly one prime above · Each extension of a prime-adic valuation comes from some prime above

LemmaMembership in a prime is detected by a prime lying over it#✓fully proved

Let \(A\) and \(B\) be Dedekind domains with \(B\) an \(A\)-algebra, let \(\mathfrak{p}\) be a height-one prime of \(A\), and let \(\mathfrak{q}\) be a height-one prime of \(B\) lying over \(\mathfrak{p}\). Then for every \(a \in A\), \(a \in \mathfrak{p}\) if and only if the image of \(a\) in \(B\) lies in \(\mathfrak{q}\).

lemma mem_of_liesOver (𝔭 : HeightOneSpectrum A) (𝔮 : HeightOneSpectrum B)
    (hlo : 𝔮.asIdeal.LiesOver 𝔭.asIdeal) (a : A) :
    a ∈ 𝔭.asIdeal ↔ algebraMap A B a ∈ 𝔮.asIdeal

Used by 1

Used byThe adic valuation of a prime lying over extends the adic valuation below

TheoremThe adic valuation of a prime lying over extends the adic valuation below#✓fully proved

Let \(A\) be a Dedekind domain with fraction field \(K\), let \(L\) be a finite separable extension of \(K\), and let \(B\) be a Dedekind domain that is the integral closure of \(A\) in \(L\) and has fraction field \(L\). If \(\mathfrak{q}\) is a height-one prime of \(B\) lying over a height-one prime \(\mathfrak{p}\) of \(A\), then the \(\mathfrak{q}\)-adic valuation of \(L\) extends the \(\mathfrak{p}\)-adic valuation of \(K\): its restriction to \(K\) is equivalent to the \(\mathfrak{p}\)-adic valuation of \(K\).

theorem valuation_extends_of_liesOver
    (𝔭 : HeightOneSpectrum A) (𝔮 : HeightOneSpectrum B)
    (hlo : 𝔮.asIdeal.LiesOver 𝔭.asIdeal) :
    extendsValuation A K L 𝔭 (𝔮.valuation L)

Uses 2

Statement usesValuations extending a prime-adic valuation

Proof usesMembership in a prime is detected by a prime lying over it

TheoremA valuation centered at a height-one prime is equivalent to its adic valuation#✓fully proved

Let \(B\) be a Dedekind domain with fraction field \(L\), let \(\mathfrak{q}\) be a height-one prime of \(B\), and let \(w\) be a valuation on \(L\) with values in the multiplicative group \(\mathbb{Z}\) with a zero adjoined. Suppose that \(w(b) \le 1\) for every \(b \in B\), and that for every \(b \in B\) we have \(b \in \mathfrak{q}\) if and only if \(w(b) < 1\). Then the \(\mathfrak{q}\)-adic valuation of \(L\) is equivalent to \(w\).

theorem dvr_overring_equiv
    {B' : Type*} [CommRing B'] [IsDedekindDomain B']
    {L' : Type*} [Field L'] [Algebra B' L'] [IsFractionRing B' L']
    (𝔮 : HeightOneSpectrum B')
    (w : Valuation L' (WithZero (Multiplicative ℤ)))
    (hB : ∀ b : B', w (algebraMap B' L' b) ≤ 1)
    (hIdeal : ∀ b : B', b ∈ 𝔮.asIdeal ↔ w (algebraMap B' L' b) < 1) :
    (𝔮.valuation L').IsEquiv w

Used by 1

Used byEach extension of a prime-adic valuation comes from some prime above

TheoremEach extension of a prime-adic valuation comes from some prime above#✓fully proved

Let \(A\) be a Dedekind domain with fraction field \(K\), let \(L\) be a finite separable extension of \(K\), and let \(B\) be a Dedekind domain that is the integral closure of \(A\) in \(L\) and has fraction field \(L\). Let \(\mathfrak{p}\) be a height-one prime of \(A\), and let \(w\) be a valuation on \(L\) with values in the multiplicative group \(\mathbb{Z}\) with a zero adjoined whose restriction to \(K\) is equivalent to the \(\mathfrak{p}\)-adic valuation of \(K\). Then there is a height-one prime \(\mathfrak{q}\) of \(B\) lying over \(\mathfrak{p}\) such that the \(\mathfrak{q}\)-adic valuation of \(L\) is equivalent to \(w\).

theorem valuation_surjective_of_extends
    (𝔭 : HeightOneSpectrum A)
    (w : Valuation L (WithZero (Multiplicative ℤ)))
    (hw : extendsValuation A K L 𝔭 w) :
    ∃ 𝔮 : HeightOneSpectrum B,
      𝔮 ∈ primesAbove A B 𝔭 ∧ (𝔮.valuation L).IsEquiv w

Uses 3 · Used by 1

Statement usesValuations extending a prime-adic valuation · Height-one primes above a prime

Proof usesA valuation centered at a height-one prime is equivalent to its adic valuation

Used byEach extension of a prime-adic valuation comes from exactly one prime above

TheoremEach extension of a prime-adic valuation comes from exactly one prime above#✓fully proved

Let \(A\) be a Dedekind domain with fraction field \(K\), let \(L\) be a finite separable extension of \(K\), and let \(B\) be a Dedekind domain that is the integral closure of \(A\) in \(L\) and has fraction field \(L\). Let \(\mathfrak{p}\) be a height-one prime of \(A\), and consider valuations on \(L\) with values in the multiplicative group \(\mathbb{Z}\) with a zero adjoined. Then (1) if \(\mathfrak{q}_1\) and \(\mathfrak{q}_2\) are height-one primes of \(B\) lying over \(\mathfrak{p}\) whose adic valuations on \(L\) are equivalent, then \(\mathfrak{q}_1 = \mathfrak{q}_2\); and (2) every such valuation \(w\) on \(L\) whose restriction to \(K\) is equivalent to the \(\mathfrak{p}\)-adic valuation of \(K\) is equivalent to the \(\mathfrak{q}\)-adic valuation of \(L\) for some height-one prime \(\mathfrak{q}\) of \(B\) lying over \(\mathfrak{p}\).

Valuations are compared only up to equivalence; no normalization or ramification index is asserted.

theorem extending_valuation_bijection_primes_above (𝔭 : HeightOneSpectrum A) :
    (∀ 𝔮₁ 𝔮₂ : HeightOneSpectrum B,
      𝔮₁ ∈ primesAbove A B 𝔭 →
      𝔮₂ ∈ primesAbove A B 𝔭 →
      (𝔮₁.valuation L).IsEquiv (𝔮₂.valuation L) → 𝔮₁ = 𝔮₂) ∧
    (∀ w : Valuation L (WithZero (Multiplicative ℤ)),
      extendsValuation A K L 𝔭 w →
      ∃ 𝔮 : HeightOneSpectrum B,
        𝔮 ∈ primesAbove A B 𝔭 ∧ (𝔮.valuation L).IsEquiv w)

Uses 3

Statement usesValuations extending a prime-adic valuation · Height-one primes above a prime

Proof usesEach extension of a prime-adic valuation comes from some prime above

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.