Adic valuations on Dedekind domains #
Let R be a Dedekind domain of Krull dimension 1, K its field of fractions and v
a maximal ideal of R. In this file we prove compactness results for the v-adic
completion of K and its ring of integers.
We import required Lean 3 results from the work of María Inés de Frutos-Fernández and Filippo A. E. Nuccio concerning the uniformizers of the ring of integers and the finiteness of its residue field, which are referenced appropriately in the docstrings.
Note that one of the main results is not proved here, since the proof is already given elsewhere in Lean 3 by María Inés de Frutos-Fernández, Filippo A. E. Nuccio in https://github.com/mariainesdff/local_fields_journal/.
Main definitions #
IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.maximalIdeal K vis the maximal ideal of the ring of integers in thev-adic completion ofK.IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.residueField K vis the residue field of the ring of integers in thev-adic completion ofK.IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.ofFiniteCoeffs π nconstructs av-adic integer from ann-tuple ofv-adic integers by using them as coefficients in a finitev-adic expansionin the uniformizerπ.IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.toFiniteCoeffs π ngives the firstncoefficients in thev-adic expansion inπof av-adic integer modulo thenth power of the maximal ideal.
Main results #
IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.residueField_finite: the residue field of thev-adic ring of integers is finite.IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.quotient_maximalIdeal_pow_finite: the quotient of thev-adic ring of integers by a power of the maximal ideal is finite.IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.isCompact: thev-adic ring of integers is compact.IsDedekindDomain.HeightOneSpectrum.locallyCompactSpace: thev-adic Completion ofKis locally compact.
References #
- [J.W.S. Cassels, A. Frölich, Algebraic Number Theory][cassels1967algebraic]
- [M.I. de Frutos-Fernández, F.A.E. Nuccio, A Formalization of Complete Discrete Valuation Rings and Local Fields][defrutosfernandez2023]
Tags #
dedekind domain, dedekind ring, adic valuation
TODO #
- Incorporate the proof that the
v-adic ring of integers has finite residue field. - Use
UniformSpace.ballinstead ofopenBall.
def
IsDedekindDomain.HeightOneSpectrum.AdicCompletion.IsUniformizer
{R : Type u_1}
[CommRing R]
[IsDomain R]
[IsDedekindDomain R]
{K : Type u_2}
[Field K]
[Algebra R K]
[IsFractionRing R K]
{v : IsDedekindDomain.HeightOneSpectrum R}
(π : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)
:
An element π ∈ v.adicCompletion K is a uniformizer if it has valuation ofAdd(-1).
Equations
- IsDedekindDomain.HeightOneSpectrum.AdicCompletion.IsUniformizer π = (Valued.v π = ↑(Multiplicative.ofAdd (-1)))
Instances For
def
IsDedekindDomain.HeightOneSpectrum.AdicCompletion.coeRingHom
{R : Type u_1}
[CommRing R]
[IsDomain R]
[IsDedekindDomain R]
(K : Type u_2)
[Field K]
[Algebra R K]
[IsFractionRing R K]
(v : IsDedekindDomain.HeightOneSpectrum R)
:
Equations
- IsDedekindDomain.HeightOneSpectrum.AdicCompletion.coeRingHom K v = UniformSpace.Completion.coeRingHom
Instances For
theorem
IsDedekindDomain.HeightOneSpectrum.AdicCompletion.exists_uniformizer
{R : Type u_1}
[CommRing R]
[IsDomain R]
[IsDedekindDomain R]
(K : Type u_2)
[Field K]
[Algebra R K]
[IsFractionRing R K]
(v : IsDedekindDomain.HeightOneSpectrum R)
:
Uniformizers exist in the field completion v.adicCompletion K.
def
IsDedekindDomain.HeightOneSpectrum.AdicCompletion.openBall
{R : Type u_1}
[CommRing R]
[IsDomain R]
[IsDedekindDomain R]
(K : Type u_2)
[Field K]
[Algebra R K]
[IsFractionRing R K]
(v : IsDedekindDomain.HeightOneSpectrum R)
(γ : (WithZero (Multiplicative ℤ))ˣ)
:
Equations
- IsDedekindDomain.HeightOneSpectrum.AdicCompletion.openBall K v γ = {y : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v | Valued.v y < ↑γ}
Instances For
theorem
IsDedekindDomain.HeightOneSpectrum.AdicCompletion.openBall_isOpen
{R : Type u_1}
[CommRing R]
[IsDomain R]
[IsDedekindDomain R]
(K : Type u_2)
[Field K]
[Algebra R K]
[IsFractionRing R K]
(v : IsDedekindDomain.HeightOneSpectrum R)
(γ : (WithZero (Multiplicative ℤ))ˣ)
:
Open balls are open in the v-adic completion of K.
theorem
IsDedekindDomain.HeightOneSpectrum.AdicCompletion.openBall_isClosed
{R : Type u_1}
[CommRing R]
[IsDomain R]
[IsDedekindDomain R]
(K : Type u_2)
[Field K]
[Algebra R K]
[IsFractionRing R K]
(v : IsDedekindDomain.HeightOneSpectrum R)
(γ : (WithZero (Multiplicative ℤ))ˣ)
:
Open balls are closed in the v-adic completion of K.
theorem
IsDedekindDomain.HeightOneSpectrum.AdicCompletion.openBall_of_le_one_subset_adicCompletionIntegers
{R : Type u_1}
[CommRing R]
[IsDomain R]
[IsDedekindDomain R]
(K : Type u_2)
[Field K]
[Algebra R K]
[IsFractionRing R K]
(v : IsDedekindDomain.HeightOneSpectrum R)
(γ : (WithZero (Multiplicative ℤ))ˣ)
(hγ : γ ≤ 1)
:
Open balls of radius ≤ 1 are contained in the v-adic integers.
theorem
IsDedekindDomain.HeightOneSpectrum.AdicCompletion.mem_openBall_mul_uniformizer_pow
{R : Type u_1}
[CommRing R]
[IsDomain R]
[IsDedekindDomain R]
(K : Type u_2)
[Field K]
[Algebra R K]
[IsFractionRing R K]
(v : IsDedekindDomain.HeightOneSpectrum R)
{γ : (WithZero (Multiplicative ℤ))ˣ}
(x : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)
(π : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)
(hx : x ∈ IsDedekindDomain.HeightOneSpectrum.AdicCompletion.openBall K v γ)
(hπ : IsDedekindDomain.HeightOneSpectrum.AdicCompletion.IsUniformizer π)
:
Open balls can be shrunk to radius < 1 by multiplying by an appropriate
power of a uniformizer.
theorem
IsDedekindDomain.HeightOneSpectrum.AdicCompletion.ne_zero_iff_valuation_ne_zero
{R : Type u_1}
[CommRing R]
[IsDomain R]
[IsDedekindDomain R]
{K : Type u_2}
[Field K]
[Algebra R K]
[IsFractionRing R K]
{v : IsDedekindDomain.HeightOneSpectrum R}
(x : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)
:
theorem
IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.exists_uniformizer
{R : Type u_1}
[CommRing R]
[IsDomain R]
[IsDedekindDomain R]
(K : Type u_2)
[Field K]
[Algebra R K]
[IsFractionRing R K]
(v : IsDedekindDomain.HeightOneSpectrum R)
:
Uniformizers exist in the ring of v-adic integers.
def
IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.maximalIdeal
{R : Type u_1}
[CommRing R]
[IsDomain R]
[IsDedekindDomain R]
(K : Type u_2)
[Field K]
[Algebra R K]
[IsFractionRing R K]
(v : IsDedekindDomain.HeightOneSpectrum R)
:
The maximal ideal of the v-adic ring of integers.
Equations
Instances For
def
IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.residueField
{R : Type u_1}
[CommRing R]
[IsDomain R]
[IsDedekindDomain R]
(K : Type u_2)
[Field K]
[Algebra R K]
[IsFractionRing R K]
(v : IsDedekindDomain.HeightOneSpectrum R)
:
Type u_2
The residue field of the v-adic ring of integers.
Equations
Instances For
theorem
IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.valuation_eq_one_of_isUnit
{R : Type u_1}
[CommRing R]
[IsDomain R]
[IsDedekindDomain R]
{K : Type u_2}
[Field K]
[Algebra R K]
[IsFractionRing R K]
{v : IsDedekindDomain.HeightOneSpectrum R}
{x : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)}
(hx : IsUnit x)
:
Valued.v ↑x = 1
The valuation of a unit is 1.
theorem
IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.isUnit_of_valuation_eq_one
{R : Type u_1}
[CommRing R]
[IsDomain R]
[IsDedekindDomain R]
{K : Type u_2}
[Field K]
[Algebra R K]
[IsFractionRing R K]
{v : IsDedekindDomain.HeightOneSpectrum R}
{x : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)}
(hx : Valued.v ↑x = 1)
:
IsUnit x
A v-adic integer with valuation 1 is a unit.
theorem
IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.isUnit_iff_valuation_eq_one
{R : Type u_1}
[CommRing R]
[IsDomain R]
[IsDedekindDomain R]
{K : Type u_2}
[Field K]
[Algebra R K]
[IsFractionRing R K]
{v : IsDedekindDomain.HeightOneSpectrum R}
(x : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v))
:
A v-adic integer is a unit if and only if it has valuation 1.
theorem
IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.not_isUnit_iff_valuation_lt_one
{R : Type u_1}
[CommRing R]
[IsDomain R]
[IsDedekindDomain R]
{K : Type u_2}
[Field K]
[Algebra R K]
[IsFractionRing R K]
{v : IsDedekindDomain.HeightOneSpectrum R}
(x : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v))
:
A v-adic integer is not a unit if and only if it has valuation < 1.
theorem
IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.isUniformizer_ne_zero
{R : Type u_1}
[CommRing R]
[IsDomain R]
[IsDedekindDomain R]
{K : Type u_2}
[Field K]
[Algebra R K]
[IsFractionRing R K]
{v : IsDedekindDomain.HeightOneSpectrum R}
{π : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)}
(h : IsDedekindDomain.HeightOneSpectrum.AdicCompletion.IsUniformizer ↑π)
:
π ≠ 0
A uniformizer is non-zero.
theorem
IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.isUniformizer_not_isUnit
{R : Type u_1}
[CommRing R]
[IsDomain R]
[IsDedekindDomain R]
{K : Type u_2}
[Field K]
[Algebra R K]
[IsFractionRing R K]
{v : IsDedekindDomain.HeightOneSpectrum R}
{π : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)}
(h : IsDedekindDomain.HeightOneSpectrum.AdicCompletion.IsUniformizer ↑π)
:
A uniformizer is not a unit in the v-adic integers.
theorem
IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.eq_pow_uniformizer_mul_unit
{R : Type u_1}
[CommRing R]
[IsDomain R]
[IsDedekindDomain R]
{K : Type u_2}
[Field K]
[Algebra R K]
[IsFractionRing R K]
{v : IsDedekindDomain.HeightOneSpectrum R}
{x : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)}
{π : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)}
(hx : ↑x ≠ 0)
(hπ : IsDedekindDomain.HeightOneSpectrum.AdicCompletion.IsUniformizer ↑π)
:
Any v-adic integer can be written as a unit multiplied by a power of a uniformizer.
theorem
IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.isUniformizer_is_generator
{R : Type u_1}
[CommRing R]
[IsDomain R]
[IsDedekindDomain R]
{K : Type u_2}
[Field K]
[Algebra R K]
[IsFractionRing R K]
{v : IsDedekindDomain.HeightOneSpectrum R}
{π : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)}
(hπ : IsDedekindDomain.HeightOneSpectrum.AdicCompletion.IsUniformizer ↑π)
:
A uniformizer generates the maximal ideal of the v-adic integers.
theorem
IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.valuation_lt_one_of_maximalIdeal
{R : Type u_1}
[CommRing R]
[IsDomain R]
[IsDedekindDomain R]
{K : Type u_2}
[Field K]
[Algebra R K]
[IsFractionRing R K]
{v : IsDedekindDomain.HeightOneSpectrum R}
{x : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)}
(hx : x ∈ IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.maximalIdeal K v)
:
Valued.v ↑x < 1
An element of the maximal ideal of the v-adic integers has valuation less than 1.
theorem
IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.valuation_le_pow_of_maximalIdeal
{R : Type u_1}
[CommRing R]
[IsDomain R]
[IsDedekindDomain R]
{K : Type u_2}
[Field K]
[Algebra R K]
[IsFractionRing R K]
{v : IsDedekindDomain.HeightOneSpectrum R}
{x : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)}
(n : ℕ)
(hx : x ∈ IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.maximalIdeal K v ^ n)
:
An element of a positive power n of the maximal ideal of the v-adic integers has
valuation less than or equal to -n.
instance
IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.residueField_finite
{R : Type u_1}
[CommRing R]
[IsDomain R]
[IsDedekindDomain R]
{K : Type u_2}
[Field K]
[Algebra R K]
[IsFractionRing R K]
{v : IsDedekindDomain.HeightOneSpectrum R}
:
The residue field of the v-adic integers is finite.
Equations
- IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.residueField_finite = sorryAx (Fintype (IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.residueField K v))
instance
IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.instCommRingForAllFinResidueFieldSubtypeAdicCompletionMemValuationSubringInstFieldAdicCompletionInstMembershipInstSetLikeValuationSubringAdicCompletionIntegersInstCommRingSubtypeMemValuationSubringInstMembershipInstSetLikeValuationSubringLocalRing
{R : Type u_1}
[CommRing R]
[IsDomain R]
[IsDedekindDomain R]
{K : Type u_2}
[Field K]
[Algebra R K]
[IsFractionRing R K]
{v : IsDedekindDomain.HeightOneSpectrum R}
{n : ℕ}
:
Equations
- One or more equations did not get rendered due to their size.
def
IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.ofFiniteCoeffs
{R : Type u_1}
[CommRing R]
[IsDomain R]
[IsDedekindDomain R]
{K : Type u_2}
[Field K]
[Algebra R K]
[IsFractionRing R K]
{v : IsDedekindDomain.HeightOneSpectrum R}
(π : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v))
(n : ℕ)
:
Takes an n-tuple (a₁, ..., aₙ) and creates a v-adic integer using the n-tuple as
coefficients in a finite v-adic expansion in some fixed v-adic integer π as
a₁ + a₂π + a₃π² + .... Note the definition does not require π to be a uniformizer.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.finiteExpansion
{R : Type u_1}
[CommRing R]
[IsDomain R]
[IsDedekindDomain R]
{K : Type u_2}
[Field K]
[Algebra R K]
[IsFractionRing R K]
{v : IsDedekindDomain.HeightOneSpectrum R}
{π : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)}
(n : ℕ)
(x : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v))
(hπ : IsDedekindDomain.HeightOneSpectrum.AdicCompletion.IsUniformizer ↑π)
:
∃ (a : Fin n → LocalRing.ResidueField ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)),
x - List.sum
(List.mapIdx
(fun (i : ℕ)
(j :
Quotient
(Submodule.quotientRel
(LocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)))) =>
Quotient.out' j * π ^ i)
(List.ofFn a)) ∈ IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.maximalIdeal K v ^ n
Given a uniformizer π of the v-adic integers and a v-adic integer x, there exists
an n-tuple of representatives in the residue field of the v-adic integers such that x can
be written as a finite v-adic expansion in π with coefficients given by the n-tuple.
def
IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.toFiniteCoeffs
{R : Type u_1}
[CommRing R]
[IsDomain R]
[IsDedekindDomain R]
{K : Type u_2}
[Field K]
[Algebra R K]
[IsFractionRing R K]
{v : IsDedekindDomain.HeightOneSpectrum R}
{π : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)}
(n : ℕ)
(hπ : IsDedekindDomain.HeightOneSpectrum.AdicCompletion.IsUniformizer ↑π)
:
Given a uniformizer π of the v-adic integers and a v-adic integer x modulo a power of
the maximal ideal, gives the coefficients of x in the finite v-adic expansion in π as an
n-tuple of representatives in the residue field.
Equations
Instances For
theorem
IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.toFiniteCoeffs_injective
{R : Type u_1}
[CommRing R]
[IsDomain R]
[IsDedekindDomain R]
{K : Type u_2}
[Field K]
[Algebra R K]
[IsFractionRing R K]
{v : IsDedekindDomain.HeightOneSpectrum R}
{π : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)}
(n : ℕ)
(hπ : IsDedekindDomain.HeightOneSpectrum.AdicCompletion.IsUniformizer ↑π)
:
theorem
IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.quotient_maximalIdeal_pow_finite
{R : Type u_1}
[CommRing R]
[IsDomain R]
[IsDedekindDomain R]
{K : Type u_2}
[Field K]
[Algebra R K]
[IsFractionRing R K]
{v : IsDedekindDomain.HeightOneSpectrum R}
{π : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)}
(n : ℕ)
(hπ : IsDedekindDomain.HeightOneSpectrum.AdicCompletion.IsUniformizer ↑π)
:
The quotient of the v-adic integers with a power of the maximal ideal is finite.
theorem
IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.isClosed
{R : Type u_1}
[CommRing R]
[IsDomain R]
[IsDedekindDomain R]
(K : Type u_2)
[Field K]
[Algebra R K]
[IsFractionRing R K]
(v : IsDedekindDomain.HeightOneSpectrum R)
:
The v-adic integers are closed in the v-adic completion of K.
theorem
IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.hasFiniteSubcover_of_openBall_one_lt
{R : Type u_1}
[CommRing R]
[IsDomain R]
[IsDedekindDomain R]
(K : Type u_2)
[Field K]
[Algebra R K]
[IsFractionRing R K]
(v : IsDedekindDomain.HeightOneSpectrum R)
{γ : (WithZero (Multiplicative ℤ))ˣ}
(hγ : ↑γ > 1)
:
∃ (t : Set (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)),
Set.Finite t ∧ ↑(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v) ⊆ ⋃ y ∈ t,
{x : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v |
(x, y) ∈ {p :
IsDedekindDomain.HeightOneSpectrum.adicCompletion K v × IsDedekindDomain.HeightOneSpectrum.adicCompletion K v |
Valued.v (p.2 - p.1) < ↑γ}}
There is a finite covering of the v-adic integers of open balls of radius larger than one,
namely the single open ball centred at 0.
theorem
IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.hasFiniteSubcover_of_openBall_eq_one
{R : Type u_1}
[CommRing R]
[IsDomain R]
[IsDedekindDomain R]
(K : Type u_2)
[Field K]
[Algebra R K]
[IsFractionRing R K]
(v : IsDedekindDomain.HeightOneSpectrum R)
{γ : (WithZero (Multiplicative ℤ))ˣ}
(hγ : ↑γ = 1)
:
∃ (t : Set (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)),
Set.Finite t ∧ ↑(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v) ⊆ ⋃ y ∈ t,
{x : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v |
(x, y) ∈ {p :
IsDedekindDomain.HeightOneSpectrum.adicCompletion K v × IsDedekindDomain.HeightOneSpectrum.adicCompletion K v |
Valued.v (p.2 - p.1) < ↑γ}}
There is a finite covering of the v-adic integers of open balls of radius equal to one,
obtained by using the finite representatives in the residue field.
theorem
IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.hasFiniteSubcover_of_openBall_lt_one
{R : Type u_1}
[CommRing R]
[IsDomain R]
[IsDedekindDomain R]
(K : Type u_2)
[Field K]
[Algebra R K]
[IsFractionRing R K]
(v : IsDedekindDomain.HeightOneSpectrum R)
{γ : (WithZero (Multiplicative ℤ))ˣ}
(hγ : ↑γ < 1)
:
∃ (t : Set (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)),
Set.Finite t ∧ ↑(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v) ⊆ ⋃ y ∈ t,
{x : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v |
(x, y) ∈ {p :
IsDedekindDomain.HeightOneSpectrum.adicCompletion K v × IsDedekindDomain.HeightOneSpectrum.adicCompletion K v |
Valued.v (p.2 - p.1) < ↑γ}}
There is a finite covering of the v-adic integers of open balls of radius less than one,
obtained by using the finite representatives in the quotient of the v-adic integers by a power
of the maximal ideal.
theorem
IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.isTotallyBounded
{R : Type u_1}
[CommRing R]
[IsDomain R]
[IsDedekindDomain R]
(K : Type u_2)
[Field K]
[Algebra R K]
[IsFractionRing R K]
(v : IsDedekindDomain.HeightOneSpectrum R)
:
The v-adic integers is a totally bounded set since they afford a finite subcover of
open balls, obtained by using the finite representatives of the quotient of the v-adic
integers by a power of the maximal ideal.
instance
IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.instCompleteSpaceSubtypeAdicCompletionMemValuationSubringInstFieldAdicCompletionInstMembershipInstSetLikeValuationSubringAdicCompletionIntegersInstUniformSpaceSubtypeToUniformSpaceToRingToDivisionRingWithZeroMultiplicativeIntInstLinearOrderedCommGroupWithZeroWithZeroLinearOrderedCommGroupLinearOrderedAddCommGroupValuedAdicCompletion
{R : Type u_1}
[CommRing R]
[IsDomain R]
[IsDedekindDomain R]
(K : Type u_2)
[Field K]
[Algebra R K]
[IsFractionRing R K]
(v : IsDedekindDomain.HeightOneSpectrum R)
:
Equations
- ⋯ = ⋯
theorem
IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.isCompact
{R : Type u_1}
[CommRing R]
[IsDomain R]
[IsDedekindDomain R]
(K : Type u_2)
[Field K]
[Algebra R K]
[IsFractionRing R K]
(v : IsDedekindDomain.HeightOneSpectrum R)
:
The v-adic integers is compact.
instance
IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.compactSpace
{R : Type u_1}
[CommRing R]
[IsDomain R]
[IsDedekindDomain R]
(K : Type u_2)
[Field K]
[Algebra R K]
[IsFractionRing R K]
(v : IsDedekindDomain.HeightOneSpectrum R)
:
Equations
- ⋯ = ⋯
instance
IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.instLocallyCompactSpaceSubtypeAdicCompletionMemValuationSubringInstFieldAdicCompletionInstMembershipInstSetLikeValuationSubringAdicCompletionIntegersInstTopologicalSpaceSubtypeToTopologicalSpaceToUniformSpaceToRingToDivisionRingWithZeroMultiplicativeIntInstLinearOrderedCommGroupWithZeroWithZeroLinearOrderedCommGroupLinearOrderedAddCommGroupValuedAdicCompletion
{R : Type u_1}
[CommRing R]
[IsDomain R]
[IsDedekindDomain R]
(K : Type u_2)
[Field K]
[Algebra R K]
[IsFractionRing R K]
(v : IsDedekindDomain.HeightOneSpectrum R)
:
Equations
- ⋯ = ⋯
theorem
IsDedekindDomain.HeightOneSpectrum.openBall_isCompact
{R : Type u_1}
[CommRing R]
[IsDomain R]
[IsDedekindDomain R]
(K : Type u_2)
[Field K]
[Algebra R K]
[IsFractionRing R K]
(v : IsDedekindDomain.HeightOneSpectrum R)
(γ : (WithZero (Multiplicative ℤ))ˣ)
:
Any open ball in the v-adic completion of K is compact.
instance
IsDedekindDomain.HeightOneSpectrum.locallyCompactSpace
{R : Type u_1}
[CommRing R]
[IsDomain R]
[IsDedekindDomain R]
(K : Type u_2)
[Field K]
[Algebra R K]
[IsFractionRing R K]
(v : IsDedekindDomain.HeightOneSpectrum R)
:
The v-adic completion of K is locally compact since the open balls give
compact neighbourhoods.
Equations
- ⋯ = ⋯