Membership in a localization realized inside the fraction field

Mathlib's Localization.subalgebra.ofField K S hS is the localization of a ring A at a submonoid S of non-zero-divisors, realized as the A-subalgebra of the fraction field K of A consisting of the quotients a / s with a ∈ A and s ∈ S. This file adds the membership tests that make it usable as a subring of K: an element z : K lies in it exactly when some s ∈ S clears its denominator, s * z ∈ A, and for S = powers x exactly when some power of x does so. It also records that the localization of a Dedekind domain, so realized, is again a Dedekind domain.

Main results

• Localization.subalgebra.mem_ofField_iff_exists_mul_mem_range and Localization.subalgebra.mem_ofField_powers_iff: membership in A[S⁻¹] ⊆ K, respectively in A[1/x] ⊆ K, by clearing denominators.
• Localization.subalgebra.isDedekindDomain_ofField: A[S⁻¹] ⊆ K is a Dedekind domain when A is.

theorem Localization.subalgebra.mem_ofField_iff_exists_mul_mem_range {A : Type u_1} {K : Type u_2} [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] (S : Submonoid A) (hS : S ≤ nonZeroDivisors A) {z : K} : z ∈ ofField K S hS ↔ ∃ s ∈ S, (algebraMap A K) s * z ∈ (algebraMap A K).range

Membership in A[S⁻¹] ⊆ K by clearing denominators: z lies in the localization exactly when some s ∈ S has s * z ∈ A.

theorem Localization.subalgebra.mem_ofField_powers_iff {A : Type u_1} {K : Type u_2} [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] (x : A) (hx : Submonoid.powers x ≤ nonZeroDivisors A) {z : K} : z ∈ ofField K (Submonoid.powers x) hx ↔ ∃ (n : ℕ), (algebraMap A K) x ^ n * z ∈ (algebraMap A K).range

Membership in A[1/x] ⊆ K: z lies in the localization of A away from x exactly when some power of x clears its denominator, x ^ n * z ∈ A.

instance Localization.subalgebra.isDedekindDomain_ofField {A : Type u_1} {K : Type u_2} [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] (S : Submonoid A) (hS : S ≤ nonZeroDivisors A) [IsDedekindDomain A] : IsDedekindDomain ↥(ofField K S hS)

The localization of a Dedekind domain at a submonoid of nonzero elements, realized inside its fraction field, is a Dedekind domain.