Moduli of a number field and multiplicative congruence

A modulus of a number field K is a pair consisting of a nonzero integral ideal of 𝓞 K (the finite part) and a finite set of real infinite places (the infinite part). Moduli are the data against which the congruence conditions defining ray classes are imposed: an element x of Kˣ is congruent to one modulo 𝔪 when the finite part divides x - 1 locally at each of its prime divisors, and x is positive at each real place selected by the infinite part.

This file builds that vocabulary:

• the carrier Modulus K, its divisibility relation, its finite support and exponent function, the trivial modulus and the modulus with unit finite part and every real place;
• the predicate IsCongrOne and the subgroup congruenceSubgroup of Kˣ it cuts out, together with the larger subgroup primeToSubgroup of elements that are units at the primes dividing the finite part, and the subgroup unitsCongruenceSubgroup of (𝓞 K)ˣ obtained by restriction;
• the group idealsPrimeTo 𝔪 of invertible fractional ideals and the monoid integralIdealsPrimeTo 𝔪 of nonzero integral ideals that are prime to the finite part.

The last two are abbreviations for TauCeti.NumberFieldArithmetic.idealsAway 𝔪.support and TauCeti.NumberFieldArithmetic.integralIdealsAway 𝔪.support: there is exactly one group of prime-to fractional ideals and one monoid of prime-to integral ideals, and both are the ones built away from a finite set of primes.

Main definitions

• TauCeti.GlobalNumberFields.Modulus: the carrier, with Modulus.support, Modulus.exponent, Modulus.one and TauCeti.GlobalNumberFields.narrowModulus.
• TauCeti.GlobalNumberFields.IsCongrOne: multiplicative congruence to one modulo a modulus.
• TauCeti.GlobalNumberFields.congruenceSubgroup, TauCeti.GlobalNumberFields.primeToSubgroup, TauCeti.GlobalNumberFields.unitsCongruenceSubgroup: the subgroups of Kˣ and (𝓞 K)ˣ these conditions define.
• TauCeti.GlobalNumberFields.unitsToPrimeToSubgroup: the inclusion of (𝓞 K)ˣ into primeToSubgroup 𝔪.
• TauCeti.GlobalNumberFields.idealsPrimeTo, TauCeti.GlobalNumberFields.integralIdealsPrimeTo: ideals prime to the finite part, with the inclusion TauCeti.GlobalNumberFields.integralIdealsPrimeToInclusion along divisibility.

Main results

• TauCeti.GlobalNumberFields.Modulus.wellFounded_dvd_and_ne: strict divisibility of moduli is well founded.
• TauCeti.GlobalNumberFields.Modulus.mem_support_iff: membership in the support is divisibility of the finite part. Modulus.support_one and Modulus.support_mono are consequences.
• TauCeti.GlobalNumberFields.Modulus.pow_exponent_dvd_finitePart and TauCeti.GlobalNumberFields.Modulus.mem_finitePart_of_forall_mem_pow_exponent: the prime power prescribed by the exponent divides the finite part, and membership in the finite part is detected by those prime powers.
• TauCeti.GlobalNumberFields.Modulus.valued_eq_one_of_valued_sub_one_le: an element of the v-adic completion congruent to one at a divisor of the finite part is a unit there.
• TauCeti.GlobalNumberFields.congruenceSubgroup_le_primeToSubgroup: an element congruent to one is a unit at every prime dividing the finite part. This is what makes the ray a subgroup of the prime-to ideals.
• TauCeti.GlobalNumberFields.IsCongrOne.mono and TauCeti.GlobalNumberFields.congruenceSubgroup_antitone: congruence to one is antitone in the modulus, which is what makes the transition maps between ray class groups run from a larger modulus to a smaller one.
• TauCeti.GlobalNumberFields.isCongrOne_narrowModulus_iff: congruence to one modulo the modulus with unit finite part and every real place is total positivity.
• TauCeti.GlobalNumberFields.unitsCongruenceSubgroup_narrowModulus: the units congruent to one modulo the narrow modulus are the totally positive integer units.
• TauCeti.GlobalNumberFields.Modulus.isCoprimeTo_of_dvd_span_singleton: a divisor of a principal ideal whose generator is a unit at the finite part is prime to the modulus.
• TauCeti.GlobalNumberFields.Modulus.isCoprimeTo_iff_sup_eq_top: being prime to the support is comaximality with the finite part.

References

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

structure TauCeti.GlobalNumberFields.Modulus (K : Type u_1) [Field K] [NumberField K] : Type u_1

A modulus of a number field K: a nonzero integral ideal of 𝓞 K together with a finite set of real infinite places. Complex places never divide a modulus, which is why the infinite part is a Finset of the subtype {w : InfinitePlace K // w.IsReal} rather than of all infinite places.

• finitePart : Ideal (NumberField.RingOfIntegers K)

  The finite part of the modulus: a nonzero integral ideal of 𝓞 K.

• finitePart_ne_bot : self.finitePart ≠ ⊥

  The finite part of a modulus is nonzero.

• infinitePart : Finset { w : NumberField.InfinitePlace K // w.IsReal }

  The infinite part of the modulus: a finite set of real places of K.

theorem TauCeti.GlobalNumberFields.Modulus.ext {K : Type u_1} [Field K] [NumberField K] {m n : Modulus K} (hfinite : m.finitePart = n.finitePart) (hinfinite : m.infinitePart = n.infinitePart) : m = n

Two moduli are equal when their finite and infinite parts are equal.

theorem TauCeti.GlobalNumberFields.Modulus.ext_iff {K : Type u_1} [Field K] [NumberField K] {m n : Modulus K} : m = n ↔ m.finitePart = n.finitePart ∧ m.infinitePart = n.infinitePart

theorem TauCeti.GlobalNumberFields.Modulus.finitePart_ne_zero {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : 𝔪.finitePart ≠ 0

@[instance_reducible]

instance TauCeti.GlobalNumberFields.Modulus.instDvd {K : Type u_1} [Field K] [NumberField K] : Dvd (Modulus K)

Divisibility of moduli: 𝔪 ∣ 𝔫 when the finite part of 𝔪 divides that of 𝔫 and the infinite part of 𝔪 is contained in that of 𝔫, so that the congruence conditions imposed by 𝔫 are the stronger ones.

Equations

• TauCeti.GlobalNumberFields.Modulus.instDvd = { dvd := fun (𝔪 𝔫 : TauCeti.GlobalNumberFields.Modulus K) => 𝔪.finitePart ∣ 𝔫.finitePart ∧ 𝔪.infinitePart ⊆ 𝔫.infinitePart }

@[simp]

theorem TauCeti.GlobalNumberFields.Modulus.dvd_iff {K : Type u_1} [Field K] [NumberField K] {𝔪 𝔫 : Modulus K} : 𝔪 ∣ 𝔫 ↔ 𝔪.finitePart ∣ 𝔫.finitePart ∧ 𝔪.infinitePart ⊆ 𝔫.infinitePart

Divisibility of moduli is componentwise. This is the introduction and elimination rule for 𝔪 ∣ 𝔫, so no proof of a divisibility statement, here or downstream, needs the Dvd (Modulus K) instance body.

theorem TauCeti.GlobalNumberFields.Modulus.dvd_refl {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : 𝔪 ∣ 𝔪

theorem TauCeti.GlobalNumberFields.Modulus.dvd_trans {K : Type u_1} [Field K] [NumberField K] {𝔪 𝔫 𝔭 : Modulus K} (h₁ : 𝔪 ∣ 𝔫) (h₂ : 𝔫 ∣ 𝔭) : 𝔪 ∣ 𝔭

theorem TauCeti.GlobalNumberFields.Modulus.dvd_antisymm {K : Type u_1} [Field K] [NumberField K] {𝔪 𝔫 : Modulus K} (hm : 𝔪 ∣ 𝔫) (hn : 𝔫 ∣ 𝔪) : 𝔪 = 𝔫

Divisibility of moduli is antisymmetric.

theorem TauCeti.GlobalNumberFields.Modulus.wellFounded_dvd_and_ne {K : Type u_1} [Field K] [NumberField K] : WellFounded fun (𝔪 𝔫 : Modulus K) => 𝔪 ∣ 𝔫 ∧ 𝔪 ≠ 𝔫

Strict divisibility of moduli is well founded: there is no infinite sequence of moduli in which each term is a proper divisor of the previous one. Along a proper divisor, the absolute norm of the finite part plus the number of real places strictly decreases. In particular every nonempty set of moduli has a member none of whose proper divisors lies in the set.

noncomputable def TauCeti.GlobalNumberFields.Modulus.support {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))

The support of a modulus: the finite set of height-one primes dividing its finite part.

Equations

• 𝔪.support = ⋯.toFinset

@[simp]

theorem TauCeti.GlobalNumberFields.Modulus.mem_support_iff {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : v ∈ 𝔪.support ↔ v.asIdeal ∣ 𝔪.finitePart

Membership in the support is divisibility of the finite part. This is the characterizing theorem of Modulus.support; Modulus.support_one and Modulus.support_mono are derived from it.

theorem TauCeti.GlobalNumberFields.Modulus.support_mono {K : Type u_1} [Field K] [NumberField K] {𝔪 𝔫 : Modulus K} (h : 𝔪 ∣ 𝔫) : 𝔪.support ⊆ 𝔫.support

The support grows with the modulus.

noncomputable def TauCeti.GlobalNumberFields.Modulus.exponent {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : ℕ

The exponent of a finite place in a modulus: the multiplicity of v in the factorization of the finite part.

Equations

• 𝔪.exponent v = (Associates.mk v.asIdeal).count (Associates.mk 𝔪.finitePart).factors

theorem TauCeti.GlobalNumberFields.Modulus.exponent_def {K : Type u_1} [Field K] [NumberField K] (m : Modulus K) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : m.exponent v = (Associates.mk v.asIdeal).count (Associates.mk m.finitePart).factors

The exponent of a finite place is its multiplicity in the factorization of the finite part.

theorem TauCeti.GlobalNumberFields.Modulus.mem_support_iff_exponent_ne_zero {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : v ∈ 𝔪.support ↔ 𝔪.exponent v ≠ 0

A prime lies in the support of a modulus exactly when it occurs in the finite part with a positive exponent.

theorem TauCeti.GlobalNumberFields.Modulus.exponent_pos_of_mem_support {K : Type u_1} [Field K] [NumberField K] {𝔪 : Modulus K} {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} (hv : v ∈ 𝔪.support) : 0 < 𝔪.exponent v

theorem TauCeti.GlobalNumberFields.Modulus.pow_dvd_finitePart_iff_le_exponent {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) {n : ℕ} : v.asIdeal ^ n ∣ 𝔪.finitePart ↔ n ≤ 𝔪.exponent v

The exponent is the exact multiplicity of the prime in the finite part: v ^ n divides the finite part exactly when n is at most the exponent of v.

theorem TauCeti.GlobalNumberFields.Modulus.pow_exponent_dvd_finitePart {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : v.asIdeal ^ 𝔪.exponent v ∣ 𝔪.finitePart

The prescribed prime power divides the finite part. This is what turns membership in the finite part into the valuation bound recorded by IsCongrOne.

theorem TauCeti.GlobalNumberFields.Modulus.mem_finitePart_of_forall_mem_pow_exponent {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) {y : NumberField.RingOfIntegers K} (h : ∀ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), v.asIdeal ∣ 𝔪.finitePart → y ∈ v.asIdeal ^ 𝔪.exponent v) : y ∈ 𝔪.finitePart

Membership in the finite part is a local condition. An algebraic integer lying in the prime power prescribed by the exponent at every prime dividing the finite part lies in the finite part itself. This is the converse direction to Modulus.pow_exponent_dvd_finitePart.

theorem TauCeti.GlobalNumberFields.Modulus.exponent_mono {K : Type u_1} [Field K] [NumberField K] {𝔪 𝔫 : Modulus K} (h : 𝔪 ∣ 𝔫) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : 𝔪.exponent v ≤ 𝔫.exponent v

Exponents grow with the modulus.

theorem TauCeti.GlobalNumberFields.Modulus.valued_eq_one_of_valued_sub_one_le {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} (hv : v.asIdeal ∣ 𝔪.finitePart) {y : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v} (hy : Valued.v (y - 1) ≤ WithZero.exp (-↑(𝔪.exponent v))) : Valued.v y = 1

A congruent coordinate is a local unit. At a prime dividing the finite part of 𝔪 the prescribed exponent is positive, so an element of the v-adic completion congruent to one to that level has valuation one.

def TauCeti.GlobalNumberFields.Modulus.one (K : Type u_2) [Field K] [NumberField K] : Modulus K

The trivial modulus: unit finite part and no real places. It imposes no condition, so its ray class group is the ordinary class group.

Equations

• TauCeti.GlobalNumberFields.Modulus.one K = { finitePart := ⊤, finitePart_ne_bot := ⋯, infinitePart := ∅ }

@[simp]

theorem TauCeti.GlobalNumberFields.Modulus.one_finitePart {K : Type u_1} [Field K] [NumberField K] : (one K).finitePart = ⊤

@[simp]

theorem TauCeti.GlobalNumberFields.Modulus.one_infinitePart {K : Type u_1} [Field K] [NumberField K] : (one K).infinitePart = ∅

@[simp]

theorem TauCeti.GlobalNumberFields.Modulus.support_one {K : Type u_1} [Field K] [NumberField K] : (one K).support = ∅

The trivial modulus has empty support: no height-one prime divides the unit ideal.

theorem TauCeti.GlobalNumberFields.Modulus.one_dvd {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : one K ∣ 𝔪

theorem TauCeti.GlobalNumberFields.Modulus.eq_one_of_dvd_one {K : Type u_1} [Field K] [NumberField K] {𝔪 : Modulus K} (h : 𝔪 ∣ one K) : 𝔪 = one K

The trivial modulus is the only divisor of itself.

noncomputable def TauCeti.GlobalNumberFields.narrowModulus (K : Type u_2) [Field K] [NumberField K] : Modulus K

The modulus with unit finite part and every real place. Its ray class group is the narrow class group.

Equations

• TauCeti.GlobalNumberFields.narrowModulus K = { finitePart := (TauCeti.GlobalNumberFields.Modulus.one K).finitePart, finitePart_ne_bot := ⋯, infinitePart := ⋯.toFinset }

@[simp]

theorem TauCeti.GlobalNumberFields.narrowModulus_finitePart {K : Type u_1} [Field K] [NumberField K] : (narrowModulus K).finitePart = ⊤

@[simp]

theorem TauCeti.GlobalNumberFields.mem_narrowModulus_infinitePart {K : Type u_1} [Field K] [NumberField K] (w : { w : NumberField.InfinitePlace K // w.IsReal }) : w ∈ (narrowModulus K).infinitePart

@[simp]

theorem TauCeti.GlobalNumberFields.narrowModulus_support {K : Type u_1} [Field K] [NumberField K] : (narrowModulus K).support = ∅

The narrow modulus has the same finite part as the trivial one, hence the same support.

Multiplicative congruence

def TauCeti.GlobalNumberFields.IsCongrOne {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) (x : Kˣ) : Prop

Multiplicative congruence to one modulo a modulus. An element x of Kˣ satisfies IsCongrOne 𝔪 x when, at every prime v dividing the finite part of 𝔪, the element x - 1 is divisible by v ^ (𝔪.exponent v) locally — equivalently v.valuation K (x - 1) is at most exp (-𝔪.exponent v) — and x is positive at every real place selected by the infinite part.

This is a condition on Kˣ, not on K. Zero is excluded because it generates no invertible principal fractional ideal, so it has no ray class to contribute, while it would satisfy the empty conditions imposed by the trivial modulus. The condition is also not unqualified membership in 1 + 𝔪.finitePart, since x need not be an algebraic integer.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.GlobalNumberFields.isCongrOne_iff {K : Type u_1} [Field K] [NumberField K] {𝔪 : Modulus K} {x : Kˣ} : IsCongrOne 𝔪 x ↔ (∀ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), v.asIdeal ∣ 𝔪.finitePart → (IsDedekindDomain.HeightOneSpectrum.valuation K v) (↑x - 1) ≤ WithZero.exp (-↑(𝔪.exponent v))) ∧ ∀ w ∈ 𝔪.infinitePart, 0 < (NumberField.InfinitePlace.embedding_of_isReal ⋯) ↑x

theorem TauCeti.GlobalNumberFields.IsCongrOne.valuation_sub_one_le {K : Type u_1} [Field K] [NumberField K] {𝔪 : Modulus K} {x : Kˣ} (hx : IsCongrOne 𝔪 x) {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} (hv : v.asIdeal ∣ 𝔪.finitePart) : (IsDedekindDomain.HeightOneSpectrum.valuation K v) (↑x - 1) ≤ WithZero.exp (-↑(𝔪.exponent v))

theorem TauCeti.GlobalNumberFields.IsCongrOne.pos {K : Type u_1} [Field K] [NumberField K] {𝔪 : Modulus K} {x : Kˣ} (hx : IsCongrOne 𝔪 x) {w : { w : NumberField.InfinitePlace K // w.IsReal }} (hw : w ∈ 𝔪.infinitePart) : 0 < (NumberField.InfinitePlace.embedding_of_isReal ⋯) ↑x

theorem TauCeti.GlobalNumberFields.IsCongrOne.valuation_sub_one_lt_one {K : Type u_1} [Field K] [NumberField K] {𝔪 : Modulus K} {x : Kˣ} (hx : IsCongrOne 𝔪 x) {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} (hv : v.asIdeal ∣ 𝔪.finitePart) : (IsDedekindDomain.HeightOneSpectrum.valuation K v) (↑x - 1) < 1

An element congruent to one modulo 𝔪 has v-adic valuation strictly less than one at x - 1, for every prime v dividing the finite part: the exponent there is positive.

theorem TauCeti.GlobalNumberFields.IsCongrOne.valuation_eq_one {K : Type u_1} [Field K] [NumberField K] {𝔪 : Modulus K} {x : Kˣ} (hx : IsCongrOne 𝔪 x) {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} (hv : v.asIdeal ∣ 𝔪.finitePart) : (IsDedekindDomain.HeightOneSpectrum.valuation K v) ↑x = 1

An element congruent to one is a unit at the primes dividing the finite part.

theorem TauCeti.GlobalNumberFields.IsCongrOne.mono {K : Type u_1} [Field K] [NumberField K] {𝔪 : Modulus K} {x : Kˣ} {𝔫 : Modulus K} (h : 𝔪 ∣ 𝔫) (hx : IsCongrOne 𝔫 x) : IsCongrOne 𝔪 x

Congruence is antitone in the modulus. An element congruent to one modulo the larger modulus 𝔫 is congruent to one modulo every divisor 𝔪 of 𝔫: the exponents can only have shrunk and fewer real places are constrained.

def TauCeti.GlobalNumberFields.congruenceSubgroup {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : Subgroup Kˣ

The subgroup of Kˣ of elements congruent to one modulo 𝔪. The ray of principal ideals is generated by its image in the fractional ideals.

Equations

• TauCeti.GlobalNumberFields.congruenceSubgroup 𝔪 = { carrier := {x : Kˣ | TauCeti.GlobalNumberFields.IsCongrOne 𝔪 x}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

@[simp]

theorem TauCeti.GlobalNumberFields.mem_congruenceSubgroup {K : Type u_1} [Field K] [NumberField K] {𝔪 : Modulus K} {x : Kˣ} : x ∈ congruenceSubgroup 𝔪 ↔ IsCongrOne 𝔪 x

theorem TauCeti.GlobalNumberFields.congruenceSubgroup_antitone {K : Type u_1} [Field K] [NumberField K] {𝔪 𝔫 : Modulus K} (h : 𝔪 ∣ 𝔫) : congruenceSubgroup 𝔫 ≤ congruenceSubgroup 𝔪

The congruence subgroups decrease as the modulus grows.

def TauCeti.GlobalNumberFields.primeToSubgroup {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : Subgroup Kˣ

The subgroup of Kˣ of elements that are units at every prime dividing the finite part of the modulus. This is the domain of reduction to the residue units.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.GlobalNumberFields.mem_primeToSubgroup {K : Type u_1} [Field K] [NumberField K] {𝔪 : Modulus K} {x : Kˣ} : x ∈ primeToSubgroup 𝔪 ↔ ∀ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), v.asIdeal ∣ 𝔪.finitePart → (IsDedekindDomain.HeightOneSpectrum.valuation K v) ↑x = 1

theorem TauCeti.GlobalNumberFields.primeToSubgroup_le_of_dvd {K : Type u_1} [Field K] [NumberField K] {𝔪 𝔫 : Modulus K} (h : 𝔪.finitePart ∣ 𝔫.finitePart) : primeToSubgroup 𝔫 ≤ primeToSubgroup 𝔪

A larger finite part has a smaller prime-to subgroup. This is the carrier map used when changing the finite part in a reduction statement.

theorem TauCeti.GlobalNumberFields.congruenceSubgroup_le_primeToSubgroup {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : congruenceSubgroup 𝔪 ≤ primeToSubgroup 𝔪

Congruence to one implies being a unit at the finite part. This inclusion is what makes the principal ideal of an element congruent to one prime to the modulus.

def TauCeti.GlobalNumberFields.unitsCongruenceSubgroup {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : Subgroup (NumberField.RingOfIntegers K)ˣ

The units of 𝓞 K congruent to one modulo 𝔪. Its index in (𝓞 K)ˣ is the unit correction in the ray class number formula.

Equations

• TauCeti.GlobalNumberFields.unitsCongruenceSubgroup 𝔪 = Subgroup.comap (Units.map ↑(algebraMap (NumberField.RingOfIntegers K) K)) (TauCeti.GlobalNumberFields.congruenceSubgroup 𝔪)

@[simp]

theorem TauCeti.GlobalNumberFields.mem_unitsCongruenceSubgroup {K : Type u_1} [Field K] [NumberField K] {𝔪 : Modulus K} {u : (NumberField.RingOfIntegers K)ˣ} : u ∈ unitsCongruenceSubgroup 𝔪 ↔ IsCongrOne 𝔪 ((Units.map ↑(algebraMap (NumberField.RingOfIntegers K) K)) u)

theorem TauCeti.GlobalNumberFields.unitsMap_mem_primeToSubgroup {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) (u : (NumberField.RingOfIntegers K)ˣ) : (Units.map ↑(algebraMap (NumberField.RingOfIntegers K) K)) u ∈ primeToSubgroup 𝔪

The image of an integer unit is a unit at every finite place, hence lies in primeToSubgroup 𝔪.

noncomputable def TauCeti.GlobalNumberFields.unitsToPrimeToSubgroup {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : (NumberField.RingOfIntegers K)ˣ →* ↥(primeToSubgroup 𝔪)

The inclusion of the integer units into the elements that are units at the finite part. Its composition with the residue-and-sign presentation is the unit obstruction in the ray class exact sequence.

Equations

• TauCeti.GlobalNumberFields.unitsToPrimeToSubgroup 𝔪 = (Units.map ↑(algebraMap (NumberField.RingOfIntegers K) K)).codRestrict (TauCeti.GlobalNumberFields.primeToSubgroup 𝔪) ⋯

@[simp]

theorem TauCeti.GlobalNumberFields.coe_unitsToPrimeToSubgroup {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) (u : (NumberField.RingOfIntegers K)ˣ) : ↑((unitsToPrimeToSubgroup 𝔪) u) = (Units.map ↑(algebraMap (NumberField.RingOfIntegers K) K)) u

@[simp]

theorem TauCeti.GlobalNumberFields.isCongrOne_one {K : Type u_1} [Field K] [NumberField K] (x : Kˣ) : IsCongrOne (Modulus.one K) x

The trivial modulus imposes no condition. Its finite part is the unit ideal, which no prime divides, and its infinite part is empty.

@[simp]

theorem TauCeti.GlobalNumberFields.congruenceSubgroup_one {K : Type u_1} [Field K] [NumberField K] : congruenceSubgroup (Modulus.one K) = ⊤

@[simp]

theorem TauCeti.GlobalNumberFields.unitsCongruenceSubgroup_one {K : Type u_1} [Field K] [NumberField K] : unitsCongruenceSubgroup (Modulus.one K) = ⊤

Every integer unit is congruent to one for the trivial modulus.

@[simp]

theorem TauCeti.GlobalNumberFields.isCongrOne_narrowModulus_iff {K : Type u_1} [Field K] [NumberField K] {x : Kˣ} : IsCongrOne (narrowModulus K) x ↔ NumberField.IsTotallyPositive ↑x

Congruence to one modulo the narrow modulus is total positivity. The finite part of narrowModulus K is the unit ideal, so only the sign conditions survive, and they are imposed at every real place.

@[simp]

theorem TauCeti.GlobalNumberFields.unitsCongruenceSubgroup_narrowModulus {K : Type u_1} [Field K] [NumberField K] : unitsCongruenceSubgroup (narrowModulus K) = NumberField.totallyPositiveIntegerUnits

The integer units congruent to one modulo the narrow modulus are exactly the totally positive integer units.

Ideals prime to a modulus

@[reducible, inline]

noncomputable abbrev TauCeti.GlobalNumberFields.idealsPrimeTo {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : Subgroup (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ

The group of fractional ideals prime to a modulus: the invertible fractional ideals whose multiplicity vanishes at every prime dividing the finite part. There is one such group, the one built away from a finite set of primes.

Equations

• TauCeti.GlobalNumberFields.idealsPrimeTo 𝔪 = TauCeti.NumberFieldArithmetic.idealsAway 𝔪.support

def TauCeti.GlobalNumberFields.Modulus.IsCoprimeTo {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) (I : Ideal (NumberField.RingOfIntegers K)) : Prop

Coprimality of a nonzero integral ideal to a modulus: it is prime to the support, that is, to the finite part. This is the membership predicate of integralIdealsPrimeTo.

Equations

• 𝔪.IsCoprimeTo I = I.IsPrimeTo ↑𝔪.support

theorem TauCeti.GlobalNumberFields.Modulus.isCoprimeTo_iff {K : Type u_1} [Field K] [NumberField K] {𝔪 : Modulus K} {I : Ideal (NumberField.RingOfIntegers K)} : 𝔪.IsCoprimeTo I ↔ I ≠ ⊥ ∧ ∀ v ∈ 𝔪.support, ¬v.asIdeal ∣ I

theorem TauCeti.GlobalNumberFields.Modulus.isCoprimeTo_of_dvd_span_singleton {K : Type u_1} [Field K] [NumberField K] {m : Modulus K} {J : Ideal (NumberField.RingOfIntegers K)} {a : NumberField.RingOfIntegers K} {x : Kˣ} (hxa : ↑x = ↑a) (hx : x ∈ primeToSubgroup m) (hdvd : J ∣ Ideal.span {a}) : m.IsCoprimeTo J

A divisor of a principal ideal with a generator prime to the modulus is prime to the modulus.

theorem TauCeti.GlobalNumberFields.Modulus.isCoprimeTo_iff_sup_eq_top {K : Type u_1} [Field K] [NumberField K] {𝔪 : Modulus K} {I : Ideal (NumberField.RingOfIntegers K)} : 𝔪.IsCoprimeTo I ↔ I ≠ ⊥ ∧ I ⊔ 𝔪.finitePart = ⊤

Being prime to the modulus is comaximality with its finite part. A prime dividing both I and the finite part is exactly a prime of the support dividing I, and such a prime exists as soon as I and the finite part fail to generate the unit ideal.

@[reducible, inline]

noncomputable abbrev TauCeti.GlobalNumberFields.integralIdealsPrimeTo {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : Submonoid (Ideal (NumberField.RingOfIntegers K))

The monoid of nonzero integral ideals prime to a modulus. There is one such monoid, the one built away from a finite set of primes; its membership predicate is Modulus.IsCoprimeTo.

Equations

• TauCeti.GlobalNumberFields.integralIdealsPrimeTo 𝔪 = TauCeti.NumberFieldArithmetic.integralIdealsAway 𝔪.support

theorem TauCeti.GlobalNumberFields.Modulus.mem_integralIdealsPrimeTo {K : Type u_1} [Field K] [NumberField K] {𝔪 : Modulus K} {I : Ideal (NumberField.RingOfIntegers K)} : I ∈ integralIdealsPrimeTo 𝔪 ↔ 𝔪.IsCoprimeTo I

theorem TauCeti.GlobalNumberFields.integralIdealsPrimeTo_antitone {K : Type u_1} [Field K] [NumberField K] {𝔪 𝔫 : Modulus K} (h : 𝔪 ∣ 𝔫) : integralIdealsPrimeTo 𝔫 ≤ integralIdealsPrimeTo 𝔪

The integral prime-to monoid is antitone in the modulus: the support of a divisor 𝔪 of 𝔫 is contained in that of 𝔫, so an ideal prime to 𝔫 is prime to 𝔪.

noncomputable def TauCeti.GlobalNumberFields.integralIdealsPrimeToInclusion {K : Type u_1} [Field K] [NumberField K] {𝔪 𝔫 : Modulus K} (h : 𝔪 ∣ 𝔫) : ↥(integralIdealsPrimeTo 𝔫) →* ↥(integralIdealsPrimeTo 𝔪)

The inclusion of the integral ideals prime to 𝔫 into those prime to 𝔪, for a divisor 𝔪 of 𝔫. It is the literal inclusion, matching NumberFieldArithmetic.idealsAwayInclusion on the fractional side.

Equations

• TauCeti.GlobalNumberFields.integralIdealsPrimeToInclusion h = Submonoid.inclusion ⋯

@[simp]

theorem TauCeti.GlobalNumberFields.coe_integralIdealsPrimeToInclusion {K : Type u_1} [Field K] [NumberField K] {𝔪 𝔫 : Modulus K} (h : 𝔪 ∣ 𝔫) (I : ↥(integralIdealsPrimeTo 𝔫)) : ↑((integralIdealsPrimeToInclusion h) I) = ↑I

The inclusion between integral prime-to monoids does not change the underlying ideal.