Documentation

TauCeti.RingTheory.DedekindDomain.SInteger.Factorization

Multiplicities transfer to the S-integers #

For v ∉ S, extension of ideals along R → 𝒪_S preserves the multiplicity at v: the multiplicity of the extension at the prime integerPrimeOverOfNotMem above v is the multiplicity of the original at v.

Main results #

These are the multiplicative analogue of the valuation-transfer lemmas valuation_integerPrimeOverOfNotMem and valuation_integerHeightOneSpectrumEquiv in SInteger/Spectrum.lean, and they are what the S-class-group computation in SInteger/ClassGroup.lean runs on. They live in their own module rather than in Spectrum.lean because they need FractionalIdeal.count, and Spectrum.lean does not otherwise depend on the factorization layer — a consumer of the valuation transfer alone should not pay for it.

Both are adapted from Michael Stoll's elliptic-curves formalisation (github.com/MichaelStollBayreuth/EllipticCurves, EllipticCurves/Mathlib/SIntegers.lean at the roadmap's §Provenance pin 66889eada51a, Apache 2.0, by Michael Stoll). Following this repository's convention for adapted material, the upstream authorship is credited here rather than in the copyright header. Stoll's unprefixed names are given the integer prefix that TauCeti/RingTheory/DedekindDomain/SInteger/ already uses.

source
@[simp]
theorem IsDedekindDomain.integer_count_coeIdeal_map {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Set (HeightOneSpectrum R)) {v : HeightOneSpectrum R} (hv : v ∉ S) {J : Ideal R} :
FractionalIdeal.count K (integerPrimeOverOfNotMem K S hv) ↑(Ideal.map (algebraMap R ↥(S.integer K)) J) = FractionalIdeal.count K v ↑J

The multiplicity of the extension of an ideal at the prime above v ∉ S is the multiplicity at v.

source
@[simp]
theorem IsDedekindDomain.integer_count_spanSingleton {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Set (HeightOneSpectrum R)) {v : HeightOneSpectrum R} (hv : v ∉ S) {x : K} :
FractionalIdeal.count K (integerPrimeOverOfNotMem K S hv) (FractionalIdeal.spanSingleton (nonZeroDivisors ↥(S.integer K)) x) = FractionalIdeal.count K v (FractionalIdeal.spanSingleton (nonZeroDivisors R) x)

The multiplicity of a principal fractional ideal at the prime above v ∉ S is the multiplicity at v.