IsDedekindDomain.HeightOneSpectrum.int_valuation_lt_one_iff_dvd
theorem IsDedekindDomain.HeightOneSpectrum.int_valuation_lt_one_iff_dvd :
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R)
(r : R), v.intValuationDef r < 1 ↔ v.asIdeal ∣ Ideal.span {r}
The theorem `IsDedekindDomain.HeightOneSpectrum.int_valuation_lt_one_iff_dvd` states that for any commutative ring `R` which is also a Dedekind domain, and for any `v` in the height one spectrum of `R`, and for any element `r` of `R`, the `v`-adic valuation of `r` is less than 1 if and only if the ideal generated by `v` divides the ideal generated by `{r}`. In other words, the valuation of `r` with respect to `v` being less than 1 is equivalent to `v` being a divisor of the ideal generated by `r` in the ring `R`.
More concisely: For any commutative Dedekind domain `R`, and any height-one prime ideal `v` of `R`, an element `r` in `R` has `v`-adic valuation less than 1 if and only if `v` divides the ideal generated by `r`.
|
IsDedekindDomain.HeightOneSpectrum.valuation_lt_one_iff_dvd
theorem IsDedekindDomain.HeightOneSpectrum.valuation_lt_one_iff_dvd :
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type u_2} [inst_2 : Field K]
[inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (r : R),
v.valuation ((algebraMap R K) r) < 1 ↔ v.asIdeal ∣ Ideal.span {r}
This theorem states that for any commutative ring `R` that is a Dedekind domain, any field `K` that is the field of fractions of `R`, any `v` which is a height one prime of `R`, and any element `r` of `R`, the `v`-adic valuation of `r` (under the algebraic map from `R` to `K`) is less than 1 if and only if `v` divides the ideal generated by `r`. In other words, the valuation of `r` being less than 1 is equivalent to `r` being an element of the ideal associated with `v`. This theorem is a key property of Dedekind domains, connecting the concept of valuation with ideal theory.
More concisely: In a commutative Dedekind domain, for any height one prime `v` and element `r`, the `v`-adic valuation of `r` is less than 1 if and only if `r` is in the ideal generated by `v`.
|
IsDedekindDomain.HeightOneSpectrum.int_valuation_zero_le
theorem IsDedekindDomain.HeightOneSpectrum.int_valuation_zero_le :
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R)
(x : ↥(nonZeroDivisors R)), 0 < v.intValuationDef ↑x
This theorem states that for any commutative ring `R` that is also a Dedekind domain, every nonzero divisor of `R` has a valuation greater than zero. Here, the valuation function `v.intValuationDef` is defined on the height one spectrum of the Dedekind domain `R`.
This means that for any nonzero divisor `x` of `R`, if we consider `x` as an element of the submonoid of non-zero divisors of `R`, then the integer valuation of `x` under any valuation function from the height one spectrum of `R` is strictly greater than zero. This underlines the property of nonzero divisors in a Dedekind domain to have positive valuations.
More concisely: In a commutative Dedekind domain, every nonzero divisor has a positive valuation under some valuation from the height one spectrum.
|
IsDedekindDomain.HeightOneSpectrum.valuation_of_mk'
theorem IsDedekindDomain.HeightOneSpectrum.valuation_of_mk' :
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type u_2} [inst_2 : Field K]
[inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) {r : R}
{s : ↥(nonZeroDivisors R)}, v.valuation (IsLocalization.mk' K r s) = v.intValuation r / v.intValuation ↑s
The theorem `IsDedekindDomain.HeightOneSpectrum.valuation_of_mk'` states that for a Dedekind domain `R`, and its field of fractions `K`, the `v`-adic valuation of a fraction `r/s`, where `r` is an element of `R` and `s` is a non-zero divisor in `R`, is equal to the `v`-adic valuation of `r` divided by the `v`-adic valuation of `s`. Here, the `v`-adic valuation is a function from the height one spectrum of `R` to the real numbers, that measures the "degree of divisibility" of an element. This theorem shows a key property of fractions in a Dedekind domain, connecting the valuation of a fraction to the valuations of its numerator and denominator.
More concisely: For a Dedekind domain R and non-zero divisor s, the `v`-adic valuation of the fraction r/s equals the difference of the `v`-adic valuations of r and s.
|
IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap
theorem IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap :
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type u_2} [inst_2 : Field K]
[inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (r : R),
v.valuation ((algebraMap R K) r) = v.intValuation r
This theorem, named `IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap`, states that for any integral domain `R` that is a Dedekind domain, its field of fractions `K`, and a `v`-adic valuation `v` on `R`, the valuation `v` extended to `K` through the algebraic map (from `R` to `K`) applied on any element `r` of `R`, equals the `v`-adic integer valuation of `r`. In simpler terms, it means the `v`-adic valuation on the field of fractions `K` extends the `v`-adic valuation on the integral domain `R`.
More concisely: For any Dedekind domain R with field of fractions K and v-adic valuation on R, the extended valuation of r in K via the algebraic map equals the v-adic integer valuation of r for any r in R.
|
IsDedekindDomain.HeightOneSpectrum.IntValuation.map_zero'
theorem IsDedekindDomain.HeightOneSpectrum.IntValuation.map_zero' :
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R),
v.intValuationDef 0 = 0
The theorem `IsDedekindDomain.HeightOneSpectrum.IntValuation.map_zero'` states that for any Type `R` that has a commutative ring structure and is a Dedekind domain, the `v`-adic valuation of zero (where `v` belongs to the height one spectrum of `R`) equals zero. In simpler terms, it says in any Dedekind domain, the valuation of zero at any prime ideal of height one is zero.
More concisely: In any Dedekind domain, the valuation of the zero element at any prime ideal of height one is zero.
|
IsDedekindDomain.HeightOneSpectrum.int_valuation_ne_zero
theorem IsDedekindDomain.HeightOneSpectrum.int_valuation_ne_zero :
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R)
(x : R), x ≠ 0 → v.intValuationDef x ≠ 0
This theorem states that in the context of a Dedekind Domain (which is a type of commutative ring), any nonzero element has a nonzero adic valuation. In other words, if `R` is a Dedekind Domain and `x` is an element of `R` that is not zero, then the adic valuation of `x` (as defined by a certain `HeightOneSpectrum` of `R`) is also not zero.
More concisely: In a Dedekind Domain, every nonzero element has a non-zero adic valuation.
|
IsDedekindDomain.HeightOneSpectrum.valuation_le_one
theorem IsDedekindDomain.HeightOneSpectrum.valuation_le_one :
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type u_2} [inst_2 : Field K]
[inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (r : R),
v.valuation ((algebraMap R K) r) ≤ 1
The theorem `IsDedekindDomain.HeightOneSpectrum.valuation_le_one` states that for every Dedekind domain `R`, field `K` such that `K` is the field of fractions of `R`, and for any `v` from the height one spectrum of `R`, and any element `r` of `R`, the `v`-adic valuation of the image of `r` under the natural embedding from `R` to `K` (given by the Algebra structure) is less than or equal to 1. In other words, for any Dedekind domain and its field of fractions, the `v`-adic valuation of any element of the domain mapped to the field is bounded above by 1.
More concisely: For any Dedekind domain R with field of fractions K, and for every height one prime ideal p of R and any element r in R, the v-adic valuation of the image of r in K is less than or equal to 1.
|
IsDedekindDomain.HeightOneSpectrum.valuation_exists_uniformizer
theorem IsDedekindDomain.HeightOneSpectrum.valuation_exists_uniformizer :
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) [inst_2 : Field K]
[inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R),
∃ π, v.valuation π = ↑(Multiplicative.ofAdd (-1))
This theorem asserts that for any integral domain `R` that is also a Dedekind domain, and for any field `K` that is the field of fractions of `R`, there exists an element `π` in `K` for every height one prime ideal `v` of `R`, such that the `v`-adic valuation of `π` is `-1` (reinterpreted as an element of the multiplicative group). Essentially, it is saying that there exists a uniformizer (an element that generates the maximal ideal of the local ring) for every height one prime ideal in the Dedekind domain.
More concisely: For any Dedekind domain `R` and its field of fractions `K`, there exists an element `π` in `K` such that for every height one prime ideal `v` of `R`, the `v`-adic valuation of `π` is `-1`.
|
IsDedekindDomain.HeightOneSpectrum.int_valuation_le_pow_iff_dvd
theorem IsDedekindDomain.HeightOneSpectrum.int_valuation_le_pow_iff_dvd :
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R)
(r : R) (n : ℕ), v.intValuationDef r ≤ ↑(Multiplicative.ofAdd (-↑n)) ↔ v.asIdeal ^ n ∣ Ideal.span {r}
The theorem `IsDedekindDomain.HeightOneSpectrum.int_valuation_le_pow_iff_dvd` states that for any commutative ring `R` which is a Dedekind domain, any `v` which is a height one prime ideal of `R`, any element `r` of `R`, and any natural number `n`, the `v`-adic valuation of `r` is less than or equal to the multiplicative conversion of `-n` if and only if `v` raised to the power `n` divides the ideal generated by `r`. In other words, this relates the `v`-adic valuation of an element of a Dedekind domain to the divisibility of the ideal generated by that element by the `n`th power of `v`.
More concisely: For a commutative Dedekind domain R, height one prime ideal v, element r in R, and natural number n, the v-adic valuation of r is less than or equal to the power n of v if and only if v^n divides the ideal generated by r.
|
IsDedekindDomain.HeightOneSpectrum.valuation_uniformizer_ne_zero
theorem IsDedekindDomain.HeightOneSpectrum.valuation_uniformizer_ne_zero :
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) [inst_2 : Field K]
[inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R),
Classical.choose ⋯ ≠ 0
This theorem states that for any integral domain `R` that is a Dedekind domain, and any field of fractions `K` of `R`, the uniformizer of the valuation ring of any height one prime ideal of `R` (i.e., an element of the height one spectrum of `R`) is non-zero. The uniformizer is a chosen element that satisfies certain conditions, and this theorem asserts that this chosen element is not zero. The `Classical.choose` function is used to select such an element from the existence proof that there is an element satisfying the conditions.
More concisely: In a Dedekind domain `R`, the uniformizer of any height one prime ideal is a non-zero element.
|
IsDedekindDomain.HeightOneSpectrum.IntValuation.map_one'
theorem IsDedekindDomain.HeightOneSpectrum.IntValuation.map_one' :
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R),
v.intValuationDef 1 = 1
This theorem states that for any commutative ring `R` that is a Dedekind domain, the `v`-adic valuation of the integer `1` is always `1`. Here, `v` refers to any element of the `HeightOneSpectrum` of the Dedekind domain `R`, which essentially represents a prime ideal in the ring. The `v`-adic valuation is a function that measures the maximum power of `v` that divides a given element of the ring.
More concisely: For any commutative Dedekind domain `R` and prime ideal `v` in its height one spectrum, the `v`-adic valuation of the integer `1` is equal to `1`.
|
IsDedekindDomain.HeightOneSpectrum.int_valuation_ne_zero'
theorem IsDedekindDomain.HeightOneSpectrum.int_valuation_ne_zero' :
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R)
(x : ↥(nonZeroDivisors R)), v.intValuationDef ↑x ≠ 0
The theorem `IsDedekindDomain.HeightOneSpectrum.int_valuation_ne_zero'` states that for any commutative ring `R` that is a Dedekind domain, and for any element `x` in the submonoid of non-zero-divisors of `R`, the integer valuation of `x` in the height one spectrum of `R` is non-zero. In more mathematical terms, it asserts that if `v` is a valuation in the height one spectrum of a Dedekind domain `R`, and `x` is a non-zero divisor in `R`, then the integer value assigned by `v` to `x` is non-zero.
More concisely: In a Dedekind domain, every non-zero divisor has non-zero valuation in the height one spectrum.
|
IsDedekindDomain.HeightOneSpectrum.int_valuation_le_one
theorem IsDedekindDomain.HeightOneSpectrum.int_valuation_le_one :
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R)
(x : R), v.intValuationDef x ≤ 1
This theorem asserts that for any Dedekind domain `R` and for any `v` of the height-one spectrum of `R`, the `v`-adic valuation of any element `x` of `R` is less than or equal to one. Here, the Dedekind domain is a commutative ring, and the height-one spectrum of a Dedekind domain is a set of prime ideals with height one. The `v`-adic valuation measures the power of `v` in the prime factorization of `x`.
More concisely: For any Dedekind domain R and prime ideal v of height one, the v-adic valuation of every element x in R is less than or equal to one.
|
IsDedekindDomain.HeightOneSpectrum.IntValuation.map_add_le_max'
theorem IsDedekindDomain.HeightOneSpectrum.IntValuation.map_add_le_max' :
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R)
(x y : R), v.intValuationDef (x + y) ≤ max (v.intValuationDef x) (v.intValuationDef y)
This theorem states that in a commutative ring R, which is a Dedekind domain, the `v`-adic valuation of the sum of any two elements, `x` and `y`, is less than or equal to the maximum of their individual `v`-adic valuations. The `v`-adic valuation is a measure of the multiplicity of a prime `v` in the factorization of a number in the ring R. Here, the `v`-adic valuation is represented by `v.intValuationDef`. The function `max` takes two inputs and returns the greater of them.
More concisely: In a commutative Dedekind domain R, the `v`-adic valuation of the sum of two elements x and y is less than or equal to the maximum of their individual `v`-adic valuations: `v.intValuationDef x + v.intValuationDef y ≤ max (v.intValuationDef x) (v.intValuationDef y)`.
|
IsDedekindDomain.HeightOneSpectrum.IntValuation.map_mul'
theorem IsDedekindDomain.HeightOneSpectrum.IntValuation.map_mul' :
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R)
(x y : R), v.intValuationDef (x * y) = v.intValuationDef x * v.intValuationDef y
This theorem states that for any commutative ring `R` that also happens to be a Dedekind domain, and a valuation `v` from the height-one spectrum of `R`, the valuation of the product of any two elements `x` and `y` from `R` equals the product of their individual valuations. That is, the valuation function preserves multiplication.
More concisely: For any commutative Dedekind domain `R` and valuation `v` on its height-one spectrum, the valuation of the product of two elements `x` and `y` in `R` is equal to the sum of the individual valuations of `x` and `y`: `v(xy) = v(x) + v(y)`.
|
IsDedekindDomain.HeightOneSpectrum.mem_adicCompletionIntegers
theorem IsDedekindDomain.HeightOneSpectrum.mem_adicCompletionIntegers :
∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) [inst_2 : Field K]
[inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R)
{x : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v},
x ∈ IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v ↔ Valued.v x ≤ 1
The theorem `IsDedekindDomain.HeightOneSpectrum.mem_adicCompletionIntegers` states that for any commutative ring `R` which is a Dedekind domain, a field `K` which is a fraction field of `R`, and a height one prime `v` of `R`, an element `x` of the `v`-adic completion of `K` is in the ring of integers of this `v`-adic completion if and only if its valuation is less than or equal to 1. The `v`-adic completion of `K` is a completion of `K` with respect to its `v`-adic valuation. The ring of integers of this `v`-adic completion is a subring of the `v`-adic completion. A valuation of `x` maps `x` to an element in a linearly ordered commutative group with zero.
More concisely: For a commutative Dedekind domain R with fraction field K and height one prime v, an element x of the v-adic completion of K belongs to the subring of integers if and only if its valuation is less than or equal to 1.
|
IsDedekindDomain.HeightOneSpectrum.int_valuation_exists_uniformizer
theorem IsDedekindDomain.HeightOneSpectrum.int_valuation_exists_uniformizer :
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R),
∃ π, v.intValuationDef π = ↑(Multiplicative.ofAdd (-1))
This theorem states that for any commutative ring `R` with the property of being a Dedekind domain, and for any `v` which is an element of the height one spectrum of `R`, there exists an element `π` in `R` such that the `v`-adic valuation of `π` is equal to the multiplicative interpretation of `-1`. The `v`-adic valuation is a way of measuring the 'size' of `π` with respect to `v`, and the Multiplicative.ofAdd function simply converts the additive `-1` into its multiplicative equivalent.
More concisely: For any commutative Dedekind domain `R` and height-1 prime ideal `v`, there exists an element `π` in `R` with `v`-adic valuation equal to the multiplicative inverse of `1`.
|