S-integers and S-units of fraction fields of Dedekind domains

Let K be the field of fractions of a Dedekind domain R, and let S be a set of prime ideals in the height one spectrum of R. An S-integer of K is defined to have v-adic valuation at most one for all primes ideals v away from S, whereas an S-unit of Kˣ is defined to have v-adic valuation exactly one for all prime ideals v away from S.

This file defines the subalgebra of S-integers of K and the subgroup of S-units of Kˣ, where K can be specialised to the case of a number field or a function field separately.

Main definitions

• Set.integer: S-integers.
• Set.unit: S-units.
• Localization.submonoid: the submonoid of non-zero elements of R that are not contained in any prime ideal away from S.

Main statements

• IsDedekindDomain.isLocalizationSInteger: The ring of S-integers is a localization of R if every class in the class group has finite order.
• IsDedekindDomain.isDedekindDomainSInteger: The ring of S-integers of a Dedekind domain with every class in the class group of finite order is a Dedekind domain.
• Set.unitEquivUnitsInteger: S-units are units of S-integers.
• IsDedekindDomain.integer_empty: ∅-integers is the usual ring of integers.
• TODO: proof that S-units is the kernel of a map to a product.
• TODO: finite generation of S-units and Dirichlet's S-unit theorem.

References

• D Marcus, Number Fields
• J W S Cassels, A Fröhlich, Algebraic Number Theory
• J Neukirch, Algebraic Number Theory

Tags

S integer, S-integer, S unit, S-unit

S-integers

noncomputable def Set.integer {R : Type u} [CommRing R] (S : Set (IsDedekindDomain.HeightOneSpectrum R)) (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] : Subalgebra R K

The R-subalgebra of S-integers of K.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Set.coe_integer {R : Type u} [CommRing R] (S : Set (IsDedekindDomain.HeightOneSpectrum R)) (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] : ↑(S.integer K) = {x : K | ∀ v ∉ S, (IsDedekindDomain.HeightOneSpectrum.valuation K v) x ≤ 1}

theorem Set.integer_eq {R : Type u} [CommRing R] (S : Set (IsDedekindDomain.HeightOneSpectrum R)) (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] : (S.integer K).toSubring = ⨅ (v : IsDedekindDomain.HeightOneSpectrum R), ⨅ (_ : v ∉ S), (IsDedekindDomain.HeightOneSpectrum.valuation K v).valuationSubring.toSubring

theorem Set.integer_valuation_le_one {R : Type u} [CommRing R] (S : Set (IsDedekindDomain.HeightOneSpectrum R)) (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] (x : ↥(S.integer K)) {v : IsDedekindDomain.HeightOneSpectrum R} (hv : v ∉ S) : (IsDedekindDomain.HeightOneSpectrum.valuation K v) ↑x ≤ 1

def Localization.submonoid {R : Type u} [CommRing R] (S : Set (IsDedekindDomain.HeightOneSpectrum R)) : Submonoid R

The submonoid of non-zero elements of R that are not contained in any non-zero prime ideal away from S.

Equations

• Localization.submonoid S = Ideal.sInfPrimeCompl ((fun (v : IsDedekindDomain.HeightOneSpectrum R) => v.asIdeal) '' Sᶜ) ⋯ ⊓ nonZeroDivisors R

@[simp]

theorem Localization.mem_submonoid_iff {R : Type u} [CommRing R] (S : Set (IsDedekindDomain.HeightOneSpectrum R)) {r : R} : r ∈ submonoid S ↔ (∀ v ∉ S, r ∉ v.asIdeal) ∧ r ∈ nonZeroDivisors R

@[simp]

theorem Localization.submonoid_eq_primeCompl {R : Type u} [CommRing R] (P : IsDedekindDomain.HeightOneSpectrum R) : submonoid {P}ᶜ = P.asIdeal.primeCompl ⊓ nonZeroDivisors R

theorem Localization.submonoid_le_nonZeroDivisors {R : Type u} [CommRing R] (S : Set (IsDedekindDomain.HeightOneSpectrum R)) : submonoid S ≤ nonZeroDivisors R

instance instFactIsMulTorsionClassGroupOfFinite {R : Type u} [CommRing R] [IsDomain R] [Finite (ClassGroup R)] : Fact (IsMulTorsion (ClassGroup R))

@[simp]

theorem IsDedekindDomain.integer_univ (R : Type u) [CommRing R] (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] : Set.univ.integer K = ⊤

If S is the whole set of places of K, then the S-integers are the whole of K.

@[simp]

theorem IsDedekindDomain.integer_empty (R : Type u) [CommRing R] (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] : ∅.integer K = ⊥

If S is the empty set, then the S-integers are the minimal R-subalgebra of K (which is just R itself, via Algebra.botEquivOfInjective and IsFractionRing.injective).

theorem IsDedekindDomain.exists_mul_algebraMap_eq_algebraMap (R : Type u) [CommRing R] (S : Set (HeightOneSpectrum R)) (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] [Fact (IsMulTorsion (ClassGroup R))] (z : ↥(S.integer K)) : ∃ (x : R × ↥(Localization.submonoid S)), z * (algebraMap R ↥(S.integer K)) ↑x.2 = (algebraMap R ↥(S.integer K)) x.1

instance IsDedekindDomain.isLocalizationSInteger (R : Type u) [CommRing R] (S : Set (HeightOneSpectrum R)) (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] [Fact (IsMulTorsion (ClassGroup R))] : IsLocalization (Localization.submonoid S) ↥(S.integer K)

When every class in the class group has finite order, the ring of S-integers is the localization of R at Localization.submonoid S, the submonoid of non-zero elements of R not contained in any prime ideal away from S.

instance IsDedekindDomain.isDedekindDomainSInteger (R : Type u) [CommRing R] (S : Set (HeightOneSpectrum R)) (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] [Fact (IsMulTorsion (ClassGroup R))] : IsDedekindDomain ↥(S.integer K)

The ring of S-integers is a Dedekind domain when every element in class group has finite order.

S-units

noncomputable def Set.unit {R : Type u} [CommRing R] (S : Set (IsDedekindDomain.HeightOneSpectrum R)) (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] : Subgroup Kˣ

The subgroup of S-units of Kˣ.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Set.coe_unit {R : Type u} [CommRing R] (S : Set (IsDedekindDomain.HeightOneSpectrum R)) (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] : ↑(S.unit K) = {x : Kˣ | ∀ v ∉ S, (IsDedekindDomain.HeightOneSpectrum.valuation K v) ↑x = 1}

theorem Set.unit_eq {R : Type u} [CommRing R] (S : Set (IsDedekindDomain.HeightOneSpectrum R)) (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] : S.unit K = ⨅ (v : IsDedekindDomain.HeightOneSpectrum R), ⨅ (_ : v ∉ S), (IsDedekindDomain.HeightOneSpectrum.valuation K v).valuationSubring.unitGroup

theorem Set.unit_valuation_eq_one {R : Type u} [CommRing R] (S : Set (IsDedekindDomain.HeightOneSpectrum R)) (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] (x : ↥(S.unit K)) {v : IsDedekindDomain.HeightOneSpectrum R} (hv : v ∉ S) : (IsDedekindDomain.HeightOneSpectrum.valuation K v) ↑↑x = 1

def Set.unitEquivUnitsInteger {R : Type u} [CommRing R] (S : Set (IsDedekindDomain.HeightOneSpectrum R)) (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] : ↥(S.unit K) ≃* (↥(S.integer K))ˣ

The group of S-units is the group of units of the ring of S-integers.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Set.val_unitEquivUnitsInteger_apply_coe {R : Type u} [CommRing R] (S : Set (IsDedekindDomain.HeightOneSpectrum R)) (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] (x : ↥(S.unit K)) : ↑↑((S.unitEquivUnitsInteger K) x) = ↑↑x

@[simp]

theorem Set.unitEquivUnitsInteger_symm_apply_coe {R : Type u} [CommRing R] (S : Set (IsDedekindDomain.HeightOneSpectrum R)) (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R] (x : (↥(S.integer K))ˣ) : ↑((S.unitEquivUnitsInteger K).symm x) = Units.mk0 ↑↑x ⋯