Integral ideals of integral finite ideles

A finite idele defines an integral ideal exactly when each of its coordinates is integral. Restricting the fractional-ideal map therefore gives a surjective monoid homomorphism to the nonzero integral ideals. Its fibres are the orbits of the everywhere-integral units. An integral finite idele need not have integral inverse; these ideles form a monoid, whereas integralUnits is a group.

Restricting further to ideles that are local units on a finite set S gives TauCeti.toIntegralIdealsAway, a surjective homomorphism to TauCeti.NumberFieldArithmetic.integralIdealsAway S, with the same fibre criterion.

The construction uses FiniteAdeleRing.toFractionalIdeal and Mathlib's FractionalIdeal.le_one_iff_exists_coeIdeal.

References

• J. Neukirch, Algebraic Number Theory, Chapter VI, §1.

theorem IsDedekindDomain.FiniteAdeleRing.adicOrd_nonneg_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) : 0 ≤ adicOrd x v ↔ ↑x v ∈ HeightOneSpectrum.adicCompletionIntegers K v

A finite-idele order is nonnegative exactly when its coordinate is integral.

@[simp]

theorem IsDedekindDomain.FiniteAdeleRing.toFractionalIdeal_le_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 ↔ ↑x ∈ integralAdeles R K

The fractional ideal of a finite idele is integral exactly when all its coordinates are.

noncomputable def IsDedekindDomain.FiniteAdeleRing.integralFiniteIdeles (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] : Submonoid (FiniteAdeleRing R K)ˣ

Finite ideles whose underlying adeles are integral at every finite place.

@[simp]

theorem IsDedekindDomain.FiniteAdeleRing.mem_integralFiniteIdeles {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 ∈ integralFiniteIdeles R K ↔ ↑x ∈ integralAdeles R K

Membership in the integral finite-idele monoid is integrality of the underlying adele.

noncomputable def IsDedekindDomain.FiniteAdeleRing.toIntegralIdeal {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] : ↥(integralFiniteIdeles R K) →* ↥(nonZeroDivisors (Ideal R))

The nonzero integral ideal defined by an integral finite idele.

@[simp]

theorem IsDedekindDomain.FiniteAdeleRing.coe_toIntegralIdeal {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (x : ↥(integralFiniteIdeles R K)) : ↑↑(toIntegralIdeal x) = ↑(toFractionalIdeal ↑x)

The integral-ideal map agrees with the fractional-ideal map.

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

Every nonzero integral ideal is defined by an integral finite idele.

@[simp]

theorem IsDedekindDomain.FiniteAdeleRing.toIntegralIdeal_eq_one_iff {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (x : ↥(integralFiniteIdeles R K)) : toIntegralIdeal x = 1 ↔ ↑x ∈ integralUnits R K

An integral finite idele defines the unit ideal exactly when it is an everywhere-integral unit.

theorem IsDedekindDomain.FiniteAdeleRing.mker_toIntegralIdeal {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] : MonoidHom.mker toIntegralIdeal = Submonoid.comap (integralFiniteIdeles R K).subtype (integralUnits R K).toSubmonoid

The kernel of the integral-ideal map is the preimage of the everywhere-integral units.

@[simp]

theorem IsDedekindDomain.FiniteAdeleRing.toIntegralIdeal_eq_iff {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (x y : ↥(integralFiniteIdeles R K)) : toIntegralIdeal x = toIntegralIdeal y ↔ ↑x / ↑y ∈ integralUnits R K

Two integral finite ideles define the same ideal exactly when their ratio is an everywhere-integral unit.

noncomputable def TauCeti.integralFiniteIdelesAway {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (S : Finset (IsDedekindDomain.HeightOneSpectrum R)) : Submonoid ↥(IsDedekindDomain.FiniteAdeleRing.integralFiniteIdeles R K)

Integral finite ideles that are local units at every place in S.

@[simp]

theorem TauCeti.mem_integralFiniteIdelesAway_iff {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (S : Finset (IsDedekindDomain.HeightOneSpectrum R)) (x : ↥(IsDedekindDomain.FiniteAdeleRing.integralFiniteIdeles R K)) : x ∈ integralFiniteIdelesAway S ↔ ∀ v ∈ S, IsDedekindDomain.FiniteAdeleRing.adicOrd (↑x) v = 0

The excluded places are precisely those at which the orders must vanish.

noncomputable def TauCeti.toIntegralIdealsAway {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (S : Finset (IsDedekindDomain.HeightOneSpectrum R)) : ↥(integralFiniteIdelesAway S) →* ↥(NumberFieldArithmetic.integralIdealsAway S)

The integral ideal away from S defined by an integral finite idele locally a unit on S. This map takes values in the existing integral prime-to monoid.

@[simp]

theorem TauCeti.coe_toIntegralIdealsAway {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (S : Finset (IsDedekindDomain.HeightOneSpectrum R)) (x : ↥(integralFiniteIdelesAway S)) : ↑((toIntegralIdealsAway S) x) = ↑(IsDedekindDomain.FiniteAdeleRing.toIntegralIdeal ↑x)

The prime-to integral-ideal map is the restriction of the integral-ideal map.

theorem TauCeti.toIntegralIdealsAway_surjective {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (S : Finset (IsDedekindDomain.HeightOneSpectrum R)) : Function.Surjective ⇑(toIntegralIdealsAway S)

Every integral ideal prime to S comes from an integral finite idele locally a unit on S.

@[simp]

theorem TauCeti.toIntegralIdealsAway_eq_one_iff {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (S : Finset (IsDedekindDomain.HeightOneSpectrum R)) (x : ↥(integralFiniteIdelesAway S)) : (toIntegralIdealsAway S) x = 1 ↔ ↑↑x ∈ IsDedekindDomain.FiniteAdeleRing.integralUnits R K

The integral prime-to map has unit ideal exactly on the everywhere-integral units.

theorem TauCeti.mker_toIntegralIdealsAway {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (S : Finset (IsDedekindDomain.HeightOneSpectrum R)) : MonoidHom.mker (toIntegralIdealsAway S) = Submonoid.comap ((IsDedekindDomain.FiniteAdeleRing.integralFiniteIdeles R K).subtype.comp (integralFiniteIdelesAway S).subtype) (IsDedekindDomain.FiniteAdeleRing.integralUnits R K).toSubmonoid

The kernel of the integral prime-to map is the preimage of the everywhere-integral units.

@[simp]

theorem TauCeti.toIntegralIdealsAway_eq_iff {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (S : Finset (IsDedekindDomain.HeightOneSpectrum R)) (x y : ↥(integralFiniteIdelesAway S)) : (toIntegralIdealsAway S) x = (toIntegralIdealsAway S) y ↔ ↑↑x / ↑↑y ∈ IsDedekindDomain.FiniteAdeleRing.integralUnits R K

Two integral finite ideles locally units on S define the same prime-to ideal exactly when their ratio is an everywhere-integral unit.