Basic API for ideles

This file records the relation between Mathlib's diagonal embeddings into the idele group and the adele ring. In particular, principal-idele membership can be tested on the underlying adele.

It also defines the finite component NumberField.IdeleGroup.toFiniteIdele of an idele, a unit of the finite adele ring, and the idele NumberField.IdeleGroup.ofFiniteIdele with a given finite component and trivial infinite components, and its counterpart NumberField.IdeleGroup.ofInfiniteIdele with a given infinite component and trivial finite components. The finite component is how ideles are handed to and from the finite-idele theory of fractional ideals: on a principal idele the finite component is the principal finite idele of the same element.

The coordinate maps IsDedekindDomain.HeightOneSpectrum.ideleFiniteCoord and NumberField.InfinitePlace.ideleInfiniteCoord read the local units of an idele. NumberField.IdeleGroup.ext determines an idele by equality of all these coordinates. The constructor TauCeti.GlobalNumberFields.ideleOfUnits assembles local units that are integral units at almost every finite place; TauCeti.GlobalNumberFields.ideleFiniteCoord_ideleOfUnits and TauCeti.GlobalNumberFields.ideleInfiniteCoord_ideleOfUnits recover those units.

The embeddings of the units of the completions, at the infinite and at the finite places, into the idele group and the idele class group are continuous.

Finally, NumberField.IdeleGroup.localUnitsEquiv identifies the idele group, with its units topology, with the product of the unit groups K_wˣ at the infinite places and the restricted product of the unit groups K_vˣ at the finite places with respect to the local integral units 𝒪_vˣ, as topological groups. Its coordinates are the coordinate maps above, and its inverse is TauCeti.GlobalNumberFields.ideleOfUnits. This is the classical description of the idele group as a restricted product over all places, and it shows that the units topology of the adele ring is the restricted-product topology of the local unit groups.

References

• J. W. S. Cassels and A. Fröhlich, eds., Algebraic Number Theory, Chapter II, §16.
• A. Weil, Basic Number Theory, Chapter IV, §3.

theorem NumberField.IdeleGroup.mem_principalSubgroup_iff (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (x : IdeleGroup R K) : x ∈ principalSubgroup R K ↔ ↑x ∈ AdeleRing.principalSubgroup R K

An idele is principal exactly when its underlying adele lies in the diagonal copy of the fraction field.

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

The finite component of an idele, a unit of the finite adele ring (a finite idele).

@[simp]

theorem NumberField.IdeleGroup.coe_toFiniteIdele (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (x : IdeleGroup R K) : ↑((toFiniteIdele R K) x) = (↑x).2

@[simp]

theorem NumberField.IdeleGroup.toFiniteIdele_unitEmbedding (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (x : Kˣ) : (toFiniteIdele R K) ((unitEmbedding R K) x) = (IsDedekindDomain.FiniteAdeleRing.unitEmbedding R K) x

The finite component of a principal idele is the principal finite idele of the same element.

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

The idele with the given finite component and all infinite components equal to 1.

@[simp]

theorem NumberField.IdeleGroup.coe_ofFiniteIdele (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (a : (IsDedekindDomain.FiniteAdeleRing R K)ˣ) : ↑((ofFiniteIdele R K) a) = (1, ↑a)

@[simp]

theorem NumberField.IdeleGroup.toFiniteIdele_ofFiniteIdele (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (a : (IsDedekindDomain.FiniteAdeleRing R K)ˣ) : (toFiniteIdele R K) ((ofFiniteIdele R K) a) = a

The finite component of ofFiniteIdele R K a is a.

noncomputable def NumberField.IdeleGroup.ofInfiniteIdele (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] : (InfiniteAdeleRing K)ˣ →* IdeleGroup R K

The idele with the given infinite component and all finite components equal to 1.

@[simp]

theorem NumberField.IdeleGroup.coe_ofInfiniteIdele (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (a : (InfiniteAdeleRing K)ˣ) : ↑((ofInfiniteIdele R K) a) = (↑a, 1)

@[simp]

theorem NumberField.IdeleGroup.toFiniteIdele_ofInfiniteIdele (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (a : (InfiniteAdeleRing K)ˣ) : (toFiniteIdele R K) ((ofInfiniteIdele R K) a) = 1

The finite component of ofInfiniteIdele R K a is trivial.

@[simp]

theorem NumberField.IdeleGroup.toFiniteIdele_ofCompletion (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (w : InfinitePlace K) (u : w.Completionˣ) : (toFiniteIdele R K) ((ofCompletion R K w) u) = 1

The finite component of an idele concentrated at an infinite place is trivial.

theorem NumberField.IdeleGroup.continuous_ofCompletion (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (w : InfinitePlace K) : Continuous ⇑(ofCompletion R K w)

The embedding of the units of the completion at an infinite place into the idele group is continuous.

theorem NumberField.IdeleGroup.continuous_ofAdicCompletion (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) : Continuous ⇑(ofAdicCompletion R K v)

The embedding of the units of the completion at a finite place into the idele group is continuous.

instance NumberField.IdeleClassGroup.instIsMulCommutative (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] : IsMulCommutative (IdeleClassGroup R K)

The idele class group is commutative. This instance makes commutativity available to instance search without unfolding the quotient abbreviation.

theorem NumberField.IdeleClassGroup.continuous_ofCompletion (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (w : InfinitePlace K) : Continuous ⇑(ofCompletion R K w)

The embedding of the units of the completion at an infinite place into the idele class group is continuous.

theorem NumberField.IdeleClassGroup.continuous_ofAdicCompletion (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) : Continuous ⇑(ofAdicCompletion R K v)

The embedding of the units of the completion at a finite place into the idele class group is continuous.

Coordinates and assembly of an idele

noncomputable def IsDedekindDomain.HeightOneSpectrum.ideleFiniteCoord {K : Type u_1} [Field K] {R : Type u_2} [CommRing R] [IsDedekindDomain R] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : NumberField.IdeleGroup R K →* (adicCompletion K v)ˣ

The coordinate of an idele at a finite place v, a unit of the v-adic completion.

noncomputable def NumberField.InfinitePlace.ideleInfiniteCoord {K : Type u_1} [Field K] {R : Type u_2} [CommRing R] [IsDedekindDomain R] [Algebra R K] [IsFractionRing R K] (w : InfinitePlace K) : IdeleGroup R K →* w.Completionˣ

The coordinate of an idele at an infinite place w, a unit of the completion at w.

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.coe_ideleFiniteCoord {K : Type u_1} [Field K] {R : Type u_2} [CommRing R] [IsDedekindDomain R] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (x : NumberField.IdeleGroup R K) : ↑(v.ideleFiniteCoord x) = (↑x).2 v

@[simp]

theorem NumberField.InfinitePlace.coe_ideleInfiniteCoord {K : Type u_1} [Field K] {R : Type u_2} [CommRing R] [IsDedekindDomain R] [Algebra R K] [IsFractionRing R K] (w : InfinitePlace K) (x : IdeleGroup R K) : ↑(w.ideleInfiniteCoord x) = (↑x).1 w

theorem NumberField.IdeleGroup.ext {K : Type u_1} [Field K] {R : Type u_2} [CommRing R] [IsDedekindDomain R] [Algebra R K] [IsFractionRing R K] {x y : IdeleGroup R K} (hinf : ∀ (w : InfinitePlace K), w.ideleInfiniteCoord x = w.ideleInfiniteCoord y) (hfin : ∀ (v : IsDedekindDomain.HeightOneSpectrum R), v.ideleFiniteCoord x = v.ideleFiniteCoord y) : x = y

Ideles are determined by their coordinates: two ideles with the same coordinate at every infinite and finite place are equal.

theorem NumberField.IdeleGroup.ext_iff {K : Type u_1} [Field K] {R : Type u_2} [CommRing R] [IsDedekindDomain R] [Algebra R K] [IsFractionRing R K] {x y : IdeleGroup R K} : x = y ↔ (∀ (w : InfinitePlace K), w.ideleInfiniteCoord x = w.ideleInfiniteCoord y) ∧ ∀ (v : IsDedekindDomain.HeightOneSpectrum R), v.ideleFiniteCoord x = v.ideleFiniteCoord y

noncomputable def TauCeti.GlobalNumberFields.ideleOfUnits {K : Type u_1} [Field K] {R : Type u_2} [CommRing R] [IsDedekindDomain R] [Algebra R K] [IsFractionRing R K] (zi : (w : NumberField.InfinitePlace K) → w.Completionˣ) (z : (v : IsDedekindDomain.HeightOneSpectrum R) → (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)ˣ) (hz : ∀ᶠ (v : IsDedekindDomain.HeightOneSpectrum R) in Filter.cofinite, z v ∈ (IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v).units) : NumberField.IdeleGroup R K

Assemble an idele from local units that are integral units at almost every finite place.

@[simp]

theorem TauCeti.GlobalNumberFields.ideleFiniteCoord_ideleOfUnits {K : Type u_1} [Field K] {R : Type u_2} [CommRing R] [IsDedekindDomain R] [Algebra R K] [IsFractionRing R K] (zi : (w : NumberField.InfinitePlace K) → w.Completionˣ) (z : (v : IsDedekindDomain.HeightOneSpectrum R) → (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)ˣ) (hz : ∀ᶠ (v : IsDedekindDomain.HeightOneSpectrum R) in Filter.cofinite, z v ∈ (IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v).units) (v : IsDedekindDomain.HeightOneSpectrum R) : v.ideleFiniteCoord (ideleOfUnits zi z hz) = z v

The finite coordinates of the idele assembled from local units are the prescribed units.

@[simp]

theorem TauCeti.GlobalNumberFields.ideleInfiniteCoord_ideleOfUnits {K : Type u_1} [Field K] {R : Type u_2} [CommRing R] [IsDedekindDomain R] [Algebra R K] [IsFractionRing R K] (zi : (w : NumberField.InfinitePlace K) → w.Completionˣ) (z : (v : IsDedekindDomain.HeightOneSpectrum R) → (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)ˣ) (hz : ∀ᶠ (v : IsDedekindDomain.HeightOneSpectrum R) in Filter.cofinite, z v ∈ (IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v).units) (w : NumberField.InfinitePlace K) : w.ideleInfiniteCoord (ideleOfUnits zi z hz) = zi w

The infinite coordinates of the idele assembled from local units are the prescribed units.

The idele group as a restricted product of local unit groups

noncomputable def NumberField.IdeleGroup.localUnitsEquiv (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] : IdeleGroup R K ≃ₜ* ((w : InfinitePlace K) → w.Completionˣ) × RestrictedProduct (fun (v : IsDedekindDomain.HeightOneSpectrum R) => (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)ˣ) (fun (v : IsDedekindDomain.HeightOneSpectrum R) => ↑(Submonoid.ofClass (IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)).units) Filter.cofinite

The idele group is the restricted product of the local unit groups: the idele group, with its units topology, is isomorphic as a topological group to the product of the unit groups K_wˣ of the completions at the infinite places with the restricted product of the unit groups K_vˣ at the finite places with respect to the local integral units 𝒪_vˣ.

@[simp]

theorem NumberField.IdeleGroup.localUnitsEquiv_apply_fst {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (x : IdeleGroup R K) (w : InfinitePlace K) : ((localUnitsEquiv R K) x).1 w = w.ideleInfiniteCoord x

The infinite part of NumberField.IdeleGroup.localUnitsEquiv consists of the coordinates of an idele at the infinite places.

@[simp]

theorem NumberField.IdeleGroup.localUnitsEquiv_apply_snd {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (x : IdeleGroup R K) (v : IsDedekindDomain.HeightOneSpectrum R) : ((localUnitsEquiv R K) x).2 v = v.ideleFiniteCoord x

The finite part of NumberField.IdeleGroup.localUnitsEquiv consists of the coordinates of an idele at the finite places.

theorem NumberField.IdeleGroup.localUnitsEquiv_symm_apply {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (zi : (w : InfinitePlace K) → w.Completionˣ) (z : (v : IsDedekindDomain.HeightOneSpectrum R) → (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)ˣ) (hz : ∀ᶠ (v : IsDedekindDomain.HeightOneSpectrum R) in Filter.cofinite, z v ∈ (IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v).units) : (localUnitsEquiv R K).symm (zi, RestrictedProduct.mk z hz) = TauCeti.GlobalNumberFields.ideleOfUnits zi z hz

The inverse of NumberField.IdeleGroup.localUnitsEquiv assembles an idele from its local units, as TauCeti.GlobalNumberFields.ideleOfUnits does.