Ideal classes generated by a set of height one primes

Closure statements about which ideal classes a set T of height one primes generates: if the v-adic multiplicities of a fractional ideal are controlled outside T, its class lies in the subgroup generated by {[v] : v ∈ T}, where [v] is IsDedekindDomain.HeightOneSpectrum.classGroupMk from TauCeti.RingTheory.ClassGroup.Basic.

Main results

• ClassGroup.mk_mem_closure_of_count_eq_zero: if the multiplicities of a unit fractional ideal vanish outside T, its class lies in Subgroup.closure (classGroupMk '' T).
• ClassGroup.mk_mem_closure_of_count_eq: the same when the multiplicities merely agree outside T with those of a principal fractional ideal (x).
• ClassGroup.mk0_mem_closure_of_count_eq: the integral-ideal specialisation, the form the S-integer material consumes.

The first is the image under ClassGroup.mk of FractionalIdeal.mem_closure_unitOfPrime_of_count_eq_zero, the corresponding statement for invertible fractional ideals. Nothing here mentions Weil divisors, so RingTheory and NumberTheory consumers can reach these results without importing TauCeti.AlgebraicGeometry.

These are an input to what TauCetiRoadmap/EllipticCurves/README.md §Layer 6 needs for weak Mordell–Weil. That argument exhibits the S-class group as a quotient of the class group by the classes of S, and concludes it is finite; neither the S-class group nor that quotient is defined here — this file supplies only the generation statements the argument rests on.

Adapted from Michael Stoll's elliptic-curves formalisation (github.com/MichaelStollBayreuth/EllipticCurves, EllipticCurves/Mathlib/FractionalIdeal.lean at the roadmap's 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.

theorem ClassGroup.mk_mem_closure_of_count_eq_zero {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {T : Set (IsDedekindDomain.HeightOneSpectrum R)} {I : (FractionalIdeal (nonZeroDivisors R) K)ˣ} (h : ∀ v ∉ T, FractionalIdeal.count K v ↑I = 0) : (mk K) I ∈ Subgroup.closure (IsDedekindDomain.HeightOneSpectrum.classGroupMk '' T)

If the v-adic multiplicities of a unit fractional ideal vanish outside a set T of height one primes, its ideal class lies in the subgroup generated by the classes of the primes in T.

theorem ClassGroup.mk_mem_closure_of_count_eq {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_3) [Field K] [Algebra R K] [IsFractionRing R K] {T : Set (IsDedekindDomain.HeightOneSpectrum R)} {I : (FractionalIdeal (nonZeroDivisors R) K)ˣ} (x : Kˣ) (h : ∀ v ∉ T, FractionalIdeal.count K v ↑I = FractionalIdeal.count K v (FractionalIdeal.spanSingleton (nonZeroDivisors R) ↑x)) : (mk K) I ∈ Subgroup.closure (IsDedekindDomain.HeightOneSpectrum.classGroupMk '' T)

If the v-adic multiplicities of a unit fractional ideal agree outside a set T of height one primes with those of a principal fractional ideal (x), then its class lies in the subgroup generated by the classes of the primes in T.

theorem ClassGroup.mk0_mem_closure_of_count_eq {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_3) [Field K] [Algebra R K] [IsFractionRing R K] {T : Set (IsDedekindDomain.HeightOneSpectrum R)} {J : ↥(nonZeroDivisors (Ideal R))} (x : Kˣ) (h : ∀ v ∉ T, FractionalIdeal.count K v ↑↑J = FractionalIdeal.count K v (FractionalIdeal.spanSingleton (nonZeroDivisors R) ↑x)) : mk0 J ∈ Subgroup.closure (IsDedekindDomain.HeightOneSpectrum.classGroupMk '' T)

The integral-ideal form of ClassGroup.mk_mem_closure_of_count_eq: if the multiplicities of a nonzero ideal J agree outside T with those of a principal fractional ideal (x), then the class of J lies in the subgroup generated by the classes of the primes in T.