Units of a Dedekind domain as S-units

Let R be a Dedekind domain with fraction field K. Every unit of R is an S-unit, for any set S of height-one primes of R. This module records the resulting canonical homomorphism TauCeti.SUnit.unitOfUnits S K : Rˣ →* S.unit K, the composite of Set.unitEmptyEquivUnits with the inclusion Set.unit_mono of the ∅-units in the S-units.

For R the ring of integers of a number field, it is the inclusion used to compare Dirichlet's logarithmic embedding of ordinary units with the logarithmic embedding of S-units.

noncomputable def TauCeti.SUnit.unitOfUnits {R : Type u_1} [CommRing R] [IsDedekindDomain R] (S : Set (IsDedekindDomain.HeightOneSpectrum R)) (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] : Rˣ →* ↥(S.unit K)

The canonical homomorphism from the units of a Dedekind domain to the S-units of its fraction field.

theorem TauCeti.SUnit.val_unitOfUnits {R : Type u_1} [CommRing R] [IsDedekindDomain R] (S : Set (IsDedekindDomain.HeightOneSpectrum R)) (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (u : Rˣ) : ↑↑((unitOfUnits S K) u) = (algebraMap R K) ↑u

The underlying element of K of the S-unit attached to a unit u of R is the image of u under the algebra map R → K.

@[simp]

theorem TauCeti.SUnit.coe_unitOfUnits {R : Type u_1} [CommRing R] [IsDedekindDomain R] (S : Set (IsDedekindDomain.HeightOneSpectrum R)) (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (u : Rˣ) : ↑((unitOfUnits S K) u) = (Units.map ↑(algebraMap R K)) u

As a unit of K, the S-unit attached to a unit u of R is the image of u under the map of unit groups induced by the algebra map R → K.