Fractional ideals of ideles

This file relates the fractional ideal of an idele's finite component to its valuations at finite places. It also gives a norm-one idele representative of every ideal class.

Let T be a set of finite places whose classes generate the ideal class group, for instance a finite set when the class group is finite (ClassGroup.exists_finite_closure_classGroupMk_image_eq_top). Write I_{K,T} for the ideles that are local units at every finite place outside T, and U_T for the T-units T.unit K. Then every idele is a principal idele times an element of I_{K,T}, and the principal ideles in I_{K,T} are exactly those of the T-units:

I_K = Kˣ · I_{K,T}, Kˣ ∩ I_{K,T} = U_T,

so the idele class group is C_K = I_{K,T} / U_T. This is the form in which the cohomology of the idele classes of a Galois extension is computed from that of the T-ideles and the T-units, for T stable under the Galois group.

Main results

• NumberField.IdeleGroup.exists_valued_ideleFiniteCoord_mul_unitEmbedding_eq_one: I_K = Kˣ · I_{K,T}.
• NumberField.IdeleGroup.mem_principalSubgroup_iff_exists_mem_unit: Kˣ ∩ I_{K,T} = U_T.
• NumberField.IdeleClassGroup.exists_valued_ideleFiniteCoord_eq_one_and_mk_eq: every idele class is the class of an element of I_{K,T}.

References

• J. S. Milne, Class Field Theory, Chapter VII, §4.
• J. Neukirch, Algebraic Number Theory, Chapter VI, §1.

theorem TauCeti.GlobalNumberFields.toFractionalIdeal_toFiniteIdele_eq_one_iff {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {x : NumberField.IdeleGroup R K} : IsDedekindDomain.FiniteAdeleRing.toFractionalIdeal ((NumberField.IdeleGroup.toFiniteIdele R K) x) = 1 ↔ ∀ (v : IsDedekindDomain.HeightOneSpectrum R), Valued.v ↑(v.ideleFiniteCoord x) = 1

The fractional ideal of an idele's finite component is trivial exactly when the idele is a unit at every finite place.

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.toFractionalIdeal_toFiniteIdele_ofAdicCompletion {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (u : (adicCompletion K v)ˣ) : FiniteAdeleRing.toFractionalIdeal ((NumberField.IdeleGroup.toFiniteIdele R K) ((NumberField.IdeleGroup.ofAdicCompletion R K v) u)) = v.unitOfPrime K ^ (-(Valued.v ↑u).log)

The fractional ideal of an idele concentrated at one finite place is the corresponding prime power, with exponent the local order of its nonzero coordinate.

theorem IsDedekindDomain.HeightOneSpectrum.toFractionalIdeal_toFiniteIdele_ofAdicCompletion_of_eq_exp_neg_one {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) {u : (adicCompletion K v)ˣ} (hu : Valued.v ↑u = WithZero.exp (-1)) : FiniteAdeleRing.toFractionalIdeal ((NumberField.IdeleGroup.toFiniteIdele R K) ((NumberField.IdeleGroup.ofAdicCompletion R K v) u)) = v.unitOfPrime K

The fractional ideal of an idele concentrated at one finite place, with a coordinate of valuation exp (-1) there (a uniformizer), is the prime of that place.

theorem ClassGroup.exists_ideleNorm_eq_one_and_toClassGroup_eq {K : Type u_1} [Field K] [NumberField K] (c : ClassGroup (NumberField.RingOfIntegers K)) : ∃ (b : NumberField.IdeleGroup (NumberField.RingOfIntegers K) K), TauCeti.GlobalNumberFields.ideleNorm b = 1 ∧ (IsDedekindDomain.FiniteAdeleRing.toClassGroup (NumberField.RingOfIntegers K) K) ((NumberField.IdeleGroup.toFiniteIdele (NumberField.RingOfIntegers K) K) b) = c

Every ideal class is the class of the finite part of an idele of norm one.

Ideles that are units outside a set of places

theorem NumberField.IdeleGroup.exists_valued_ideleFiniteCoord_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 (IsDedekindDomain.HeightOneSpectrum R)} (hT : Subgroup.closure (IsDedekindDomain.HeightOneSpectrum.classGroupMk '' T) = ⊤) (x : IdeleGroup R K) : ∃ (a : Kˣ), ∀ v ∉ T, Valued.v ↑(v.ideleFiniteCoord (x * (unitEmbedding R K) a)) = 1

Every idele is a principal idele times an idele that is a unit at the finite places outside T, when the classes of the primes in T generate the ideal class group: I_K = Kˣ · I_{K,T}.

theorem NumberField.IdeleGroup.forall_valued_ideleFiniteCoord_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 (IsDedekindDomain.HeightOneSpectrum R)} (a : Kˣ) : (∀ v ∉ T, Valued.v ↑(v.ideleFiniteCoord ((unitEmbedding R K) a)) = 1) ↔ a ∈ T.unit K

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

theorem NumberField.IdeleGroup.mem_principalSubgroup_iff_exists_mem_unit {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)} {x : IdeleGroup R K} (hx : ∀ v ∉ T, Valued.v ↑(v.ideleFiniteCoord x) = 1) : x ∈ principalSubgroup R K ↔ ∃ a ∈ T.unit K, (unitEmbedding R K) a = x

The principal ideles that are units outside T are those of the T-units: Kˣ ∩ I_{K,T} = U_T.

theorem NumberField.IdeleClassGroup.exists_valued_ideleFiniteCoord_eq_one_and_mk_eq {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)} (hT : Subgroup.closure (IsDedekindDomain.HeightOneSpectrum.classGroupMk '' T) = ⊤) (c : IdeleClassGroup R K) : ∃ (x : IdeleGroup R K), (∀ v ∉ T, Valued.v ↑(v.ideleFiniteCoord x) = 1) ∧ ↑x = c

Every idele class is represented by an idele that is a unit at the finite places outside T, when the classes of the primes in T generate the ideal class group. With NumberField.IdeleGroup.mem_principalSubgroup_iff_exists_mem_unit, this identifies C_K with I_{K,T} / U_T.