Finite approximation in Dedekind domains

This file gives the finite approximation theorem in the form used to patch local data over a Dedekind domain. Given residue classes modulo powers of the maximal ideals in finitely many localizations, one global element realizes all of them.

The proof combines the Chinese remainder theorem Ideal.pi_quotient_surjective with the canonical comparison IsLocalization.AtPrime.equivQuotMaximalIdealPow between a prime-power quotient and the corresponding quotient after localization.

Main results

• TauCeti.DedekindDomain.exists_eq_mod_localized_prime_pow: simultaneous approximation of finitely many classes in localized prime-power quotients.
• TauCeti.DedekindDomain.exists_forall_sub_mem_map_localizationAtPrime: one element of R agrees with a prescribed element of every localization R_v modulo a fixed nonzero ideal. Only the finitely many primes containing the ideal impose a condition.
• TauCeti.DedekindDomain.exists_forall_sub_mem_span_singleton_localizationAtPrime: the specialization to a nonzero principal modulus.

This is the finite approximation input for the local-to-global patching arguments in Silverman, The Arithmetic of Elliptic Curves, Chapter VIII, Section 8.

theorem TauCeti.DedekindDomain.exists_eq_mod_localized_prime_pow {R : Type u_1} {ι : Type u_2} [CommRing R] [IsDedekindDomain R] [Finite ι] (v : ι → IsDedekindDomain.HeightOneSpectrum R) (hv : Function.Injective v) (n : ι → ℕ) (x : (i : ι) → Localization.AtPrime (v i).asIdeal ⧸ IsLocalRing.maximalIdeal (Localization.AtPrime (v i).asIdeal) ^ n i) : ∃ (a : R), ∀ (i : ι), (Ideal.Quotient.mk (IsLocalRing.maximalIdeal (Localization.AtPrime (v i).asIdeal) ^ n i)) ((algebraMap R (Localization.AtPrime (v i).asIdeal)) a) = x i

Finite approximation at height-one primes.

For pairwise distinct height-one primes v i, arbitrary residue classes modulo the indicated powers of the maximal ideals of R_{v i} are simultaneously represented by a single element of R.

Allowing exponent zero is harmless: the corresponding quotient is the zero ring, so that component imposes no condition.

theorem TauCeti.DedekindDomain.exists_forall_sub_mem_map_localizationAtPrime {R : Type u_1} [CommRing R] [IsDedekindDomain R] {I : Ideal R} (hI : I ≠ ⊥) (x : (v : IsDedekindDomain.HeightOneSpectrum R) → Localization.AtPrime v.asIdeal) : ∃ (a : R), ∀ (v : IsDedekindDomain.HeightOneSpectrum R), (algebraMap R (Localization.AtPrime v.asIdeal)) a - x v ∈ Ideal.map (algebraMap R (Localization.AtPrime v.asIdeal)) I

Approximation modulo a nonzero ideal at every height-one prime.

Given an element x v of every localization R_v, a single a ∈ R is congruent to each x v modulo the extension of I to R_v. The family is indexed by all height-one primes; only the finitely many containing I constrain a, since at every other prime the extension is the unit ideal.

theorem TauCeti.DedekindDomain.exists_forall_sub_mem_span_singleton_localizationAtPrime {R : Type u_1} [CommRing R] [IsDedekindDomain R] {d : R} (hd : d ≠ 0) (x : (v : IsDedekindDomain.HeightOneSpectrum R) → Localization.AtPrime v.asIdeal) : ∃ (a : R), ∀ (v : IsDedekindDomain.HeightOneSpectrum R), (algebraMap R (Localization.AtPrime v.asIdeal)) a - x v ∈ Ideal.span {(algebraMap R (Localization.AtPrime v.asIdeal)) d}

Approximation modulo a nonzero element at every height-one prime.

Given an element x v of every localization R_v, a single a ∈ R is congruent to each x v modulo d. Only the finitely many primes containing d constrain a.