The class group of the S-integers

For a Dedekind domain R with fraction field K and a set S of height one primes, the class group of the ring 𝒪_S of S-integers is the class group of R modulo the classes of the primes in S:

IsDedekindDomain.integerClassGroupEquiv : ClassGroup 𝒪_S ≃* ClassGroup R ⧸ ⟨[v] : v ∈ S⟩.

Main definitions

• IsDedekindDomain.integerClassGroupEquiv: the isomorphism above.

Main results

• IsDedekindDomain.finite_integer_classGroup: Cl(𝒪_S) is finite whenever Cl(R) is.
• IsDedekindDomain.integer_extendedHom_mk0_idealUnder: the class of I is extended from the class of its contraction — the explicit preimage witnessing surjectivity, so a consumer holding a concrete I need not go through Exists.choose.
• IsDedekindDomain.integerClassGroupEquiv_symm_mk, ..._extendedHom and ..._mk0: how the isomorphism evaluates, on a class extended from Cl(R) and on a concrete ClassGroup.mk0.

The proof is the first isomorphism theorem applied to extension of ideals Cl(R) → Cl(𝒪_S):

• IsDedekindDomain.integer_extendedHom_surjective: extension is surjective, because every ideal of 𝒪_S is extended from R (integer_map_comap_eq);
• IsDedekindDomain.ker_integer_extendedHom: its kernel is generated by the classes of the primes in S. One inclusion is that a prime of S extends to ⊤ (integer_map_asIdeal_eq_top); the other compares multiplicities off S, which is what IsDedekindDomain.integer_count_coeIdeal_map and IsDedekindDomain.integer_count_spanSingleton supply — they are in TauCeti/RingTheory/DedekindDomain/SInteger/Factorization.lean, since neither mentions the class group — and then applies ClassGroup.mk0_mem_closure_of_count_eq.

IsDedekindDomain.finite_integer_classGroup is the consequence the arithmetic wants: Cl(𝒪_S) is finite whenever Cl(R) is, being a quotient of it. That is one of the two finiteness inputs to weak Mordell–Weil (the other being the S-unit theorem), so this advances TauCetiRoadmap/EllipticCurves/README.md §Layer 6 (Mordell–Weil), whose Kummer argument needs E(K)/2E(K) finite.

Adapted from Michael Stoll's elliptic-curves formalisation (github.com/MichaelStollBayreuth/EllipticCurves, EllipticCurves/Mathlib/SIntegers.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. Stoll's unprefixed names are given the integer prefix that TauCeti/RingTheory/DedekindDomain/SInteger/ already uses.

theorem IsDedekindDomain.integer_extendedHom_mk0_idealUnder {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Set (HeightOneSpectrum R)) (I : ↥(nonZeroDivisors (Ideal ↥(S.integer K)))) : (ClassGroup.extendedHom R ↥(S.integer K)) (ClassGroup.mk0 (integerIdealUnder K S I)) = ClassGroup.mk0 I

The explicit preimage under extension: the class of I is extended from the class of the contraction of I to R. Every ideal of 𝒪_S is generated by its contraction (integer_map_comap_eq), so extending the contraction returns I.

This is the content of integer_extendedHom_surjective, stated rather than hidden inside an existential: a consumer holding a concrete I can name its preimage instead of recovering it from Exists.choose.

theorem IsDedekindDomain.integer_extendedHom_surjective {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Set (HeightOneSpectrum R)) : Function.Surjective ⇑(ClassGroup.extendedHom R ↥(S.integer K))

Extension of ideals Cl(R) → Cl(𝒪_S) is surjective.

instance IsDedekindDomain.finite_integer_classGroup {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Set (HeightOneSpectrum R)) [Finite (ClassGroup R)] : Finite (ClassGroup ↥(S.integer K))

The class group of 𝒪_S is finite as soon as that of R is, being a quotient of it. This is one of the two finiteness inputs to weak Mordell–Weil.

theorem IsDedekindDomain.ker_integer_extendedHom {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Set (HeightOneSpectrum R)) : (ClassGroup.extendedHom R ↥(S.integer K)).ker = Subgroup.closure (HeightOneSpectrum.classGroupMk '' S)

The kernel of extension is exactly the subgroup generated by the classes of the primes in S.

noncomputable def IsDedekindDomain.integerClassGroupEquiv {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Set (HeightOneSpectrum R)) : ClassGroup ↥(S.integer K) ≃* ClassGroup R ⧸ Subgroup.closure (HeightOneSpectrum.classGroupMk '' S)

The class group of the S-integers. Cl(𝒪_S) is Cl(R) modulo the classes of the primes in S: the first isomorphism theorem applied to extension of ideals.

Equations

• IsDedekindDomain.integerClassGroupEquiv K S = (QuotientGroup.quotientKerEquivOfSurjective (ClassGroup.extendedHom R ↥(S.integer K)) ⋯).symm.trans (QuotientGroup.quotientMulEquivOfEq ⋯)

@[simp]

theorem IsDedekindDomain.integerClassGroupEquiv_extendedHom {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Set (HeightOneSpectrum R)) (c : ClassGroup R) : (integerClassGroupEquiv K S) ((ClassGroup.extendedHom R ↥(S.integer K)) c) = ↑c

integerClassGroupEquiv in the stated direction: the class extended from c : Cl(R) maps to the class of c in the quotient.

@[simp]

theorem IsDedekindDomain.integerClassGroupEquiv_symm_mk {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Set (HeightOneSpectrum R)) (c : ClassGroup R) : (integerClassGroupEquiv K S).symm ↑c = (ClassGroup.extendedHom R ↥(S.integer K)) c

integerClassGroupEquiv inverts extension: the class of c in the quotient corresponds to the class extended from c : Cl(R). The symm counterpart of integerClassGroupEquiv_extendedHom.

@[simp]

theorem IsDedekindDomain.integerClassGroupEquiv_mk0 {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Set (HeightOneSpectrum R)) (I : ↥(nonZeroDivisors (Ideal ↥(S.integer K)))) : (integerClassGroupEquiv K S) (ClassGroup.mk0 I) = ↑(ClassGroup.mk0 (integerIdealUnder K S I))

integerClassGroupEquiv evaluated on a concrete ideal: the class of I corresponds to the class of the contraction of I to R. This is the evaluation to use when the argument is literally a ClassGroup.mk0; integerClassGroupEquiv_extendedHom is the one phrased through extension.