The ideal class group as a quotient of the finite ideles

Let R be a Dedekind domain with fraction field K. A finite idele is a unit of the finite adele ring 𝔸ᶠ[R, K]: a family (x_v) of nonzero elements of the completions K_v, integral with integral inverse at all but finitely many height one primes v. Reading off the v-adic orders of the components attaches an invertible fractional ideal to a finite idele, and this file identifies the ideal class group of R with the quotient of the group of finite ideles by the everywhere-integral units together with the principal finite ideles.

Main definitions

• IsDedekindDomain.FiniteAdeleRing.adicOrd: the v-adic order of a finite idele, normalized so that a uniformizer at v has order 1.
• IsDedekindDomain.FiniteAdeleRing.toFractionalIdeal: the homomorphism from the finite ideles to the invertible fractional ideals whose multiplicity at v is the v-adic order.
• IsDedekindDomain.FiniteAdeleRing.integralUnits: the finite ideles whose components are units of the local integers at every place, that is, the unit group of the integral finite adeles.
• IsDedekindDomain.FiniteAdeleRing.sIntegralUnits: the finite ideles whose components are local units away from a prescribed set of places.
• IsDedekindDomain.FiniteAdeleRing.toClassGroup: the induced homomorphism to ClassGroup R.

Main results

• IsDedekindDomain.FiniteAdeleRing.count_coe_toFractionalIdeal: the multiplicity of v in the fractional ideal of a finite idele is its v-adic order. This is the characterizing property of toFractionalIdeal.
• IsDedekindDomain.FiniteAdeleRing.integralUnits_eq_units_integralAdeles: the everywhere-integral units are the unit group of the integral finite adeles.
• IsDedekindDomain.FiniteAdeleRing.sIntegralUnits_eq_units_sIntegralAdeles: the analogous description of the S-integral units.
• IsDedekindDomain.FiniteAdeleRing.mem_sIntegralUnits_iff_subset: the restricted-product condition: a finite idele is S-integral exactly when S contains its non-unit places.
• IsDedekindDomain.FiniteAdeleRing.toFractionalIdeal_surjective and IsDedekindDomain.FiniteAdeleRing.ker_toFractionalIdeal: the fractional-ideal map is surjective with kernel the everywhere-integral units, so the invertible fractional ideals are the quotient of the finite ideles by 𝒪̂ˣ.
• IsDedekindDomain.FiniteAdeleRing.exists_forall_adicOrd_eq_count: every invertible fractional ideal has a finite-idele representative with the corresponding local orders.
• IsDedekindDomain.FiniteAdeleRing.ker_toClassGroup: the kernel of the class-group map is the subgroup generated by the everywhere-integral units and the principal finite ideles.
• IsDedekindDomain.FiniteAdeleRing.quotientEquivClassGroup: the resulting isomorphism between the quotient of the finite ideles by that subgroup and ClassGroup R.
• IsDedekindDomain.FiniteAdeleRing.toClassGroup_mem_closure_iff: the class of a finite idele lies in the subgroup generated by the classes of a set T of primes exactly when some principal multiple of it is a local unit at every place outside T.
• IsDedekindDomain.FiniteAdeleRing.exists_valued_mul_unitEmbedding_eq_one: if the classes of the primes in T generate the class group, every finite idele is a principal finite idele times a finite idele that is a local unit outside T.
• IsDedekindDomain.FiniteAdeleRing.forall_valued_unitEmbedding_eq_one_iff: the principal finite ideles that are local units outside T are those of the T-units T.unit K.
• IsDedekindDomain.FiniteAdeleRing.comap_unitEmbedding_sIntegralUnits: the subgroup form of the previous result: the principal S-integral finite ideles are those of the S-units.
• IsDedekindDomain.FiniteAdeleRing.map_toClassGroup_sIntegralUnits and IsDedekindDomain.FiniteAdeleRing.sIntegralUnits_sup_range_unitEmbedding_eq_top_iff: the ideal classes of the S-integral finite ideles are the subgroup generated by the classes of the primes in S, so together with the principal finite ideles they generate the finite ideles exactly when these classes generate the class group.

On a principal finite idele the order at v is the v-adic order of the global element it comes from, so toFractionalIdeal extends Mathlib's toPrincipalIdeal along the diagonal embedding of Kˣ: this is IsDedekindDomain.FiniteAdeleRing.toFractionalIdeal_unitEmbedding, and it is what puts the principal finite ideles in the kernel of the class-group map.

The passage between the adic valuation and the multiplicity of a fractional ideal is IsDedekindDomain.HeightOneSpectrum.FractionalIdeal.count_toPrincipalIdeal_eq_neg_log_valuation, and the factorization of an invertible fractional ideal into prime powers is IsDedekindDomain.HeightOneSpectrum.FractionalIdeal.finprod_unitOfPrime_zpow_count.

References

• J. W. S. Cassels and A. Fröhlich, eds., Algebraic Number Theory, Chapter II, §16.
• J. Neukirch, Algebraic Number Theory, Chapter VI, §1.

The local orders of a finite idele

theorem IsDedekindDomain.FiniteAdeleRing.coe_units_apply_ne_zero {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (x : (FiniteAdeleRing R K)ˣ) (v : HeightOneSpectrum R) : ↑x v ≠ 0

Every component of a finite idele is nonzero.

theorem IsDedekindDomain.FiniteAdeleRing.valued_coe_units_apply_ne_zero {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (x : (FiniteAdeleRing R K)ˣ) (v : HeightOneSpectrum R) : Valued.v (↑x v) ≠ 0

The valuation of a component of a finite idele is nonzero.

theorem IsDedekindDomain.FiniteAdeleRing.eventually_valued_coe_units_apply_eq_one {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (x : (FiniteAdeleRing R K)ˣ) : ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, Valued.v (↑x v) = 1

A finite idele is a unit of the local integers at all but finitely many places.

@[simp]

theorem IsDedekindDomain.FiniteAdeleRing.valued_coe_units_inv_apply {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (x : (FiniteAdeleRing R K)ˣ) (v : HeightOneSpectrum R) : Valued.v (↑x⁻¹ v) = (Valued.v (↑x v))⁻¹

The valuations of a finite idele and of its inverse at a place are inverse to each other.

noncomputable def IsDedekindDomain.FiniteAdeleRing.adicOrd {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (x : (FiniteAdeleRing R K)ˣ) (v : HeightOneSpectrum R) : ℤ

The v-adic order of a finite idele x, that is, the exponent of v in the fractional ideal that x defines. The sign is chosen so that a uniformizer at v has order 1.

theorem IsDedekindDomain.FiniteAdeleRing.adicOrd_def {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (x : (FiniteAdeleRing R K)ˣ) (v : HeightOneSpectrum R) : adicOrd x v = -(Valued.v (↑x v)).log

The defining formula for the v-adic order of a finite idele.

@[simp]

theorem IsDedekindDomain.FiniteAdeleRing.adicOrd_eq_zero_iff {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {x : (FiniteAdeleRing R K)ˣ} {v : HeightOneSpectrum R} : adicOrd x v = 0 ↔ Valued.v (↑x v) = 1

The v-adic order vanishes exactly at the places where the idele is a local unit.

@[simp]

theorem IsDedekindDomain.FiniteAdeleRing.adicOrd_one {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : adicOrd 1 v = 0

The unit idele has order 0 everywhere.

@[simp]

theorem IsDedekindDomain.FiniteAdeleRing.adicOrd_mul {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (x y : (FiniteAdeleRing R K)ˣ) (v : HeightOneSpectrum R) : adicOrd (x * y) v = adicOrd x v + adicOrd y v

The v-adic order is additive in the finite idele.

@[simp]

theorem IsDedekindDomain.FiniteAdeleRing.adicOrd_inv {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (x : (FiniteAdeleRing R K)ˣ) (v : HeightOneSpectrum R) : adicOrd x⁻¹ v = -adicOrd x v

The order of the inverse of a finite idele is the negative of its order.

theorem IsDedekindDomain.FiniteAdeleRing.eventually_adicOrd_eq_zero {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (x : (FiniteAdeleRing R K)ˣ) : ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, adicOrd x v = 0

A finite idele has order 0 at all but finitely many places.

theorem IsDedekindDomain.FiniteAdeleRing.hasFiniteMulSupport_unitOfPrime_zpow_adicOrd {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (x : (FiniteAdeleRing R K)ˣ) : (Function.mulSupport fun (v : HeightOneSpectrum R) => v.unitOfPrime K ^ adicOrd x v).Finite

The prime powers cut out by the orders of a finite idele have finite multiplicative support, so their product over all height one primes is defined.

The fractional ideal of a finite idele

noncomputable def IsDedekindDomain.FiniteAdeleRing.toFractionalIdeal {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] : (FiniteAdeleRing R K)ˣ →* (FractionalIdeal (nonZeroDivisors R) K)ˣ

The invertible fractional ideal ∏_v v ^ ord_v(x) attached to a finite idele x.

theorem IsDedekindDomain.FiniteAdeleRing.toFractionalIdeal_apply {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (x : (FiniteAdeleRing R K)ˣ) : toFractionalIdeal x = ∏ᶠ (v : HeightOneSpectrum R), v.unitOfPrime K ^ adicOrd x v

The defining prime factorization of the fractional ideal of a finite idele.

@[simp]

theorem IsDedekindDomain.FiniteAdeleRing.count_coe_toFractionalIdeal {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (x : (FiniteAdeleRing R K)ˣ) (v : HeightOneSpectrum R) : FractionalIdeal.count K v ↑(toFractionalIdeal x) = adicOrd x v

The characterizing property of toFractionalIdeal: the multiplicity of v in the fractional ideal of a finite idele is its v-adic order.

@[simp]

theorem IsDedekindDomain.FiniteAdeleRing.toFractionalIdeal_eq_one_iff {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {x : (FiniteAdeleRing R K)ˣ} : toFractionalIdeal x = 1 ↔ ∀ (v : HeightOneSpectrum R), adicOrd x v = 0

A finite idele defines the trivial fractional ideal exactly when all its orders vanish.

theorem IsDedekindDomain.FiniteAdeleRing.toFractionalIdeal_surjective {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] : Function.Surjective ⇑toFractionalIdeal

Every invertible fractional ideal comes from a finite idele.

theorem IsDedekindDomain.FiniteAdeleRing.exists_forall_adicOrd_eq_count {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (I : (FractionalIdeal (nonZeroDivisors R) K)ˣ) : ∃ (x : (FiniteAdeleRing R K)ˣ), ∀ (v : HeightOneSpectrum R), adicOrd x v = FractionalIdeal.count K v ↑I

Every invertible fractional ideal has a finite-idele representative whose order at each place is the multiplicity of that place in the ideal.

The everywhere-integral units

def IsDedekindDomain.FiniteAdeleRing.integralUnits (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] : Subgroup (FiniteAdeleRing R K)ˣ

The finite ideles that are units of the local integers at every place: the unit group of the integral finite adeles ∏_v 𝒪_v.

@[simp]

theorem IsDedekindDomain.FiniteAdeleRing.mem_integralUnits_iff {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {x : (FiniteAdeleRing R K)ˣ} : x ∈ integralUnits R K ↔ ∀ (v : HeightOneSpectrum R), Valued.v (↑x v) = 1

Membership in integralUnits, unfolded.

The S-integral units

def IsDedekindDomain.FiniteAdeleRing.sIntegralUnits (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Set (HeightOneSpectrum R)) : Subgroup (FiniteAdeleRing R K)ˣ

The S-integral finite ideles: the finite ideles whose components are units of the local integers at every place outside S. These are the unit group of the S-integral finite adeles ∏_{v ∈ S} K_v × ∏_{v ∉ S} 𝒪_v.

@[simp]

theorem IsDedekindDomain.FiniteAdeleRing.mem_sIntegralUnits_iff {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {S : Set (HeightOneSpectrum R)} {x : (FiniteAdeleRing R K)ˣ} : x ∈ sIntegralUnits R K S ↔ ∀ v ∉ S, Valued.v (↑x v) = 1

A finite idele is S-integral exactly when its components outside S have valuation one.

theorem IsDedekindDomain.FiniteAdeleRing.mem_sIntegralUnits_iff_subset {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {S : Set (HeightOneSpectrum R)} {x : (FiniteAdeleRing R K)ˣ} : x ∈ sIntegralUnits R K S ↔ {v : HeightOneSpectrum R | Valued.v (↑x v) ≠ 1} ⊆ S

The restricted-product condition, in terms of S-integral finite ideles. A finite idele is S-integral exactly when S contains the finitely many places (IsDedekindDomain.FiniteAdeleRing.eventually_valued_coe_units_apply_eq_one) at which it is not a local unit.

@[simp]

theorem IsDedekindDomain.FiniteAdeleRing.sIntegralUnits_empty (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] : sIntegralUnits R K ∅ = integralUnits R K

The ∅-integral finite ideles are the everywhere-integral units.

@[simp]

theorem IsDedekindDomain.FiniteAdeleRing.sIntegralUnits_univ (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] : sIntegralUnits R K Set.univ = ⊤

Every finite idele is integral outside the set of all finite places.

theorem IsDedekindDomain.FiniteAdeleRing.sIntegralUnits_mono (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] : Monotone (sIntegralUnits R K)

Allowing more non-integral places gives a larger group of S-integral finite ideles.

theorem IsDedekindDomain.FiniteAdeleRing.mem_sIntegralUnits_iff_mem_sIntegralAdeles {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {S : Set (HeightOneSpectrum R)} {x : (FiniteAdeleRing R K)ˣ} : x ∈ sIntegralUnits R K S ↔ ↑x ∈ sIntegralAdeles R K S ∧ ↑x⁻¹ ∈ sIntegralAdeles R K S

A finite idele is S-integral exactly when both it and its inverse are S-integral finite adeles.

theorem IsDedekindDomain.FiniteAdeleRing.sIntegralUnits_eq_units_sIntegralAdeles (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Set (HeightOneSpectrum R)) : sIntegralUnits R K S = (sIntegralAdeles R K S).units

The S-integral finite ideles are the unit group of the S-integral finite adeles.

theorem IsDedekindDomain.FiniteAdeleRing.mem_integralUnits_iff_forall_mem_adicCompletionIntegers {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {x : (FiniteAdeleRing R K)ˣ} : x ∈ integralUnits R K ↔ ∀ (v : HeightOneSpectrum R), ↑x v ∈ HeightOneSpectrum.adicCompletionIntegers K v ∧ ↑x⁻¹ v ∈ HeightOneSpectrum.adicCompletionIntegers K v

A finite idele is an everywhere-integral unit exactly when both it and its inverse are integral at every place.

theorem IsDedekindDomain.FiniteAdeleRing.integralUnits_eq_units_integralAdeles (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] : integralUnits R K = (integralAdeles R K).units

The everywhere-integral units are the unit group of the integral finite adeles ∏_v 𝒪_v: a finite idele lies in integralUnits exactly when it and its inverse are integral finite adeles.

theorem IsDedekindDomain.FiniteAdeleRing.exists_finset_mem_sIntegralUnits {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (x : (FiniteAdeleRing R K)ˣ) : ∃ (S : Finset (HeightOneSpectrum R)), x ∈ sIntegralUnits R K ↑S

Every finite idele is S-integral for some finite set S of places.

theorem IsDedekindDomain.FiniteAdeleRing.iSup_sIntegralUnits (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] : ⨆ (S : Finset (HeightOneSpectrum R)), sIntegralUnits R K ↑S = ⊤

The finite idele group is the union of its S-integral subgroups over finite sets S.

@[simp]

theorem IsDedekindDomain.FiniteAdeleRing.unitEmbedding_map_algebraMap_mem_integralUnits {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (u : Rˣ) : (unitEmbedding R K) ((Units.map ↑(algebraMap R K)) u) ∈ integralUnits R K

The principal finite idele of a unit of R is an everywhere-integral unit.

theorem IsDedekindDomain.FiniteAdeleRing.ker_toFractionalIdeal {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] : toFractionalIdeal.ker = integralUnits R K

The finite ideles defining the trivial fractional ideal are exactly the everywhere-integral units.

Principal finite ideles and the class group

@[simp]

theorem IsDedekindDomain.FiniteAdeleRing.toFractionalIdeal_unitEmbedding {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (u : Kˣ) : toFractionalIdeal ((unitEmbedding R K) u) = (toPrincipalIdeal R K) u

The fractional ideal of a principal finite idele is the corresponding principal fractional ideal.

noncomputable def IsDedekindDomain.FiniteAdeleRing.toClassGroup (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] : (FiniteAdeleRing R K)ˣ →* ClassGroup R

The ideal class attached to a finite idele.

@[simp]

theorem IsDedekindDomain.FiniteAdeleRing.toClassGroup_apply {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (x : (FiniteAdeleRing R K)ˣ) : (toClassGroup R K) x = (ClassGroup.mk K) (toFractionalIdeal x)

The ideal class of a finite idele is the class of its fractional ideal.

theorem IsDedekindDomain.FiniteAdeleRing.toClassGroup_surjective {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] : Function.Surjective ⇑(toClassGroup R K)

Every ideal class is the class of a finite idele.

theorem IsDedekindDomain.FiniteAdeleRing.ker_toClassGroup {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] : (toClassGroup R K).ker = integralUnits R K ⊔ (unitEmbedding R K).range

The finite-idele description of the ideal class group: the kernel of the class-group map is generated by the everywhere-integral units and the principal finite ideles.

noncomputable def IsDedekindDomain.FiniteAdeleRing.quotientEquivClassGroup (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] : (FiniteAdeleRing R K)ˣ ⧸ integralUnits R K ⊔ (unitEmbedding R K).range ≃* ClassGroup R

The ideal class group is the quotient of the finite ideles by the everywhere-integral units and the principal finite ideles.

@[simp]

theorem IsDedekindDomain.FiniteAdeleRing.quotientEquivClassGroup_mk {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (x : (FiniteAdeleRing R K)ˣ) : (quotientEquivClassGroup R K) ↑x = (toClassGroup R K) x

quotientEquivClassGroup sends the class of a finite idele to its ideal class.

Sets of primes generating the class group

theorem IsDedekindDomain.FiniteAdeleRing.toClassGroup_mem_closure_iff {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {T : Set (HeightOneSpectrum R)} (x : (FiniteAdeleRing R K)ˣ) : (toClassGroup R K) x ∈ Subgroup.closure (HeightOneSpectrum.classGroupMk '' T) ↔ ∃ (a : Kˣ), ∀ v ∉ T, Valued.v (↑(x * (unitEmbedding R K) a) v) = 1

The ideal class of a finite idele lies in the subgroup generated by the classes of the primes in T exactly when some principal multiple of the idele is a local unit at every place outside T.

theorem IsDedekindDomain.FiniteAdeleRing.exists_valued_mul_unitEmbedding_eq_one {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {T : Set (HeightOneSpectrum R)} (hT : Subgroup.closure (HeightOneSpectrum.classGroupMk '' T) = ⊤) (x : (FiniteAdeleRing R K)ˣ) : ∃ (a : Kˣ), ∀ v ∉ T, Valued.v (↑(x * (unitEmbedding R K) a) v) = 1

Every finite idele is a principal finite idele times a unit outside T, when the classes of the primes in T generate the ideal class group.

theorem IsDedekindDomain.FiniteAdeleRing.forall_valued_unitEmbedding_eq_one_iff {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {T : Set (HeightOneSpectrum R)} (a : Kˣ) : (∀ v ∉ T, Valued.v (↑((unitEmbedding R K) a) v) = 1) ↔ a ∈ T.unit K

A principal finite idele is a local unit at every place outside T exactly when it comes from a T-unit.

Principal S-integral finite ideles

@[simp]

theorem IsDedekindDomain.FiniteAdeleRing.comap_unitEmbedding_sIntegralUnits (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Set (HeightOneSpectrum R)) : Subgroup.comap (unitEmbedding R K) (sIntegralUnits R K S) = S.unit K

The principal S-integral finite ideles are those of the S-units: an element of Kˣ has S-integral principal finite idele exactly when it lies in S.unit K.

Ideal classes of S-integral finite ideles

@[simp]

theorem IsDedekindDomain.FiniteAdeleRing.map_toClassGroup_sIntegralUnits (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Set (HeightOneSpectrum R)) : Subgroup.map (toClassGroup R K) (sIntegralUnits R K S) = Subgroup.closure (HeightOneSpectrum.classGroupMk '' S)

The ideal classes of the S-integral finite ideles form the subgroup of the class group generated by the classes of the primes in S.

theorem IsDedekindDomain.FiniteAdeleRing.sIntegralUnits_sup_range_unitEmbedding_eq_top_iff (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Set (HeightOneSpectrum R)) : sIntegralUnits R K S ⊔ (unitEmbedding R K).range = ⊤ ↔ Subgroup.closure (HeightOneSpectrum.classGroupMk '' S) = ⊤

The S-integral finite ideles and the principal finite ideles generate the finite ideles exactly when the classes of the primes in S generate the ideal class group.