Ray class groups

TheoremFinite part of the modulus of a real place#✓fully proved

For a real place \(v\) of a number field \(K\), let \(\mathfrak m_v\) be the modulus of \(K\) with finite part the unit ideal \(\mathcal O_K\) and infinite part \(\{v\}\). The finite part of \(\mathfrak m_v\) is the unit ideal \(\mathcal O_K\).

@[simp] theorem infinite_finitePart (v : RealPlace K) :
    (infinite v).finitePart = 1

TheoremInfinite part of the modulus of a real place#✓fully proved

For a real place \(v\) of a number field \(K\), let \(\mathfrak m_v\) be the modulus of \(K\) with finite part the unit ideal \(\mathcal O_K\) and infinite part \(\{v\}\). The infinite part of \(\mathfrak m_v\) is the singleton \(\{v\}\).

@[simp] theorem infinite_infinitePart (v : RealPlace K) :
    (infinite v).infinitePart = {v}

DefinitionPrimes dividing a modulus#✓fully proved

Let \(\mathfrak m\) be a modulus of a number field \(K\), with finite part the nonzero ideal \(\mathfrak m_0\) of \(\mathcal O_K\). A nonzero prime ideal \(\mathfrak p\) of \(\mathcal O_K\) lies in the finite support of \(\mathfrak m\) when \(\mathfrak m_0 \subseteq \mathfrak p\), that is, when \(\mathfrak p\) divides \(\mathfrak m_0\).

def finiteSupported (m : Modulus K) (v : IsDedekindDomain.HeightOneSpectrum (𝓞 K)) : Prop :=
  (m.finitePart : Ideal (𝓞 K)) ≤ v.asIdeal

Used by 39

Used byThe Artin map at a prime · Unramified outside a modulus implies unramified at coprime primes · The coprime primes generate the coprime ideals · Prime coprime units · The prime coprime units are the image of the coprime primes · Primes coprime to a modulus · The free group on the coprime primes maps to the coprime ideals · The kernel of the free-group map lies in the commutator subgroup · The free-group map on generators · The free group on the coprime primes surjects onto the coprime ideals · Chosen Frobenius element at a coprime prime · The chosen Frobenius is an arithmetic Frobenius at an unramified prime · Extensions unramified outside a modulus · Primes not dividing the modulus are coprime to it · Membership in the prime coprime units · The prime as a coprime fractional ideal · Restriction of the Artin map at a prime · The Artin map commutes with restriction · Restriction of Frobenius elements in a tower · Coprimality passes to divisors of a modulus · Inclusion of coprime ideal groups under divisibility of moduli · Ray congruence to \(1\) passes to divisors of the modulus · Multiplicative congruence to one at the finite part · Fractional ideals coprime to a modulus · Coprime representation of ray elements · Weak approximation with a finite target and prescribed signs · Weak approximation with prescribed signs at a modulus · The finite ray-one subgroup · Kernel criterion for the finite residue map · Valuation criterion for the finite residue map to be trivial · Nonzero integral ideals coprime to the modulus are coprime fractional ideals · Integral units as ray elements · Integral units embed injectively into the ray elements · Inverses preserve congruence to one at the finite part · Elements of valuation one at the primes dividing a modulus are ray elements · Product of two elements congruent to one at the finite part · Ray elements have order zero at the primes dividing the modulus · Ray elements have valuation one at the primes dividing the modulus · Surjectivity of the residue-sign map

DefinitionExponent of a modulus at a prime#✓fully proved

Let \(\mathfrak m\) be a modulus of a number field \(K\), with finite part the nonzero ideal \(\mathfrak m_0\) of \(\mathcal O_K\). For a nonzero prime ideal \(\mathfrak p\) of \(\mathcal O_K\), the finite exponent of \(\mathfrak m\) at \(\mathfrak p\) is the integer \(v_{\mathfrak p}(\mathfrak m_0)\), the exponent of \(\mathfrak p\) in the prime factorization of \(\mathfrak m_0\).

def finiteExponent (m : Modulus K) (v : IsDedekindDomain.HeightOneSpectrum (𝓞 K)) : ℤ :=
  FractionalIdeal.count K v
    ((m.finitePart : Ideal (𝓞 K)) : FractionalIdeal (𝓞 K)⁰ K)

Used by 11

Used byExponents of a modulus grow under divisibility · Ray congruence to \(1\) passes to divisors of the modulus · Multiplicative congruence to one at the finite part · Weak approximation with a finite target and prescribed signs · Weak approximation with prescribed signs at a modulus · The finite ray-one subgroup · Kernel criterion for the finite residue map · Valuation criterion for the finite residue map to be trivial · Inverses preserve congruence to one at the finite part · Product of two elements congruent to one at the finite part · Surjectivity of the residue-sign map

DefinitionFractional ideals coprime to a modulus#✓fully proved

Let \(\mathfrak m\) be a modulus of a number field \(K\), with finite part the nonzero ideal \(\mathfrak m_0\) of \(\mathcal O_K\). For an invertible fractional ideal \(I\) of \(\mathcal O_K\) and a nonzero prime ideal \(\mathfrak p\), write \(v_{\mathfrak p}(I)\) for the exponent of \(\mathfrak p\) in the factorization of \(I\). The fractional ideals coprime to \(\mathfrak m\) form the subgroup of the group of invertible fractional ideals of \(\mathcal O_K\) consisting of those \(I\) with \(v_{\mathfrak p}(I) = 0\) for every nonzero prime ideal \(\mathfrak p\) of \(\mathcal O_K\) containing \(\mathfrak m_0\).

NumberField.Modulus.coprimeFractionalIdeals · 19 lines

def coprimeFractionalIdeals (m : Modulus K) :
    Subgroup (FractionalIdeal (𝓞 K)⁰ K)ˣ where
  carrier :=
    { u |
      ∀ v, finiteSupported m v →
        FractionalIdeal.count K v (u : FractionalIdeal (𝓞 K)⁰ K) = 0 }
  one_mem' := by
    intro v _
    rw [Units.val_one]
    exact FractionalIdeal.count_one K v
  mul_mem' := by
    intro a b ha hb v hv
    rw [Units.val_mul]
    rw [FractionalIdeal.count_mul K v (Units.ne_zero a) (Units.ne_zero b)]
    rw [ha v hv, hb v hv, add_zero]
  inv_mem' := by
    intro a ha v hv
    rw [Units.val_inv_eq_inv_val]
    rw [FractionalIdeal.count_inv K v (a : FractionalIdeal (𝓞 K)⁰ K), ha v hv, neg_zero]

Uses 1 · Used by 90

Statement usesPrimes dividing a modulus

Used byArtin map · The Artin map factors the free-group Frobenius map · The Artin map at a prime · The coprime primes generate the coprime ideals · Prime coprime units · The prime coprime units are the image of the coprime primes · The free group on the coprime primes maps to the coprime ideals · The kernel of the free-group map is the commutator subgroup · The kernel of the free-group map lies in the commutator subgroup · Kernel containment for the free-group Frobenius map · The free-group map on generators · The free group on the coprime primes surjects onto the coprime ideals · Primes not dividing the modulus are coprime to it · Membership in the prime coprime units · The prime as a coprime fractional ideal · Restriction of the Artin map at a prime · The Artin map commutes with restriction · Change of modulus of a congruence subgroup · The change of modulus is equivalent to the original pair · Ambient subgroup of a change of modulus · Ambient subgroup of a change of modulus to a divisor · Congruence subgroup · Coprimality passes to divisors of a modulus · Criterion for an equivalent congruence subgroup at a divisor of the modulus · Image of a congruence subgroup in the ray class group · Equivalence of congruence subgroup pairs · Criterion for equivalence of congruence subgroup pairs · Largest congruence subgroup · Membership in the image of a congruence subgroup · Ray group among all fractional ideals · The ray group consists of coprime ideals · A congruence subgroup contains the ray group · Equivalence of congruence subgroup pairs is reflexive · Smallest congruence subgroup · Equivalence of congruence subgroup pairs is symmetric · Congruence subgroup as a subgroup of all invertible fractional ideals · Inclusion of coprime ideal groups under divisibility of moduli · Complex value of a ray class character · Ray class characters take the complex value \(1\) on the ray group · Extension by zero of a ray class character · Induced ray class character · Induced characters agree on coprime ideals · Primitivity in terms of the level-change map · Level-change map on ray class groups · The level-change map on ray classes · Ray congruence to \(1\) passes to divisors of the modulus · Pullback of a ray class character to ideals · Pulled-back ray class characters are trivial on the ray group · Ray class character · Trivial character · Ideal-class map on coprime fractional ideals · Value of the ideal-class map on a coprime ideal · Every ideal class contains a fractional ideal coprime to the modulus · Nonzero integral ideals coprime to the modulus are coprime fractional ideals · Exactness at the ray-element quotient · Exactness at the residue-sign group · Elements of valuation one at the primes dividing a modulus are ray elements · Principal ray ideal map · Value of the principal ray ideal map · Integral units generate the unit ideal · Ray class group · Ray class map · The ray class exact sequence, sign and residue form · The ray class exact sequence · Projection from the ray class group to the class group · The ideal-class map factors through the ray class group · Kernel of the projection from the ray class group to the class group · Projection to the class group on ray class representatives · Projecting the image of a ray element to the class group · Projecting the image of a residue-sign value to the class group · The ray class group surjects onto the class group · Ray-element class map · Value of the ray-element class map · Ray elements have order zero at the primes dividing the modulus · Elements coprime to a modulus · Generators of the ray group · The ray group of a modulus · The ray group is the image of the ray-one elements · The ray group lies in the kernel of the ideal-class map · Ray-one elements have trivial ray class · Quotient-to-ray-class map · Exactness at the ray-element quotient (kernel form) · Quotient-to-ray-class map on representatives · Exactness at the ray class group · Ray class map on residues and signs · The residue-sign transport square commutes · Residue-sign-to-ray-class map through the quotient isomorphism · Kernel of the ray class map on residue-sign values · Exactness at the ray class group, residue-sign form · Ray class map on residue-sign values

DefinitionElements coprime to a modulus#✓fully proved

Let \(\mathfrak m\) be a modulus of a number field \(K\), with finite part the nonzero ideal \(\mathfrak m_0\) of \(\mathcal O_K\). The elements coprime to \(\mathfrak m\) form the subgroup of \(K^\times\) consisting of those \(x\) whose principal fractional ideal \((x)\) is coprime to \(\mathfrak m\), that is, has exponent \(0\) at every nonzero prime ideal \(\mathfrak p\) of \(\mathcal O_K\) containing \(\mathfrak m_0\).

def rayElements (m : Modulus K) : Subgroup Kˣ :=
  Subgroup.comap (toPrincipalIdeal (𝓞 K) K)
    (coprimeFractionalIdeals m)

Uses 1 · Used by 65

Statement usesFractional ideals coprime to a modulus

Used byLevel-change map on ray class groups · Ray congruence to \(1\) passes to divisors of the modulus · Coprime representation of ray elements · The finite ray-one subgroup · Finite residue map · Computing the finite residue map from a representation · Kernel criterion for the finite residue map · Valuation criterion for the finite residue map to be trivial · Kernel of the finite residue map · Infinite sign map of a modulus · Coordinates of the infinite sign map · Trivial infinite sign means positivity at the modulus · Ray-one integral units · Exactness of the ray sequence at the integral units · Integral units as ray elements · Ray-element image of an integral unit as a field unit · Integral units embed injectively into the ray elements · Map from integral units to the ray quotient · Value of the ray-quotient map on integral units · Kernel of the ray-quotient map on integral units · Exactness at the ray-element quotient · Residue-sign map on integral units · Value of the residue-sign map on integral units · Kernel of the residue-sign map on integral units · Inverses preserve congruence to one at the finite part · Elements congruent to one modulo a modulus · Membership in the ray-one integral units · Membership in the positive ray elements · Elements of valuation one at the primes dividing a modulus are ray elements · Membership in the ray-one subgroup · Product of two elements congruent to one at the finite part · Ray elements positive at the infinite part · Principal ray ideal map · Value of the principal ray ideal map · Integral units generate the unit ideal · The ray class exact sequence · Kernel of the projection from the ray class group to the class group · Projecting the image of a ray element to the class group · Projecting the image of a residue-sign value to the class group · Ray-element class map · Value of the ray-element class map · Ray elements have order zero at the primes dividing the modulus · Ray elements have valuation one at the primes dividing the modulus · The residue-sign isomorphism · The residue-sign isomorphism on classes · Generators of the ray group · The ray group is the image of the ray-one elements · The ray group lies in the kernel of the ideal-class map · Ray-one subgroup · Ray-one elements have trivial ray class · Quotient-to-ray-class map · Exactness at the ray-element quotient (kernel form) · Quotient-to-ray-class map on representatives · Exactness at the ray class group · Residue-sign map · Components of the residue-sign map · Kernel criterion for the residue-sign map · Kernel of the residue-sign map · Surjectivity of the residue-sign map · Ray class map on residues and signs · The residue-sign transport square commutes · Residue-sign-to-ray-class map through the quotient isomorphism · Kernel of the ray class map on residue-sign values · Exactness at the ray class group, residue-sign form · Ray class map on residue-sign values

DefinitionMultiplicative congruence to one at the finite part#✓fully proved

Let \(\mathfrak m\) be a modulus of a number field \(K\), with finite part the nonzero ideal \(\mathfrak m_0\) of \(\mathcal O_K\). For a nonzero prime ideal \(\mathfrak p\) of \(\mathcal O_K\), write \(v_{\mathfrak p}(I)\) for the exponent of \(\mathfrak p\) in the factorization of a nonzero fractional ideal \(I\) of \(\mathcal O_K\), and for \(y \in K\) write \(v_{\mathfrak p}(y) = v_{\mathfrak p}((y))\) (with \(v_{\mathfrak p}(0) = 0\)). An element \(x \in K^\times\) is congruent to \(1\) at the finite part of \(\mathfrak m\) when, for every nonzero prime ideal \(\mathfrak p\) of \(\mathcal O_K\) containing \(\mathfrak m_0\), either \(x = 1\) or \(v_{\mathfrak p}(\mathfrak m_0) \le v_{\mathfrak p}(x - 1)\).

def CongruentOneAtFinitePart (m : Modulus K) (x : Kˣ) : Prop :=
  ∀ v, finiteSupported m v →
    (x : K) = 1 ∨
      finiteExponent m v ≤
        FractionalIdeal.count K v
          (FractionalIdeal.spanSingleton (𝓞 K)⁰ ((x : K) - 1))

Uses 2 · Used by 14

Statement usesExponent of a modulus at a prime · Primes dividing a modulus

Used byLevel-change map on ray class groups · Ray congruence to \(1\) passes to divisors of the modulus · The finite ray-one subgroup · Kernel criterion for the finite residue map · Valuation criterion for the finite residue map to be trivial · Kernel of the finite residue map · Inverses preserve congruence to one at the finite part · Elements congruent to one modulo a modulus · Membership in the ray-one integral units · Membership in the ray-one subgroup · Product of two elements congruent to one at the finite part · Generators of the ray group · The ray group is the image of the ray-one elements · Kernel criterion for the residue-sign map

DefinitionPositivity at the infinite part of a modulus#✓fully proved

Let \(\mathfrak m\) be a modulus of a number field \(K\), with infinite part the finite set \(\mathfrak m_\infty\) of real places of \(K\). An element \(x \in K^\times\) is positive at the infinite part of \(\mathfrak m\) when \(\sigma_w(x) > 0\) for every real place \(w \in \mathfrak m_\infty\), where \(\sigma_w \colon K \to \mathbb R\) is the real embedding corresponding to \(w\).

def PositiveAtInfinitePart (m : Modulus K) (x : Kˣ) : Prop :=
  ∀ w : RealPlace K, w ∈ m.infinitePart →
    InfinitePlace.embedding_of_isReal w.property (x : K) > 0

Used by 10

Used byLevel-change map on ray class groups · Ray congruence to \(1\) passes to divisors of the modulus · Trivial infinite sign means positivity at the modulus · Elements congruent to one modulo a modulus · Membership in the ray-one integral units · Membership in the positive ray elements · Membership in the ray-one subgroup · Generators of the ray group · The ray group is the image of the ray-one elements · Kernel criterion for the residue-sign map

DefinitionElements congruent to one modulo a modulus#✓fully proved

Let \(\mathfrak m\) be a modulus of a number field \(K\), with finite part the nonzero ideal \(\mathfrak m_0\) of \(\mathcal O_K\) and infinite part the finite set \(\mathfrak m_\infty\) of real places of \(K\). For a nonzero prime ideal \(\mathfrak p\) of \(\mathcal O_K\), write \(v_{\mathfrak p}(I)\) for the exponent of \(\mathfrak p\) in the factorization of a nonzero fractional ideal \(I\) of \(\mathcal O_K\), and for \(y \in K\) write \(v_{\mathfrak p}(y) = v_{\mathfrak p}((y))\) (with \(v_{\mathfrak p}(0) = 0\)); for a real place \(w\) write \(\sigma_w \colon K \to \mathbb R\) for the corresponding real embedding. An element \(x \in K^\times\) is congruent to \(1\) modulo \(\mathfrak m\) when, for every nonzero prime ideal \(\mathfrak p\) of \(\mathcal O_K\) containing \(\mathfrak m_0\), \(v_{\mathfrak p}(x) = 0\) and either \(x = 1\) or \(v_{\mathfrak p}(\mathfrak m_0) \le v_{\mathfrak p}(x - 1)\), and \(\sigma_w(x) > 0\) for every real place \(w \in \mathfrak m_\infty\).

def IsRayElementOne (m : Modulus K) (x : Kˣ) : Prop :=
  x ∈ rayElements m ∧ CongruentOneAtFinitePart m x ∧ PositiveAtInfinitePart m x

Uses 3 · Used by 6

Statement usesMultiplicative congruence to one at the finite part · Positivity at the infinite part of a modulus · Elements coprime to a modulus

Used byLevel-change map on ray class groups · Ray congruence to \(1\) passes to divisors of the modulus · Membership in the ray-one integral units · Generators of the ray group · The ray group is the image of the ray-one elements · Kernel criterion for the residue-sign map

DefinitionGenerators of the ray group#✓fully proved

Let \(\mathfrak m\) be a modulus of a number field \(K\). The ray generators of \(\mathfrak m\) are the fractional ideals coprime to \(\mathfrak m\) of the form \((x)\), the principal fractional ideal of an element \(x \in K^\times\) that is congruent to \(1\) modulo \(\mathfrak m\).

def rayGenerators (m : Modulus K) : Set (coprimeFractionalIdeals m) :=
  { y |
    ∃ x : Kˣ, ∃ hx : IsRayElementOne m x,
      (⟨toPrincipalIdeal (𝓞 K) K x,
        Subgroup.mem_comap.mp hx.1⟩ :
        coprimeFractionalIdeals m) = y }

Uses 5 · Used by 3

Statement usesMultiplicative congruence to one at the finite part · Elements congruent to one modulo a modulus · Positivity at the infinite part of a modulus · Fractional ideals coprime to a modulus · Elements coprime to a modulus

Used byLevel-change map on ray class groups · The ray group of a modulus · The ray group is the image of the ray-one elements

DefinitionThe ray group of a modulus#✓fully proved

Let \(\mathfrak m\) be a modulus of a number field \(K\). The ray group of \(\mathfrak m\) is the subgroup of the group of fractional ideals coprime to \(\mathfrak m\) generated by the principal ideals \((x)\) of the elements \(x \in K^\times\) congruent to \(1\) modulo \(\mathfrak m\).

def rayGroup (m : Modulus K) : Subgroup (coprimeFractionalIdeals m) :=
  Subgroup.closure (rayGenerators m)

Uses 2 · Used by 50

Statement usesFractional ideals coprime to a modulus · Generators of the ray group

Used byChange of modulus of a congruence subgroup · Ambient subgroup of a change of modulus · Congruence subgroup · Image of a congruence subgroup in the ray class group · Largest congruence subgroup · Membership in the image of a congruence subgroup · Ray group among all fractional ideals · The ray group consists of coprime ideals · A congruence subgroup contains the ray group · Smallest congruence subgroup · Complex value of a ray class character · Ray class characters take the complex value \(1\) on the ray group · Extension by zero of a ray class character · Induced ray class character · Induced characters agree on coprime ideals · Primitivity in terms of the level-change map · Level-change map on ray class groups · The level-change map on ray classes · Pullback of a ray class character to ideals · Pulled-back ray class characters are trivial on the ray group · Ray class character · Trivial character · Exactness at the ray-element quotient · Exactness at the residue-sign group · Ray class group · Ray class map · The ray class exact sequence, sign and residue form · The ray class exact sequence · Projection from the ray class group to the class group · The ideal-class map factors through the ray class group · Kernel of the projection from the ray class group to the class group · Projection to the class group on ray class representatives · Projecting the image of a ray element to the class group · Projecting the image of a residue-sign value to the class group · The ray class group surjects onto the class group · Ray-element class map · Value of the ray-element class map · The ray group is the image of the ray-one elements · The ray group lies in the kernel of the ideal-class map · Ray-one elements have trivial ray class · Quotient-to-ray-class map · Exactness at the ray-element quotient (kernel form) · Quotient-to-ray-class map on representatives · Exactness at the ray class group · Ray class map on residues and signs · The residue-sign transport square commutes · Residue-sign-to-ray-class map through the quotient isomorphism · Kernel of the ray class map on residue-sign values · Exactness at the ray class group, residue-sign form · Ray class map on residue-sign values

TheoremLower bound for the exponent of a sum#✓fully proved

Let \(K\) be a number field and \(\mathfrak p\) a nonzero prime ideal of \(\mathcal O_K\). For \(x \in K\) write \(c_{\mathfrak p}(x)\) for the exponent of \(\mathfrak p\) in the principal fractional ideal \(x \mathcal O_K\), with the convention \(c_{\mathfrak p}(0) = 0\). If \(x, y \in K\) satisfy \(x + y \neq 0\) and \(n \in \mathbb Z\) satisfies \(n \le c_{\mathfrak p}(x)\) and \(n \le c_{\mathfrak p}(y)\), then \(n \le c_{\mathfrak p}(x + y)\).

Only \(x + y \neq 0\) is assumed: \(x\) or \(y\) may be zero.

theorem count_spanSingleton_add_ge_of_ne_zero
    (v : IsDedekindDomain.HeightOneSpectrum (𝓞 K))
    {x y : K} {n : ℤ} (hxy : x + y ≠ 0)
    (hx : n ≤ FractionalIdeal.count K v
      (FractionalIdeal.spanSingleton (𝓞 K)⁰ x))
    (hy : n ≤ FractionalIdeal.count K v
      (FractionalIdeal.spanSingleton (𝓞 K)⁰ y)) :
    n ≤ FractionalIdeal.count K v
      (FractionalIdeal.spanSingleton (𝓞 K)⁰ (x + y))

Used by 1

Used byProduct of two elements congruent to one at the finite part

TheoremRay elements have order zero at the primes dividing the modulus#✓fully proved

Let \(m\) be a modulus of a number field \(K\) and let \(x \in K^\times\) be a ray element of \(m\). Then for every finite prime \(\mathfrak p\) of \(K\) dividing the finite part of \(m\), the exponent of \(\mathfrak p\) in the principal fractional ideal \(x \mathcal O_K\) is \(0\).

theorem rayElement_count_spanSingleton_eq_zero
    (m : Modulus K) (x : Kˣ)
    (hx : x ∈ rayElements m)
    (v : IsDedekindDomain.HeightOneSpectrum (𝓞 K))
    (hv : finiteSupported m v) :
    FractionalIdeal.count K v
      (FractionalIdeal.spanSingleton (𝓞 K)⁰ (x : K)) = 0

Uses 3 · Used by 3

Statement usesPrimes dividing a modulus · Elements coprime to a modulus

Proof usesFractional ideals coprime to a modulus

Used byInverses preserve congruence to one at the finite part · Product of two elements congruent to one at the finite part · Ray elements have valuation one at the primes dividing the modulus

TheoremRay elements have valuation one at the primes dividing the modulus#✓fully proved

Let \(m\) be a modulus of a number field \(K\) and let \(x \in K^\times\) be a ray element of \(m\). Then for every finite prime \(\mathfrak p\) of \(K\) dividing the finite part of \(m\), the multiplicative \(\mathfrak p\)-adic valuation of \(x\) equals \(1\).

theorem rayElement_valuation_eq_one
    (m : Modulus K) (x : rayElements m)
    (v : IsDedekindDomain.HeightOneSpectrum (𝓞 K))
    (hv : finiteSupported m v) :
    v.valuation K (((x : Kˣ) : K)) = 1

Sources

• N406 §21.3, the supported-finite-place fact; compare valuation_eq_one_of_spanSingleton_coprime' and hx_coprime.

Uses 3 · Used by 1

Statement usesPrimes dividing a modulus · Elements coprime to a modulus

Proof usesRay elements have order zero at the primes dividing the modulus

Used byCoprime representation of ray elements

TheoremElements of valuation one at the primes dividing a modulus are ray elements#✓fully proved

Let \(K\) be a number field, \(\mathfrak m\) a modulus of \(K\) with finite part \(\mathfrak m_0\), and \(a \in K^\times\). If the multiplicative \(\mathfrak p\)-adic valuation of \(a\) equals \(1\) at every nonzero prime ideal \(\mathfrak p\) of \(\mathcal O_K\) containing \(\mathfrak m_0\), then \(a\) is coprime to \(\mathfrak m\), that is, a ray element of \(\mathfrak m\): its principal fractional ideal \((a)\) has exponent \(0\) at every such \(\mathfrak p\).

theorem mem_rayElements_of_valuation_eq_one
    (m : Modulus K) (a : Kˣ)
    (h : ∀ v : IsDedekindDomain.HeightOneSpectrum (𝓞 K),
      finiteSupported m v → v.valuation K ((a : K)) = 1) :
    a ∈ rayElements m

Sources

• N406 Section 21.3. This is the converse of rayElement_valuation_eq_one, the converse valuation criterion used to turn the controlled approximation witness into a ray element; it is a reusable bridge toward N406, not itself the full source theorem.

Uses 3 · Used by 3

Statement usesPrimes dividing a modulus · Elements coprime to a modulus

Proof usesFractional ideals coprime to a modulus

Used byIntegral units as ray elements · Integral units embed injectively into the ray elements · Surjectivity of the residue-sign map

TheoremProduct of two elements congruent to one at the finite part#✓fully proved

Let \(m\) be a modulus of a number field \(K\) and let \(x, y \in K^\times\) both be congruent to \(1\) at the finite part of \(m\). If moreover \(x\) is a ray element of \(m\), then \(xy\) is congruent to \(1\) at the finite part of \(m\).

theorem CongruentOneAtFinitePart.mul
    {m : Modulus K} {x y : Kˣ}
    (hx : CongruentOneAtFinitePart m x)
    (hy : CongruentOneAtFinitePart m y)
    (hmem : x ∈ rayElements m) :
    CongruentOneAtFinitePart m (x * y)

Uses 6 · Used by 1

Statement usesMultiplicative congruence to one at the finite part · Elements coprime to a modulus

Proof usesLower bound for the exponent of a sum · Exponent of a modulus at a prime · Primes dividing a modulus · Ray elements have order zero at the primes dividing the modulus

Used byThe finite ray-one subgroup

TheoremInverses preserve congruence to one at the finite part#✓fully proved

Let \(K\) be a number field and \(\mathfrak m\) a modulus of \(K\). If a ray element \(x\) of \(\mathfrak m\) is congruent to \(1\) at the finite part of \(\mathfrak m\), then so is \(x^{-1}\).

theorem CongruentOneAtFinitePart.inv
    {m : Modulus K} {x : Kˣ}
    (hx : CongruentOneAtFinitePart m x)
    (hmem : x ∈ rayElements m) :
    CongruentOneAtFinitePart m x⁻¹

Uses 5 · Used by 1

Statement usesMultiplicative congruence to one at the finite part · Elements coprime to a modulus

Proof usesExponent of a modulus at a prime · Primes dividing a modulus · Ray elements have order zero at the primes dividing the modulus

Used byThe finite ray-one subgroup

DefinitionThe finite ray-one subgroup#✓fully proved

Let \(K\) be a number field and \(\mathfrak m\) a modulus of \(K\) with finite part \(\mathfrak m_0\). The finite ray-one subgroup of \(\mathfrak m\) is the subgroup of the group of ray elements of \(\mathfrak m\) consisting of the \(x\) that are congruent to \(1\) at the finite part of \(\mathfrak m\): for every nonzero prime \(\mathfrak p\) of \(\mathcal O_K\) containing \(\mathfrak m_0\), either \(x = 1\) or the exponent of \(\mathfrak p\) in \((x - 1) \mathcal O_K\) is at least the exponent of \(\mathfrak p\) in \(\mathfrak m_0\).

def finiteRayOneElements (m : Modulus K) : Subgroup (rayElements m) where
  carrier := { x | CongruentOneAtFinitePart m (x : Kˣ) }
  one_mem' := by
    simpa using congruentOneAtFinitePart_one m
  mul_mem' := by
    intro a b ha hb
    change CongruentOneAtFinitePart m ((a * b : rayElements m) : Kˣ)
    rw [Subgroup.coe_mul]
    exact CongruentOneAtFinitePart.mul ha hb a.property
  inv_mem' := by
    intro a ha
    change CongruentOneAtFinitePart m ((a⁻¹ : rayElements m) : Kˣ)
    rw [Subgroup.coe_inv]
    exact CongruentOneAtFinitePart.inv ha a.property

Uses 6 · Used by 4

Statement usesMultiplicative congruence to one at the finite part · Inverses preserve congruence to one at the finite part · Product of two elements congruent to one at the finite part · Exponent of a modulus at a prime · Primes dividing a modulus · Elements coprime to a modulus

Used byKernel of the finite residue map · Membership in the ray-one subgroup · Ray-one subgroup · Kernel of the residue-sign map

TheoremCoprime representation of ray elements#✓fully proved

Let \(K\) be a number field and \(\mathfrak m\) a modulus of \(K\) with finite part \(\mathfrak m_0\), a nonzero ideal of \(\mathcal O_K\). Every ray element \(x\) of \(\mathfrak m\) can be written as \(x = a / b\) in \(K\) with \(a, b \in \mathcal O_K\) whose residue classes are units of \(\mathcal O_K / \mathfrak m_0\).

Source (N406 §21.3): the coprime_rep_exists admissible integral numerator/denominator representation with both residues units.

theorem exists_isUnit_mod_finitePart_div_eq
    (m : Modulus K) (x : rayElements m) :
    ∃ a b : 𝓞 K,
      IsUnit (Ideal.Quotient.mk (m.finitePart : Ideal (𝓞 K)) a) ∧
      IsUnit (Ideal.Quotient.mk (m.finitePart : Ideal (𝓞 K)) b) ∧
      algebraMap (𝓞 K) K a / algebraMap (𝓞 K) K b = ((x : Kˣ) : K)

Uses 3 · Used by 3

Statement usesElements coprime to a modulus

Proof usesPrimes dividing a modulus · Ray elements have valuation one at the primes dividing the modulus

Used byFinite residue map · Computing the finite residue map from a representation · Kernel criterion for the finite residue map

TheoremEqual fractions give equal residues modulo the finite part#✓fully proved

Let \(m\) be a modulus of a number field \(K\) with finite part \(\mathfrak m_0\), an ideal of \(\mathcal O_K\), and write \(\bar x\) for the image of \(x \in \mathcal O_K\) in \(\mathcal O_K / \mathfrak m_0\). Let \(a, b, c, d \in \mathcal O_K\) be such that \(\bar a\), \(\bar b\), \(\bar c\) and \(\bar d\) are units. If \(a / b = c / d\) in \(K\), then \(\bar a \bar b^{-1} = \bar c \bar d^{-1}\) in the unit group \((\mathcal O_K / \mathfrak m_0)^\times\).

theorem quotientUnits_div_eq_of_div_eq
    (m : Modulus K) (a b c d : 𝓞 K)
    (ha : IsUnit (Ideal.Quotient.mk (m.finitePart : Ideal (𝓞 K)) a))
    (hb : IsUnit (Ideal.Quotient.mk (m.finitePart : Ideal (𝓞 K)) b))
    (hc : IsUnit (Ideal.Quotient.mk (m.finitePart : Ideal (𝓞 K)) c))
    (hd : IsUnit (Ideal.Quotient.mk (m.finitePart : Ideal (𝓞 K)) d))
    (h : algebraMap (𝓞 K) K a / algebraMap (𝓞 K) K b =
      algebraMap (𝓞 K) K c / algebraMap (𝓞 K) K d) :
    ha.unit * hb.unit⁻¹ = hc.unit * hd.unit⁻¹

Used by 2

Used byFinite residue map · Computing the finite residue map from a representation

DefinitionFinite residue map#✓fully proved

Let \(K\) be a number field and \(\mathfrak m\) a modulus of \(K\) with finite part \(\mathfrak m_0\), a nonzero ideal of \(\mathcal O_K\). The finite residue map of \(\mathfrak m\) is the group homomorphism from the ray elements of \(\mathfrak m\) to \((\mathcal O_K / \mathfrak m_0)^\times\) sending \(x\) to \(\bar a \bar b^{-1}\), where \(x = a / b\) with \(a, b \in \mathcal O_K\) whose residue classes \(\bar a, \bar b\) are units of \(\mathcal O_K / \mathfrak m_0\); such \(a\) and \(b\) exist, and the value does not depend on their choice.

Source (N406 §21.3): the finitePartMapHom finite component of the quotient isomorphism.

NumberField.Modulus.finiteResidueMap · 36 lines

noncomputable def finiteResidueMap (m : Modulus K) :
    rayElements m →* (𝓞 K ⧸ (m.finitePart : Ideal (𝓞 K)))ˣ where
  toFun := finiteResidueMapFn m
  map_one' := by
    have h := finiteResidueMapFn_eq_of_div_eq m 1 1 1 isUnit_one isUnit_one
      (by simp)
    simpa using h
  map_mul' := fun x y => by
    obtain ⟨a1, b1, ha1, hb1, r1⟩ := exists_isUnit_mod_finitePart_div_eq m x
    obtain ⟨a2, b2, ha2, hb2, r2⟩ := exists_isUnit_mod_finitePart_div_eq m y
    have h12a : IsUnit
        (Ideal.Quotient.mk (m.finitePart : Ideal (𝓞 K)) (a1 * a2)) := by
      rw [map_mul]
      exact IsUnit.mul ha1 ha2
    have h12b : IsUnit
        (Ideal.Quotient.mk (m.finitePart : Ideal (𝓞 K)) (b1 * b2)) := by
      rw [map_mul]
      exact IsUnit.mul hb1 hb2
    have hfrac : algebraMap (𝓞 K) K (a1 * a2) / algebraMap (𝓞 K) K (b1 * b2) =
        (((x * y : rayElements m) : Kˣ) : K) := by
      rw [map_mul, map_mul, ← div_mul_div_comm, r1, r2, Subgroup.coe_mul,
        Units.val_mul]
    have hx := finiteResidueMapFn_eq_of_div_eq m x a1 b1 ha1 hb1 r1
    have hy := finiteResidueMapFn_eq_of_div_eq m y a2 b2 ha2 hb2 r2
    have hxy := finiteResidueMapFn_eq_of_div_eq m (x * y) (a1 * a2) (b1 * b2)
      h12a h12b hfrac
    have hu1 : h12a.unit = ha1.unit * ha2.unit := by
      apply Units.ext
      simp only [Units.val_mul, IsUnit.unit_spec, map_mul]
    have hu2 : h12b.unit = hb1.unit * hb2.unit := by
      apply Units.ext
      simp only [Units.val_mul, IsUnit.unit_spec, map_mul]
    change finiteResidueMapFn m (x * y) =
      finiteResidueMapFn m x * finiteResidueMapFn m y
    rw [hx, hy, hxy, hu1, hu2]
    simp [mul_inv_rev, mul_comm, mul_assoc, mul_left_comm]

Uses 3 · Used by 8

Statement usesCoprime representation of ray elements · Equal fractions give equal residues modulo the finite part · Elements coprime to a modulus

Used byComputing the finite residue map from a representation · Kernel criterion for the finite residue map · Valuation criterion for the finite residue map to be trivial · Kernel of the finite residue map · Residue-sign map · Components of the residue-sign map · Kernel of the residue-sign map · Surjectivity of the residue-sign map

TheoremComputing the finite residue map from a representation#✓fully proved

Let \(K\) be a number field and \(\mathfrak m\) a modulus of \(K\) with finite part \(\mathfrak m_0\). Let \(x\) be a ray element of \(\mathfrak m\), and let \(a, b \in \mathcal O_K\) have residue classes \(\bar a, \bar b\) that are units of \(\mathcal O_K / \mathfrak m_0\) and satisfy \(a / b = x\) in \(K\). Then the finite residue map of \(\mathfrak m\) sends \(x\) to \(\bar a \bar b^{-1}\) in \((\mathcal O_K / \mathfrak m_0)^\times\).

Source (N406 §21.3): the representation-independence computation coprime_rep_well_def for the finite component.

theorem finiteResidueMap_apply_of_div_eq
    (m : Modulus K) (x : rayElements m) (a b : 𝓞 K)
    (ha : IsUnit (Ideal.Quotient.mk (m.finitePart : Ideal (𝓞 K)) a))
    (hb : IsUnit (Ideal.Quotient.mk (m.finitePart : Ideal (𝓞 K)) b))
    (hab : algebraMap (𝓞 K) K a / algebraMap (𝓞 K) K b =
      ((x : Kˣ) : K)) :
    finiteResidueMap m x = ha.unit * hb.unit⁻¹

Uses 4 · Used by 2

Statement usesFinite residue map · Elements coprime to a modulus

Proof usesCoprime representation of ray elements · Equal fractions give equal residues modulo the finite part

Used byKernel criterion for the finite residue map · Surjectivity of the residue-sign map

TheoremKernel criterion for the finite residue map#✓fully proved

Let \(K\) be a number field and \(\mathfrak m\) a modulus of \(K\). A ray element \(x\) of \(\mathfrak m\) is sent to \(1\) by the finite residue map of \(\mathfrak m\) if and only if \(x\) is congruent to \(1\) at the finite part of \(\mathfrak m\).

Source (N406 §21.3): helper finitePartMapHom_ker_iff.

theorem finiteResidueMap_eq_one_iff (m : Modulus K) (x : rayElements m) :
    finiteResidueMap m x = 1 ↔ CongruentOneAtFinitePart m (x : Kˣ)

Uses 7 · Used by 2

Statement usesMultiplicative congruence to one at the finite part · Finite residue map · Elements coprime to a modulus

Proof usesCoprime representation of ray elements · Exponent of a modulus at a prime · Computing the finite residue map from a representation · Primes dividing a modulus

Used byValuation criterion for the finite residue map to be trivial · Kernel of the finite residue map

TheoremKernel of the finite residue map#✓fully proved

Let \(K\) be a number field and \(\mathfrak m\) a modulus of \(K\). The kernel of the finite residue map of \(\mathfrak m\) is the finite ray-one subgroup of \(\mathfrak m\).

Source (N406 §21.3): the finite kernel component used in the theorem_21_8_quotient_iso.

theorem finiteResidueMap_ker (m : Modulus K) :
    (finiteResidueMap m).ker = finiteRayOneElements m

Uses 5 · Used by 1

Statement usesThe finite ray-one subgroup · Finite residue map · Elements coprime to a modulus

Proof usesMultiplicative congruence to one at the finite part · Kernel criterion for the finite residue map

Used byKernel of the residue-sign map

TheoremValuation criterion for the finite residue map to be trivial#✓fully proved

Let \(K\) be a number field, \(\mathfrak m\) a modulus of \(K\) with finite part \(\mathfrak m_0\), and \(z\) a ray element of \(\mathfrak m\). Suppose that at every nonzero prime ideal \(\mathfrak p\) of \(\mathcal O_K\) containing \(\mathfrak m_0\), the multiplicative \(\mathfrak p\)-adic valuation of \(z - 1\) is at most \(\exp(-e_{\mathfrak p})\), where \(e_{\mathfrak p}\) is the exponent of \(\mathfrak p\) in \(\mathfrak m_0\); equivalently, \(z = 1\) or \(z - 1\) has \(\mathfrak p\)-adic order at least \(e_{\mathfrak p}\). Then the finite residue map of \(\mathfrak m\) sends \(z\) to \(1\) in \((\mathcal O_K / \mathfrak m_0)^\times\).

theorem finiteResidueMap_eq_one_of_valuation_le
    (m : Modulus K) (z : rayElements m)
    (h : ∀ v : IsDedekindDomain.HeightOneSpectrum (𝓞 K),
      finiteSupported m v →
        v.valuation K (((z : Kˣ) : K) - 1) ≤
          WithZero.exp (-(finiteExponent m v))) :
    finiteResidueMap m z = 1

Sources

• N406, Theorem 21.8, Section 21.3 (ATLAS NumberTheoryI item N406): the native-API finite-congruence step corresponding to finitePartMapHom_ker_iff, used by the weak-approximation argument before residue/sign surjectivity and by theorem_21_8_quotient_iso. It is not the generalized weak-approximation theorem and not the final N406 result.

Uses 6 · Used by 1

Statement usesExponent of a modulus at a prime · Finite residue map · Primes dividing a modulus · Elements coprime to a modulus

Proof usesMultiplicative congruence to one at the finite part · Kernel criterion for the finite residue map

Used bySurjectivity of the residue-sign map

AbbreviationRay class group#✓fully proved

The ray class group of a modulus \(\mathfrak m\) of a number field \(K\) is the quotient of the group of nonzero fractional ideals of \(K\) coprime to the finite part of \(\mathfrak m\) by the ray group of \(\mathfrak m\).

abbrev RayClassGroup (m : Modulus K) :=
  ↥(coprimeFractionalIdeals m) ⧸ rayGroup m

Uses 2 · Used by 39

Statement usesFractional ideals coprime to a modulus · The ray group of a modulus

Used byImage of a congruence subgroup in the ray class group · Membership in the image of a congruence subgroup · Complex value of a ray class character · Ray class characters take the complex value \(1\) on the ray group · Extension by zero of a ray class character · Induced ray class character · Induced characters agree on coprime ideals · Primitivity in terms of the level-change map · Level-change map on ray class groups · The level-change map on ray classes · Pullback of a ray class character to ideals · Pulled-back ray class characters are trivial on the ray group · Ray class character · Trivial character · Exactness at the ray-element quotient · Exactness at the residue-sign group · Ray class map · The ray class exact sequence, sign and residue form · The ray class exact sequence · Projection from the ray class group to the class group · The ideal-class map factors through the ray class group · Kernel of the projection from the ray class group to the class group · Projection to the class group on ray class representatives · Projecting the image of a ray element to the class group · Projecting the image of a residue-sign value to the class group · The ray class group surjects onto the class group · Ray-element class map · Value of the ray-element class map · Ray-one elements have trivial ray class · Quotient-to-ray-class map · Exactness at the ray-element quotient (kernel form) · Quotient-to-ray-class map on representatives · Exactness at the ray class group · Ray class map on residues and signs · The residue-sign transport square commutes · Residue-sign-to-ray-class map through the quotient isomorphism · Kernel of the ray class map on residue-sign values · Exactness at the ray class group, residue-sign form · Ray class map on residue-sign values

DefinitionRay class map#✓fully proved

For a modulus \(\mathfrak m\) of a number field \(K\), the ray class map is the canonical quotient homomorphism from the group of nonzero fractional ideals of \(K\) coprime to the finite part of \(\mathfrak m\) onto the ray class group of \(\mathfrak m\), sending each such ideal to its class modulo the ray group of \(\mathfrak m\).

def rayClassMap (m : Modulus K) :
    coprimeFractionalIdeals m →* RayClassGroup m :=
  QuotientGroup.mk' (rayGroup m)

Uses 3 · Used by 19

Statement usesRay class group · Fractional ideals coprime to a modulus · The ray group of a modulus

Used byImage of a congruence subgroup in the ray class group · Membership in the image of a congruence subgroup · Ray class characters take the complex value \(1\) on the ray group · Extension by zero of a ray class character · Induced characters agree on coprime ideals · The level-change map on ray classes · Pullback of a ray class character to ideals · Pulled-back ray class characters are trivial on the ray group · The ideal-class map factors through the ray class group · Kernel of the projection from the ray class group to the class group · Projection to the class group on ray class representatives · Projecting the image of a ray element to the class group · Projecting the image of a residue-sign value to the class group · The ray class group surjects onto the class group · Ray-element class map · Value of the ray-element class map · Ray-one elements have trivial ray class · Exactness at the ray-element quotient (kernel form) · Quotient-to-ray-class map on representatives

DefinitionSign of a unit at a real place#✓fully proved

For a real place \(w\) of a number field \(K\), let \(\sigma_w \colon K \to \mathbb{R}\) be the corresponding real embedding. The sign at \(w\) is the group homomorphism from \(K^\times\) to \(\mathbb{Z}/2\mathbb{Z}\), written multiplicatively, that sends \(x\) to the class of \(0\) (the identity) if \(\sigma_w(x) > 0\) and to the class of \(1\) otherwise.

NumberField.Modulus.signAtRealPlace · 27 lines

noncomputable def signAtRealPlace (w : RealPlace K) :
    Kˣ →* Multiplicative (ZMod 2) where
  toFun x :=
    Multiplicative.ofAdd
      (signBit (InfinitePlace.embedding_of_isReal w.property (x : K)))
  map_one' := by
    change Multiplicative.ofAdd
        (signBit (InfinitePlace.embedding_of_isReal w.property ((1 : Kˣ) : K))) =
        1
    rw [Units.val_one, map_one, signBit_of_pos one_pos, ofAdd_zero_eq_one]
  map_mul' := fun x y => by
    have hx : InfinitePlace.embedding_of_isReal w.property (x : K) ≠ 0 :=
      (map_ne_zero_iff _
        (RingHom.injective (InfinitePlace.embedding_of_isReal w.property))).mpr
        (Units.ne_zero x)
    have hy : InfinitePlace.embedding_of_isReal w.property (y : K) ≠ 0 :=
      (map_ne_zero_iff _
        (RingHom.injective (InfinitePlace.embedding_of_isReal w.property))).mpr
        (Units.ne_zero y)
    change Multiplicative.ofAdd
        (signBit
          (InfinitePlace.embedding_of_isReal w.property ((x * y : Kˣ) : K))) =
        Multiplicative.ofAdd
          (signBit (InfinitePlace.embedding_of_isReal w.property (x : K))) *
          Multiplicative.ofAdd
            (signBit (InfinitePlace.embedding_of_isReal w.property (y : K)))
    rw [Units.val_mul, map_mul, signBit_mul hx hy, ofAdd_add]

Used by 5

Used byInfinite sign map of a modulus · Coordinates of the infinite sign map · Trivial infinite sign means positivity at the modulus · Surjectivity of the residue-sign map · Trivial sign at a real place means positivity

TheoremTrivial sign at a real place means positivity#✓fully proved

Let \(w\) be a real place of a number field \(K\) with real embedding \(\sigma_w \colon K \to \mathbb{R}\). For every \(x \in K^\times\), the sign of \(x\) at \(w\), an element of \(\mathbb{Z}/2\mathbb{Z}\) written multiplicatively, is the identity if and only if \(\sigma_w(x) > 0\).

@[simp] theorem signAtRealPlace_apply_eq_one_iff (w : RealPlace K) (x : Kˣ) :
    signAtRealPlace w x = 1 ↔
      0 < InfinitePlace.embedding_of_isReal w.property (x : K)

Uses 1 · Used by 2

Statement usesSign of a unit at a real place

Used byTrivial infinite sign means positivity at the modulus · Surjectivity of the residue-sign map

DefinitionInfinite sign map of a modulus#✓fully proved

Let \(m\) be a modulus of a number field \(K\) and let \(m_\infty\) be its finite set of real places. The infinite sign map of \(m\) is the group homomorphism from the ray elements of \(m\) to the group of functions \(m_\infty \to \mathbb{Z}/2\mathbb{Z}\), with \(\mathbb{Z}/2\mathbb{Z}\) written multiplicatively and the pointwise product, that sends \(x\) to the function whose value at \(w \in m_\infty\) is the sign of \(x\) at the real place \(w\).

noncomputable def infiniteSignMap (m : Modulus K) :
    rayElements m →* (m.infinitePart → Multiplicative (ZMod 2)) where
  toFun x := fun w => signAtRealPlace (w : RealPlace K) (x : Kˣ)
  map_one' := by
    funext w
    change signAtRealPlace (w : RealPlace K) ((1 : rayElements m) : Kˣ) = 1
    rw [show ((1 : rayElements m) : Kˣ) = (1 : Kˣ) from rfl, map_one]
  map_mul' := fun x y => by
    funext w
    change signAtRealPlace (w : RealPlace K) ((x * y : rayElements m) : Kˣ) =
      signAtRealPlace (w : RealPlace K) (x : Kˣ) *
        signAtRealPlace (w : RealPlace K) (y : Kˣ)
    rw [show ((x * y : rayElements m) : Kˣ) = (x : Kˣ) * (y : Kˣ) from rfl,
      map_mul]

Uses 2 · Used by 8

Statement usesElements coprime to a modulus · Sign of a unit at a real place

Used byCoordinates of the infinite sign map · Trivial infinite sign means positivity at the modulus · Membership in the positive ray elements · Ray elements positive at the infinite part · Residue-sign map · Components of the residue-sign map · Kernel of the residue-sign map · Surjectivity of the residue-sign map

TheoremCoordinates of the infinite sign map#✓fully proved

Let \(m\) be a modulus of a number field \(K\) with finite set of real places \(m_\infty\). For every ray element \(x\) of \(m\) and every \(w \in m_\infty\), the value at \(w\) of the infinite sign map of \(m\) applied to \(x\) is the sign of \(x\) at the real place \(w\).

@[simp] theorem infiniteSignMap_apply (m : Modulus K) (x : rayElements m)
    (w : m.infinitePart) :
    infiniteSignMap m x w = signAtRealPlace (w : RealPlace K) (x : Kˣ)

Uses 3 · Used by 2

Statement usesInfinite sign map of a modulus · Elements coprime to a modulus · Sign of a unit at a real place

Used byTrivial infinite sign means positivity at the modulus · Surjectivity of the residue-sign map

TheoremTrivial infinite sign means positivity at the modulus#✓fully proved

Let \(m\) be a modulus of a number field \(K\) with finite set of real places \(m_\infty\), and for a real place \(w\) let \(\sigma_w\) be the corresponding real embedding of \(K\). For every ray element \(x\) of \(m\), the infinite sign map of \(m\) sends \(x\) to the identity if and only if \(x\) is positive at the infinite part of \(m\), that is, \(\sigma_w(x) > 0\) for every \(w \in m_\infty\).

@[simp] theorem infiniteSignMap_eq_one_iff (m : Modulus K) (x : rayElements m) :
    infiniteSignMap m x = 1 ↔ PositiveAtInfinitePart m (x : Kˣ)

Uses 6 · Used by 1

Statement usesPositivity at the infinite part of a modulus · Infinite sign map of a modulus · Elements coprime to a modulus

Proof usesCoordinates of the infinite sign map · Sign of a unit at a real place · Trivial sign at a real place means positivity

Used byMembership in the positive ray elements

DefinitionRay elements positive at the infinite part#✓fully proved

Let \(m\) be a modulus of a number field \(K\) with finite set of real places \(m_\infty\), and for a real place \(w\) let \(\sigma_w\) be the real embedding of \(K\) at \(w\). The positive ray elements of \(m\) form the subgroup of the ray elements of \(m\) defined as the kernel of the infinite sign map of \(m\); equivalently, they are the ray elements \(x\) with \(\sigma_w(x) > 0\) for every \(w \in m_\infty\).

def positiveRayElements (m : Modulus K) : Subgroup (rayElements m) :=
  (infiniteSignMap m).ker

Uses 2 · Used by 4

Statement usesInfinite sign map of a modulus · Elements coprime to a modulus

Used byMembership in the positive ray elements · Membership in the ray-one subgroup · Ray-one subgroup · Kernel of the residue-sign map

TheoremMembership in the positive ray elements#✓fully proved

Let \(m\) be a modulus of a number field \(K\) with finite set of real places \(m_\infty\), and for a real place \(w\) let \(\sigma_w\) be the real embedding of \(K\) at \(w\). A ray element \(x\) of \(m\) is a positive ray element of \(m\) if and only if \(x\) is positive at the infinite part of \(m\), that is, \(\sigma_w(x) > 0\) for every \(w \in m_\infty\).

@[simp] theorem mem_positiveRayElements_iff (m : Modulus K) (x : rayElements m) :
    x ∈ positiveRayElements m ↔ PositiveAtInfinitePart m (x : Kˣ)

Uses 5 · Used by 1

Statement usesPositivity at the infinite part of a modulus · Ray elements positive at the infinite part · Elements coprime to a modulus

Proof usesInfinite sign map of a modulus · Trivial infinite sign means positivity at the modulus

Used byMembership in the ray-one subgroup

TheoremWeak approximation with a finite target and prescribed signs#✓fully proved

Let \(K\) be a number field and \(\mathfrak m\) a modulus of \(K\), with finite part \(\mathfrak m_0\) (a nonzero ideal of \(\mathcal O_K\)) and infinite part \(\mathfrak m_\infty\) (a finite set of real places of \(K\)). For a nonzero prime \(\mathfrak p\) of \(\mathcal O_K\) write \(v_{\mathfrak p}\) for the \(\mathfrak p\)-adic valuation on \(K\) (with \(v_{\mathfrak p}(0) = \infty\)) and \(e_{\mathfrak p}\) for the exponent of \(\mathfrak p\) in \(\mathfrak m_0\); for a real place \(w\) write \(\sigma_w : K \to \mathbb R\) for its real embedding. Let \(P\) be any set of places in \(\mathfrak m_\infty\), and let \(a \in K\) be nonzero with \(v_{\mathfrak p}(a) = 0\) for every nonzero prime \(\mathfrak p\) dividing \(\mathfrak m_0\). Then there is a nonzero \(x \in K\) such that \(v_{\mathfrak p}(x) = 0\) and \(v_{\mathfrak p}(x - a) \ge e_{\mathfrak p}\) for every nonzero prime \(\mathfrak p\) dividing \(\mathfrak m_0\), and such that for every \(w \in \mathfrak m_\infty\), \(\sigma_w(x) > 0\) if \(w \in P\) and \(\sigma_w(x) < 0\) if \(w \notin P\).

theorem exists_ne_zero_with_target_and_sign
    (m : Modulus K) (a : K)
    (pos : {w : RealPlace K // w ∈ m.infinitePart} → Prop)
    (ha0 : a ≠ 0)
    (haval : ∀ v : IsDedekindDomain.HeightOneSpectrum (𝓞 K),
      finiteSupported m v → v.valuation K a = 1) :
    ∃ x : K, x ≠ 0 ∧
      (∀ v : IsDedekindDomain.HeightOneSpectrum (𝓞 K),
        finiteSupported m v →
          v.valuation K x = 1 ∧
          v.valuation K (x - a) ≤ WithZero.exp (-(finiteExponent m v))) ∧
      ∀ (w : RealPlace K) (hw : w ∈ m.infinitePart),
        (pos ⟨w, hw⟩ → 0 < InfinitePlace.embedding_of_isReal w.property x) ∧
        (¬ pos ⟨w, hw⟩ → InfinitePlace.embedding_of_isReal w.property x < 0)

Sources

• mapping toward ATLAS N406, Theorem 21.8, Section 21.3 (weak_approx_coprime_sign_finitePart, lines 2255--2568): the finite target a is lifted at source lines 2267--2275 with supported valuation-one hypothesis at 2277--2292; the finite/infinite index family below is at 2314--2385; modulus-dependent tolerances at 2388--2404; nonzero witness at 2406--2412; valuation preservation at 2414--2451; sign control at 2458--2477; and the strict absolute-value-to-discrete-valuation residue comparison at 2480--2568.

Uses 2 · Used by 2

Statement usesExponent of a modulus at a prime · Primes dividing a modulus

Used byWeak approximation with prescribed signs at a modulus · Surjectivity of the residue-sign map

TheoremWeak approximation with prescribed signs at a modulus#✓fully proved

Let \(K\) be a number field and \(\mathfrak m\) a modulus of \(K\), with finite part \(\mathfrak m_0\) (a nonzero ideal of \(\mathcal O_K\)) and infinite part \(\mathfrak m_\infty\) (a finite set of real places of \(K\)); for a real place \(w\) write \(\sigma_w : K \to \mathbb R\) for its real embedding. For every set \(P\) of places in \(\mathfrak m_\infty\) there is a nonzero \(x \in K\) whose \(\mathfrak p\)-adic valuation is \(0\) for every nonzero prime \(\mathfrak p\) of \(\mathcal O_K\) dividing \(\mathfrak m_0\), and such that for every \(w \in \mathfrak m_\infty\), \(\sigma_w(x) > 0\) if \(w \in P\) and \(\sigma_w(x) < 0\) if \(w \notin P\).

This is the special case of weak approximation with a finite target and prescribed signs in which the target is \(1\).

theorem exists_ne_zero_with_valuation_one_and_sign
    (m : Modulus K)
    (pos : {w : RealPlace K // w ∈ m.infinitePart} → Prop) :
    ∃ x : K, x ≠ 0 ∧
      (∀ v : IsDedekindDomain.HeightOneSpectrum (𝓞 K),
        finiteSupported m v → v.valuation K x = 1) ∧
      ∀ (w : RealPlace K) (hw : w ∈ m.infinitePart),
        (pos ⟨w, hw⟩ → 0 < InfinitePlace.embedding_of_isReal w.property x) ∧
        (¬ pos ⟨w, hw⟩ → InfinitePlace.embedding_of_isReal w.property x < 0)

Uses 3

Statement usesPrimes dividing a modulus

Proof usesWeak approximation with a finite target and prescribed signs · Exponent of a modulus at a prime

AbbreviationResidue-sign target#✓fully proved

Let \(m\) be a modulus of a number field \(K\), with finite part the nonzero ideal \(\mathfrak{m}_0\) of the ring of integers \(\mathcal{O}_K\) and infinite part the finite set \(S\) of real places of \(K\). Let \(G\) denote \(\mathbb{Z}/2\mathbb{Z}\) written multiplicatively, let \(G^S\) denote the group of functions from \(S\) to \(G\) (one sign for each place in \(S\)), and let \((\mathcal{O}_K/\mathfrak{m}_0)^\times\) denote the unit group of the quotient ring \(\mathcal{O}_K/\mathfrak{m}_0\). The residue-sign target of \(m\) is the product group \(G^S \times (\mathcal{O}_K/\mathfrak{m}_0)^\times\).

abbrev ResidueSignTarget (m : Modulus K) :=
  (m.infinitePart → Multiplicative (ZMod 2)) ×
    (𝓞 K ⧸ (m.finitePart : Ideal (𝓞 K)))ˣ

Used by 20

Used byExactness at the integral units, residue-sign form · Residue-sign map on integral units · Value of the residue-sign map on integral units · Kernel of the residue-sign map on integral units · Exactness at the residue-sign group · The ray class exact sequence, sign and residue form · Projecting the image of a residue-sign value to the class group · The residue-sign isomorphism · The residue-sign isomorphism on classes · Residue-sign map · Components of the residue-sign map · Kernel criterion for the residue-sign map · Kernel of the residue-sign map · Surjectivity of the residue-sign map · Ray class map on residues and signs · The residue-sign transport square commutes · Residue-sign-to-ray-class map through the quotient isomorphism · Kernel of the ray class map on residue-sign values · Exactness at the ray class group, residue-sign form · Ray class map on residue-sign values

DefinitionResidue-sign map#✓fully proved

Let \(m\) be a modulus of a number field \(K\). The residue-sign map of \(m\) is the group homomorphism from the ray elements of \(m\) to the residue-sign target of \(m\) that sends a ray element \(x\) to the pair formed by the image of \(x\) under the infinite sign map of \(m\) and the image of \(x\) under the finite residue map of \(m\).

noncomputable def residueSignMap (m : Modulus K) :
    rayElements m →* ResidueSignTarget m :=
  (infiniteSignMap m).prod (finiteResidueMap m)

Uses 4 · Used by 10

Statement usesResidue-sign target · Finite residue map · Infinite sign map of a modulus · Elements coprime to a modulus

Used byValue of the residue-sign map on integral units · Projecting the image of a residue-sign value to the class group · The residue-sign isomorphism · The residue-sign isomorphism on classes · Components of the residue-sign map · Kernel criterion for the residue-sign map · Kernel of the residue-sign map · Surjectivity of the residue-sign map · The residue-sign transport square commutes · Ray class map on residue-sign values

TheoremComponents of the residue-sign map#✓fully proved

Let \(m\) be a modulus of a number field \(K\). For every ray element \(x\) of \(m\), the image of \(x\) under the residue-sign map of \(m\) is the pair whose first component is the image of \(x\) under the infinite sign map of \(m\) and whose second component is the image of \(x\) under the finite residue map of \(m\).

@[simp] theorem residueSignMap_apply (m : Modulus K) (x : rayElements m) :
    residueSignMap m x = (infiniteSignMap m x, finiteResidueMap m x)

Uses 5 · Used by 1

Statement usesResidue-sign target · Finite residue map · Infinite sign map of a modulus · Elements coprime to a modulus · Residue-sign map

Used bySurjectivity of the residue-sign map

DefinitionRay-one subgroup#✓fully proved

Let \(m\) be a modulus of a number field \(K\). The ray-one subgroup of \(m\) is the subgroup of the ray elements of \(m\) consisting of the ray elements \(x\) that lie in the finite ray-one subgroup of \(m\) (those congruent to \(1\) at the finite part of \(m\)) and in the subgroup of ray elements positive at every real place in the infinite part of \(m\).

def rayOneElements (m : Modulus K) : Subgroup (rayElements m) :=
  finiteRayOneElements m ⊓ positiveRayElements m

Uses 3 · Used by 30

Statement usesThe finite ray-one subgroup · Ray elements positive at the infinite part · Elements coprime to a modulus

Used byRay-one integral units · Exactness of the ray sequence at the integral units · Map from integral units to the ray quotient · Value of the ray-quotient map on integral units · Kernel of the ray-quotient map on integral units · Exactness at the ray-element quotient · Residue-sign map on integral units · Value of the residue-sign map on integral units · Kernel of the residue-sign map on integral units · Membership in the ray-one integral units · Membership in the ray-one subgroup · The ray class exact sequence · Kernel of the projection from the ray class group to the class group · Projecting the image of a ray element to the class group · The residue-sign isomorphism · The residue-sign isomorphism on classes · The ray group is the image of the ray-one elements · The ray group lies in the kernel of the ideal-class map · Ray-one elements have trivial ray class · Quotient-to-ray-class map · Exactness at the ray-element quotient (kernel form) · Quotient-to-ray-class map on representatives · Exactness at the ray class group · Kernel criterion for the residue-sign map · Kernel of the residue-sign map · Ray class map on residues and signs · Residue-sign-to-ray-class map through the quotient isomorphism · Kernel of the ray class map on residue-sign values · Exactness at the ray class group, residue-sign form · Ray class map on residue-sign values

TheoremMembership in the ray-one subgroup#✓fully proved

Let \(m\) be a modulus of a number field \(K\). A ray element \(x\) of \(m\) lies in the ray-one subgroup of \(m\) if and only if \(x\) is congruent to \(1\) at the finite part of \(m\) and \(x\) is positive at every real place in the infinite part of \(m\).

@[simp] theorem mem_rayOneElements_iff (m : Modulus K) (x : rayElements m) :
    x ∈ rayOneElements m ↔
      CongruentOneAtFinitePart m (x : Kˣ) ∧
        PositiveAtInfinitePart m (x : Kˣ)

Uses 7 · Used by 3

Statement usesMultiplicative congruence to one at the finite part · Positivity at the infinite part of a modulus · Elements coprime to a modulus · Ray-one subgroup

Proof usesThe finite ray-one subgroup · Membership in the positive ray elements · Ray elements positive at the infinite part

Used byMembership in the ray-one integral units · The ray group is the image of the ray-one elements · Kernel criterion for the residue-sign map

TheoremSurjectivity of the residue-sign map#✓fully proved

Let \(m\) be a modulus of a number field \(K\). Every element of the residue-sign target of \(m\) is the image of some ray element of \(m\) under the residue-sign map of \(m\).

theorem residueSignMap_surjective (m : Modulus K) :
    Function.Surjective (residueSignMap m)

Uses 15 · Used by 2

Statement usesResidue-sign target · Elements coprime to a modulus · Residue-sign map

Proof usesWeak approximation with a finite target and prescribed signs · Exponent of a modulus at a prime · Finite residue map · Computing the finite residue map from a representation · Valuation criterion for the finite residue map to be trivial · Primes dividing a modulus · Infinite sign map of a modulus · Coordinates of the infinite sign map · Elements of valuation one at the primes dividing a modulus are ray elements · Components of the residue-sign map · Sign of a unit at a real place · Trivial sign at a real place means positivity

Used byThe residue-sign isomorphism · The residue-sign isomorphism on classes

TheoremKernel of the residue-sign map#✓fully proved

Let \(m\) be a modulus of a number field \(K\). The kernel of the residue-sign map of \(m\) is the ray-one subgroup of \(m\).

@[simp] theorem residueSignMap_ker (m : Modulus K) :
    (residueSignMap m).ker = rayOneElements m

Uses 9 · Used by 2

Statement usesResidue-sign target · Elements coprime to a modulus · Ray-one subgroup · Residue-sign map

Proof usesThe finite ray-one subgroup · Finite residue map · Kernel of the finite residue map · Infinite sign map of a modulus · Ray elements positive at the infinite part

Used byThe residue-sign isomorphism · Kernel criterion for the residue-sign map

TheoremKernel criterion for the residue-sign map#✓fully proved

Let \(m\) be a modulus of a number field \(K\). A ray element \(x\) of \(m\) is sent to \(1\) by the residue-sign map of \(m\) if and only if \(x\) is a ray element congruent to \(1\) modulo \(m\): \(x\) is a ray element of \(m\), \(x\) is congruent to \(1\) at the finite part of \(m\), and \(x\) is positive at every real place in the infinite part of \(m\).

theorem residueSignMap_eq_one_iff (m : Modulus K) (x : rayElements m) :
    residueSignMap m x = 1 ↔ IsRayElementOne m (x : Kˣ)

Uses 9

Statement usesElements congruent to one modulo a modulus · Residue-sign target · Elements coprime to a modulus · Residue-sign map

Proof usesMultiplicative congruence to one at the finite part · Positivity at the infinite part of a modulus · Membership in the ray-one subgroup · Ray-one subgroup · Kernel of the residue-sign map

DefinitionThe residue-sign isomorphism#✓fully proved

Let \(m\) be a modulus of a number field \(K\). The residue-sign isomorphism of \(m\) is the group isomorphism from the quotient of the ray elements of \(m\) by the ray-one subgroup of \(m\) onto the residue-sign target of \(m\) induced by the residue-sign map, which is surjective with kernel the ray-one subgroup; it sends the class of a ray element \(x\) to the image of \(x\) under the residue-sign map.

noncomputable def rayElementsQuotientEquivResidueSign (m : Modulus K) :
    (rayElements m ⧸ rayOneElements m) ≃* ResidueSignTarget m := by
  haveI : (rayOneElements m).Normal :=
    residueSignMap_ker m ▸ (residueSignMap m).normal_ker
  exact (QuotientGroup.quotientMulEquivOfEq (residueSignMap_ker m).symm).trans
    (QuotientGroup.quotientKerEquivOfSurjective _ (residueSignMap_surjective m))

Uses 6 · Used by 9

Statement usesResidue-sign target · Elements coprime to a modulus · Ray-one subgroup · Residue-sign map · Kernel of the residue-sign map · Surjectivity of the residue-sign map

Used byResidue-sign map on integral units · Value of the residue-sign map on integral units · Kernel of the residue-sign map on integral units · The residue-sign isomorphism on classes · Ray class map on residues and signs · Residue-sign-to-ray-class map through the quotient isomorphism · Kernel of the ray class map on residue-sign values · Exactness at the ray class group, residue-sign form · Ray class map on residue-sign values

TheoremThe residue-sign isomorphism on classes#✓fully proved

Let \(m\) be a modulus of a number field \(K\). For every ray element \(x\) of \(m\), the residue-sign isomorphism of \(m\) sends the class of \(x\) in the quotient of the ray elements of \(m\) by the ray-one subgroup to the image of \(x\) under the residue-sign map of \(m\).

@[simp] theorem rayElementsQuotientEquivResidueSign_mk (m : Modulus K)
    (x : rayElements m) :
    rayElementsQuotientEquivResidueSign m (QuotientGroup.mk x) =
      residueSignMap m x

Uses 6 · Used by 2

Statement usesResidue-sign target · Elements coprime to a modulus · The residue-sign isomorphism · Ray-one subgroup · Residue-sign map

Proof usesSurjectivity of the residue-sign map

Used byValue of the residue-sign map on integral units · Ray class map on residue-sign values

DefinitionEmbedding of integral units into field units#✓fully proved

Let \(K\) be a field and \(\mathcal{O}_K\) its ring of integers, the integral closure of \(\mathbb{Z}\) in \(K\). This is the group homomorphism \(\mathcal{O}_K^\times \to K^\times\) induced by the inclusion \(\mathcal{O}_K \subseteq K\): it sends a unit of \(\mathcal{O}_K\) to the same element regarded as a unit of \(K\).

def integralUnitsToFieldUnits : (𝓞 K)ˣ →* Kˣ :=
  Units.map (algebraMap (𝓞 K) K).toMonoidHom

Sources

• ATLAS okUnitsToKUnits.

Used by 5

Used byIntegral units embed injectively into field units · Integral units as ray elements · Ray-element image of an integral unit as a field unit · Integral units embed injectively into the ray elements · Integral units generate the unit ideal

TheoremIntegral units embed injectively into field units#✓fully proved

Let \(K\) be a field and \(\mathcal{O}_K\) its ring of integers, the integral closure of \(\mathbb{Z}\) in \(K\). The group homomorphism \(\mathcal{O}_K^\times \to K^\times\) induced by the inclusion \(\mathcal{O}_K \subseteq K\) is injective.

theorem integralUnitsToFieldUnits_injective :
    Function.Injective (integralUnitsToFieldUnits (K := K))

Uses 1 · Used by 1

Statement usesEmbedding of integral units into field units

Used byIntegral units embed injectively into the ray elements

DefinitionIntegral units as ray elements#✓fully proved

Let \(K\) be a number field with ring of integers \(\mathcal{O}_K\), let \(\mathfrak{m}\) be a modulus of \(K\), and let \(K_{\mathfrak{m}} \subseteq K^\times\) be the group of ray elements for \(\mathfrak{m}\). Every unit of \(\mathcal{O}_K\) has \(\mathfrak{p}\)-adic valuation \(0\) at every prime \(\mathfrak{p}\) of \(\mathcal{O}_K\), so it lies in \(K_{\mathfrak{m}}\). This is the group homomorphism \(\mathcal{O}_K^\times \to K_{\mathfrak{m}}\) sending a unit \(u\) to its image in \(K^\times\).

def integralUnitsToRayElements (m : Modulus K) :
    (𝓞 K)ˣ →* rayElements m :=
  MonoidHom.codRestrict integralUnitsToFieldUnits (rayElements m)
    (fun u => mem_rayElements_of_valuation_eq_one m
      (integralUnitsToFieldUnits u) (fun v _ =>
        (v.valuation_eq_one_iff_notMem).2 (v.asIdeal.notMem_of_isUnit u.isUnit)))

Sources

• ATLAS okUnitsToUnitsCoprime; ATLAS valuation_algebraMap_unit_eq_one is discharged inline in the definition.

Uses 4 · Used by 10

Statement usesPrimes dividing a modulus · Embedding of integral units into field units · Elements of valuation one at the primes dividing a modulus are ray elements · Elements coprime to a modulus

Used byRay-one integral units · Ray-element image of an integral unit as a field unit · Integral units embed injectively into the ray elements · Map from integral units to the ray quotient · Value of the ray-quotient map on integral units · Kernel of the ray-quotient map on integral units · Value of the residue-sign map on integral units · Membership in the ray-one integral units · Integral units generate the unit ideal · Exactness at the ray-element quotient (kernel form)

TheoremRay-element image of an integral unit as a field unit#✓fully proved

Let \(K\) be a number field with ring of integers \(\mathcal{O}_K\), let \(\mathfrak{m}\) be a modulus of \(K\), and let \(u \in \mathcal{O}_K^\times\). The image of \(u\) in the group of ray elements for \(\mathfrak{m}\), regarded as an element of \(K^\times\), equals the image of \(u\) under the embedding \(\mathcal{O}_K^\times \to K^\times\).

@[simp] theorem integralUnitsToRayElements_coe (m : Modulus K) (u : (𝓞 K)ˣ) :
    ((integralUnitsToRayElements m u : rayElements m) : Kˣ) =
      integralUnitsToFieldUnits u

Uses 3

Statement usesEmbedding of integral units into field units · Integral units as ray elements · Elements coprime to a modulus

TheoremIntegral units embed injectively into the ray elements#✓fully proved

Let \(K\) be a number field with ring of integers \(\mathcal{O}_K\) and let \(\mathfrak{m}\) be a modulus of \(K\). The homomorphism from \(\mathcal{O}_K^\times\) to the group of ray elements for \(\mathfrak{m}\) that sends a unit to its image in \(K^\times\) is injective.

theorem integralUnitsToRayElements_injective (m : Modulus K) :
    Function.Injective (integralUnitsToRayElements m)

Uses 6

Statement usesIntegral units as ray elements · Elements coprime to a modulus

Proof usesPrimes dividing a modulus · Embedding of integral units into field units · Integral units embed injectively into field units · Elements of valuation one at the primes dividing a modulus are ray elements

DefinitionRay-one integral units#✓fully proved

Let \(K\) be a number field with ring of integers \(\mathcal{O}_K\), let \(\mathfrak{m}\) be a modulus of \(K\) with finite part \(\mathfrak{m}_0\), and send each unit of \(\mathcal{O}_K\) to its image in the group of ray elements for \(\mathfrak{m}\). For a nonzero prime \(\mathfrak{p}\) of \(\mathcal{O}_K\), write \(v_{\mathfrak{p}}\) for the \(\mathfrak{p}\)-adic valuation of nonzero elements and nonzero ideals. The ray-one integral units for \(\mathfrak{m}\) form the subgroup of \(\mathcal{O}_K^\times\) of those units \(u\) whose image lies in the ray-one subgroup, that is: for every prime \(\mathfrak{p}\) dividing \(\mathfrak{m}_0\), either \(u = 1\) or \(v_{\mathfrak{p}}(u - 1) \ge v_{\mathfrak{p}}(\mathfrak{m}_0)\), and \(u\) is positive under the real embedding of every real place in the infinite part of \(\mathfrak{m}\).

def integralRayOneUnits (m : Modulus K) : Subgroup (𝓞 K)ˣ :=
  (rayOneElements m).comap (integralUnitsToRayElements m)

Sources

• ATLAS UnitsInCongruenceSubgroup.

Uses 3 · Used by 9

Statement usesIntegral units as ray elements · Elements coprime to a modulus · Ray-one subgroup

Used byInclusion of the ray-one integral units · The inclusion of the ray-one integral units is injective · Exactness of the ray sequence at the integral units · Exactness at the integral units, residue-sign form · Kernel of the ray-quotient map on integral units · Kernel of the residue-sign map on integral units · Membership in the ray-one integral units · The ray class exact sequence, sign and residue form · The ray class exact sequence

TheoremMembership in the ray-one integral units#✓fully proved

Let \(\mathfrak m\) be a modulus of a number field \(K\) with finite part \(\mathfrak m_0\) and set of real places \(\mathfrak m_\infty\), and for a nonzero prime \(\mathfrak p\) of the ring of integers \(\mathcal O_K\) write \(v_{\mathfrak p}\) for the exponent of \(\mathfrak p\) in a fractional ideal of \(K\), applied to an element through its principal fractional ideal. A unit \(u\) of \(\mathcal O_K\) lies in the subgroup of ray-one integral units if and only if \(u\), viewed as an element of \(K^\times\), is a ray element congruent to \(1\) modulo \(\mathfrak m\): its principal fractional ideal is coprime to \(\mathfrak m_0\), for every nonzero prime \(\mathfrak p\) dividing \(\mathfrak m_0\) either \(u = 1\) or \(v_{\mathfrak p}(u - 1) \ge v_{\mathfrak p}(\mathfrak m_0)\), and \(u\) is positive under the real embedding of every place in \(\mathfrak m_\infty\).

@[simp] theorem mem_integralRayOneUnits_iff (m : Modulus K) (u : (𝓞 K)ˣ) :
    u ∈ integralRayOneUnits m ↔
      IsRayElementOne m
        ((integralUnitsToRayElements m u : rayElements m) : Kˣ)

Uses 8

Statement usesElements congruent to one modulo a modulus · Ray-one integral units · Integral units as ray elements · Elements coprime to a modulus

Proof usesMultiplicative congruence to one at the finite part · Positivity at the infinite part of a modulus · Membership in the ray-one subgroup · Ray-one subgroup

DefinitionInclusion of the ray-one integral units#✓fully proved

Let \(K\) be a number field with ring of integers \(\mathcal{O}_K\) and let \(\mathfrak{m}\) be a modulus of \(K\). The inclusion of the ray-one integral units for \(\mathfrak{m}\) is the group homomorphism from the subgroup of ray-one integral units for \(\mathfrak{m}\) to \(\mathcal{O}_K^\times\) that sends each such unit to itself.

def integralRayOneUnitsInclusion (m : Modulus K) :
    integralRayOneUnits m →* (𝓞 K)ˣ :=
  (integralRayOneUnits m).subtype

Sources

• ATLAS exactSeq_map1.

Uses 1 · Used by 5

Statement usesRay-one integral units

Used byThe inclusion of the ray-one integral units is injective · Exactness of the ray sequence at the integral units · Exactness at the integral units, residue-sign form · The ray class exact sequence, sign and residue form · The ray class exact sequence

DefinitionMap from integral units to the ray quotient#✓fully proved

Let \(\mathfrak m\) be a modulus of a number field \(K\), let \(K_{\mathfrak m} \le K^\times\) be the group of ray elements (elements whose principal fractional ideal is coprime to the finite part of \(\mathfrak m\)) and let \(K_{\mathfrak m,1} \le K_{\mathfrak m}\) be the ray-one subgroup. This is the group homomorphism \(\mathcal O_K^\times \to K_{\mathfrak m}/K_{\mathfrak m,1}\) sending a unit \(u\) of the ring of integers \(\mathcal O_K\) to the coset of \(u\), viewed as an element of \(K_{\mathfrak m}\).

def integralUnitsToRayQuotient (m : Modulus K) :
    (𝓞 K)ˣ →* rayElements m ⧸ rayOneElements m :=
  (QuotientGroup.mk' (rayOneElements m)).comp (integralUnitsToRayElements m)

Sources

• ATLAS exactSeq_map2.

Uses 3 · Used by 10

Statement usesIntegral units as ray elements · Elements coprime to a modulus · Ray-one subgroup

Used byExactness of the ray sequence at the integral units · Value of the ray-quotient map on integral units · Kernel of the ray-quotient map on integral units · Exactness at the ray-element quotient · Residue-sign map on integral units · Value of the residue-sign map on integral units · Kernel of the residue-sign map on integral units · The ray class exact sequence · Exactness at the ray-element quotient (kernel form) · Kernel of the ray class map on residue-sign values

TheoremValue of the ray-quotient map on integral units#✓fully proved

Let \(\mathfrak m\) be a modulus of a number field \(K\), let \(K_{\mathfrak m} \le K^\times\) be the group of ray elements (elements whose principal fractional ideal is coprime to the finite part of \(\mathfrak m\)) and let \(K_{\mathfrak m,1} \le K_{\mathfrak m}\) be the ray-one subgroup. For every unit \(u\) of the ring of integers \(\mathcal O_K\), the map \(\mathcal O_K^\times \to K_{\mathfrak m}/K_{\mathfrak m,1}\) sends \(u\) to the coset of \(u\), viewed as an element of \(K_{\mathfrak m}\).

@[simp] theorem integralUnitsToRayQuotient_apply (m : Modulus K) (u : (𝓞 K)ˣ) :
    integralUnitsToRayQuotient m u =
      QuotientGroup.mk (integralUnitsToRayElements m u)

Uses 4 · Used by 2

Statement usesIntegral units as ray elements · Map from integral units to the ray quotient · Elements coprime to a modulus · Ray-one subgroup

Used byValue of the residue-sign map on integral units · Exactness at the ray-element quotient (kernel form)

DefinitionResidue-sign map on integral units#✓fully proved

Let \(\mathfrak m\) be a modulus of a number field \(K\) with finite part \(\mathfrak m_0\) and set of real places \(\mathfrak m_\infty\), let \(K_{\mathfrak m} \le K^\times\) be the group of ray elements and let \(K_{\mathfrak m,1} \le K_{\mathfrak m}\) be the ray-one subgroup. The residue-sign map on integral units is the group homomorphism from \(\mathcal O_K^\times\) to \((\mathbb Z/2\mathbb Z)^{\mathfrak m_\infty} \times (\mathcal O_K/\mathfrak m_0)^\times\), with \(\mathbb Z/2\mathbb Z\) written multiplicatively, obtained by composing the map \(\mathcal O_K^\times \to K_{\mathfrak m}/K_{\mathfrak m,1}\) sending a unit to its coset with the isomorphism from \(K_{\mathfrak m}/K_{\mathfrak m,1}\) onto this group induced by the residue-sign homomorphism on \(K_{\mathfrak m}\).

noncomputable def integralUnitsToResidueSign (m : Modulus K) :
    (𝓞 K)ˣ →* ResidueSignTarget m :=
  (rayElementsQuotientEquivResidueSign m).toMonoidHom.comp
    (integralUnitsToRayQuotient m)

Uses 5 · Used by 6

Statement usesResidue-sign target · Map from integral units to the ray quotient · Elements coprime to a modulus · The residue-sign isomorphism · Ray-one subgroup

Used byExactness at the integral units, residue-sign form · Value of the residue-sign map on integral units · Kernel of the residue-sign map on integral units · Exactness at the residue-sign group · The ray class exact sequence, sign and residue form · Kernel of the ray class map on residue-sign values

TheoremValue of the residue-sign map on integral units#✓fully proved

Let \(\mathfrak m\) be a modulus of a number field \(K\) and let \(K_{\mathfrak m} \le K^\times\) be the group of ray elements. For every unit \(u\) of the ring of integers \(\mathcal O_K\), the residue-sign map on integral units sends \(u\) to the image of \(u\), viewed as an element of \(K_{\mathfrak m}\), under the residue-sign homomorphism on \(K_{\mathfrak m}\).

@[simp] theorem integralUnitsToResidueSign_apply (m : Modulus K) (u : (𝓞 K)ˣ) :
    integralUnitsToResidueSign m u =
      residueSignMap m (integralUnitsToRayElements m u)

Uses 10

Statement usesResidue-sign target · Integral units as ray elements · Residue-sign map on integral units · Elements coprime to a modulus · Residue-sign map

Proof usesMap from integral units to the ray quotient · Value of the ray-quotient map on integral units · The residue-sign isomorphism · The residue-sign isomorphism on classes · Ray-one subgroup

TheoremKernel of the ray-quotient map on integral units#✓fully proved

Let \(\mathfrak m\) be a modulus of a number field \(K\), let \(K_{\mathfrak m} \le K^\times\) be the group of ray elements and \(K_{\mathfrak m,1} \le K_{\mathfrak m}\) the ray-one subgroup. The kernel of the homomorphism \(\mathcal O_K^\times \to K_{\mathfrak m}/K_{\mathfrak m,1}\) sending a unit of the ring of integers \(\mathcal O_K\) to its coset is the subgroup of ray-one integral units, the units of \(\mathcal O_K\) that lie in \(K_{\mathfrak m,1}\).

@[simp] theorem integralUnitsToRayQuotient_ker (m : Modulus K) :
    (integralUnitsToRayQuotient m).ker = integralRayOneUnits m

Uses 5 · Used by 2

Statement usesRay-one integral units · Map from integral units to the ray quotient · Elements coprime to a modulus · Ray-one subgroup

Proof usesIntegral units as ray elements

Used byExactness of the ray sequence at the integral units · Kernel of the residue-sign map on integral units

TheoremKernel of the residue-sign map on integral units#✓fully proved

Let \(\mathfrak m\) be a modulus of a number field \(K\). The kernel of the residue-sign map on the unit group \(\mathcal O_K^\times\) of the ring of integers is the subgroup of ray-one integral units, the units of \(\mathcal O_K\) whose image in the group of ray elements modulo \(\mathfrak m\) lies in its ray-one subgroup.

@[simp] theorem integralUnitsToResidueSign_ker (m : Modulus K) :
    (integralUnitsToResidueSign m).ker = integralRayOneUnits m

Uses 8 · Used by 1

Statement usesResidue-sign target · Ray-one integral units · Residue-sign map on integral units

Proof usesMap from integral units to the ray quotient · Kernel of the ray-quotient map on integral units · Elements coprime to a modulus · The residue-sign isomorphism · Ray-one subgroup

Used byExactness at the integral units, residue-sign form

TheoremThe inclusion of the ray-one integral units is injective#✓fully proved

Let \(K\) be a number field with ring of integers \(\mathcal{O}_K\) and let \(\mathfrak{m}\) be a modulus of \(K\). The inclusion homomorphism from the subgroup of ray-one integral units for \(\mathfrak{m}\) into the unit group \(\mathcal{O}_K^\times\) is injective.

theorem integralRayOneUnitsInclusion_injective (m : Modulus K) :
    Function.Injective (integralRayOneUnitsInclusion m)

Uses 2 · Used by 2

Statement usesRay-one integral units · Inclusion of the ray-one integral units

Used byThe ray class exact sequence, sign and residue form · The ray class exact sequence

TheoremExactness of the ray sequence at the integral units#✓fully proved

Let \(K\) be a number field with ring of integers \(\mathcal{O}_K\) and let \(\mathfrak{m}\) be a modulus of \(K\). Write \(K_{\mathfrak{m}}\) for the group of ray elements for \(\mathfrak{m}\), \(K_{\mathfrak{m},1}\) for its ray-one subgroup, and \(U_{\mathfrak{m},1} \subseteq \mathcal{O}_K^\times\) for the subgroup of ray-one integral units. Consider the sequence

\[U_{\mathfrak{m},1} \to \mathcal{O}_K^\times \to K_{\mathfrak{m}}/K_{\mathfrak{m},1}\]

whose first map is the inclusion and whose second map sends a unit to the class of its image in \(K_{\mathfrak{m}}\). For every \(u \in \mathcal{O}_K^\times\), the class of \(u\) is the identity if and only if \(u\) lies in the image of the first map; that is, the sequence is exact at \(\mathcal{O}_K^\times\).

theorem integralUnits_mulExact_quotient (m : Modulus K) :
    Function.MulExact (integralRayOneUnitsInclusion m)
      (integralUnitsToRayQuotient m)

Sources

• ATLAS exactSeq_exact_at_units.

Uses 6 · Used by 1

Statement usesRay-one integral units · Inclusion of the ray-one integral units · Map from integral units to the ray quotient · Elements coprime to a modulus · Ray-one subgroup

Proof usesKernel of the ray-quotient map on integral units

Used byThe ray class exact sequence

TheoremExactness at the integral units, residue-sign form#✓fully proved

Let \(K\) be a number field with ring of integers \(\mathcal{O}_K\) and let \(\mathfrak{m}\) be a modulus of \(K\) with finite part \(\mathfrak{m}_0\). Let \(T_{\mathfrak{m}}\) be the residue-sign target of \(\mathfrak{m}\): the product of a copy of \(\mathbb{Z}/2\mathbb{Z}\), written multiplicatively, for each real place in the infinite part of \(\mathfrak{m}\), with \((\mathcal{O}_K/\mathfrak{m}_0)^\times\). Let \(\rho \colon \mathcal{O}_K^\times \to T_{\mathfrak{m}}\) send a unit to the class of its image in the quotient of the group of ray elements for \(\mathfrak{m}\) by its ray-one subgroup, followed by the canonical isomorphism of that quotient with \(T_{\mathfrak{m}}\) induced by the residue-sign map. Then for every \(u \in \mathcal{O}_K^\times\), \(\rho(u) = 1\) if and only if \(u\) is in the image of the inclusion of the ray-one integral units for \(\mathfrak{m}\) into \(\mathcal{O}_K^\times\).

theorem integralUnits_mulExact_residueSign (m : Modulus K) :
    Function.MulExact (integralRayOneUnitsInclusion m)
      (integralUnitsToResidueSign m)

Uses 5 · Used by 1

Statement usesResidue-sign target · Ray-one integral units · Inclusion of the ray-one integral units · Residue-sign map on integral units

Proof usesKernel of the residue-sign map on integral units

Used byThe ray class exact sequence, sign and residue form

DefinitionPrincipal ray ideal map#✓fully proved

Let \(\mathfrak m\) be a modulus of a number field \(K\) with ring of integers \(\mathcal O_K\). The principal ray ideal map is the group homomorphism from the group of ray elements for \(\mathfrak m\) (the \(x \in K^\times\) whose principal ideal is coprime to \(\mathfrak m\)) to the group of fractional ideals coprime to \(\mathfrak m\) that sends \(x\) to the principal fractional ideal \(x\mathcal O_K\).

noncomputable def principalRayIdealMap (m : Modulus K) :
    rayElements m →* coprimeFractionalIdeals m :=
  ((toPrincipalIdeal (𝓞 K) K).domRestrict (rayElements m)).codRestrict
    (coprimeFractionalIdeals m)
    (fun x => (mem_rayElements_iff m _).mp x.property)

Uses 2 · Used by 12

Statement usesFractional ideals coprime to a modulus · Elements coprime to a modulus

Used byValue of the principal ray ideal map · Integral units generate the unit ideal · Kernel of the projection from the ray class group to the class group · Projecting the image of a ray element to the class group · Projecting the image of a residue-sign value to the class group · Ray-element class map · Value of the ray-element class map · The ray group is the image of the ray-one elements · The ray group lies in the kernel of the ideal-class map · Ray-one elements have trivial ray class · Exactness at the ray-element quotient (kernel form) · Quotient-to-ray-class map on representatives

TheoremValue of the principal ray ideal map#✓fully proved

Let \(\mathfrak m\) be a modulus of a number field \(K\) with ring of integers \(\mathcal O_K\). For every ray element \(x \in K^\times\) for \(\mathfrak m\), the image of \(x\) under the principal ray ideal map, viewed as an invertible fractional ideal of \(K\), is the principal fractional ideal \(x\mathcal O_K\).

@[simp] theorem principalRayIdealMap_apply (m : Modulus K) (x : rayElements m) :
    (principalRayIdealMap m x : (FractionalIdeal (𝓞 K)⁰ K)ˣ) =
      toPrincipalIdeal (𝓞 K) K (x : Kˣ)

Uses 3 · Used by 5

Statement usesFractional ideals coprime to a modulus · Principal ray ideal map · Elements coprime to a modulus

Used byIntegral units generate the unit ideal · Kernel of the projection from the ray class group to the class group · The ray group is the image of the ray-one elements · The ray group lies in the kernel of the ideal-class map · Exactness at the ray-element quotient (kernel form)

TheoremPrincipal ideals agree exactly up to an integral unit#✓fully proved

Let \(K\) be a number field with ring of integers \(\mathcal O_K\). For all \(x, y \in K^\times\), the principal fractional ideals \(x\mathcal O_K\) and \(y\mathcal O_K\) are equal if and only if \(x = uy\) for some unit \(u \in \mathcal O_K^\times\).

theorem toPrincipalIdeal_eq_iff_exists_integralUnit_mul (x y : Kˣ) :
    toPrincipalIdeal (𝓞 K) K x = toPrincipalIdeal (𝓞 K) K y ↔
      ∃ u : (𝓞 K)ˣ,
        x = Units.map (algebraMap (𝓞 K) K).toMonoidHom u * y

Used by 2

Used byIntegral units generate the unit ideal · Exactness at the ray-element quotient (kernel form)

TheoremThe ray group is the image of the ray-one elements#✓fully proved

Let \(\mathfrak m\) be a modulus of a number field \(K\). The ray group of \(\mathfrak m\) equals the image under the principal ray ideal map of the subgroup of ray-one elements, that is, of the ray elements for \(\mathfrak m\) that are congruent to \(1\) modulo the finite part of \(\mathfrak m\) and positive at every real place in its infinite part.

theorem rayGroup_eq_map_rayOneElements (m : Modulus K) :
    rayGroup m = (rayOneElements m).map (principalRayIdealMap m)

Uses 11 · Used by 3

Statement usesFractional ideals coprime to a modulus · Principal ray ideal map · Elements coprime to a modulus · The ray group of a modulus · Ray-one subgroup

Proof usesMultiplicative congruence to one at the finite part · Elements congruent to one modulo a modulus · Positivity at the infinite part of a modulus · Membership in the ray-one subgroup · Value of the principal ray ideal map · Generators of the ray group

Used byThe ray group lies in the kernel of the ideal-class map · Ray-one elements have trivial ray class · Exactness at the ray-element quotient (kernel form)

DefinitionRay-element class map#✓fully proved

For a modulus \(\mathfrak m\) of a number field \(K\), the ray-element class map is the group homomorphism from the group of ray elements of \(\mathfrak m\) to the ray class group \(\mathrm{Cl}_{\mathfrak m}\) that sends \(x\) to the ray class of its principal fractional ideal \((x)\), which is coprime to \(\mathfrak m\); that is, the principal-ideal map followed by the projection onto the ray class group.

noncomputable def rayElementClassMap (m : Modulus K) :
    rayElements m →* RayClassGroup m :=
  (rayClassMap m).comp (principalRayIdealMap m)

Sources

• ATLAS exactSeq_map3, before the quotient lift.

Uses 6 · Used by 10

Statement usesRay class group · Fractional ideals coprime to a modulus · Principal ray ideal map · Ray class map · Elements coprime to a modulus · The ray group of a modulus

Used byKernel of the projection from the ray class group to the class group · Projecting the image of a ray element to the class group · Projecting the image of a residue-sign value to the class group · Value of the ray-element class map · Ray-one elements have trivial ray class · Quotient-to-ray-class map · Exactness at the ray-element quotient (kernel form) · Quotient-to-ray-class map on representatives · The residue-sign transport square commutes · Ray class map on residue-sign values

TheoremValue of the ray-element class map#✓fully proved

Let \(\mathfrak m\) be a modulus of a number field \(K\) and let \(\mathrm{Cl}_{\mathfrak m}\) be its ray class group. For every ray element \(x\) of \(\mathfrak m\), the ray-element class map sends \(x\) to the ray class in \(\mathrm{Cl}_{\mathfrak m}\) of the principal fractional ideal \((x)\), viewed as a fractional ideal coprime to \(\mathfrak m\).

@[simp] theorem rayElementClassMap_apply (m : Modulus K) (x : rayElements m) :
    rayElementClassMap m x = rayClassMap m (principalRayIdealMap m x)

Uses 7 · Used by 5

Statement usesRay class group · Fractional ideals coprime to a modulus · Principal ray ideal map · Ray class map · Ray-element class map · Elements coprime to a modulus · The ray group of a modulus

Used byKernel of the projection from the ray class group to the class group · Projecting the image of a ray element to the class group · Projecting the image of a residue-sign value to the class group · Ray-one elements have trivial ray class · Exactness at the ray-element quotient (kernel form)

TheoremRay-one elements have trivial ray class#✓fully proved

Let \(\mathfrak m\) be a modulus of a number field \(K\). Every ray-one element of \(\mathfrak m\) lies in the kernel of the ray-element class map; that is, its principal fractional ideal has trivial class in the ray class group \(\mathrm{Cl}_{\mathfrak m}\).

theorem rayOneElements_le_rayElementClassMap_ker (m : Modulus K) :
    rayOneElements m ≤ (rayElementClassMap m).ker

Uses 10 · Used by 1

Statement usesRay class group · Fractional ideals coprime to a modulus · Ray-element class map · Elements coprime to a modulus · The ray group of a modulus · Ray-one subgroup

Proof usesPrincipal ray ideal map · Ray class map · Value of the ray-element class map · The ray group is the image of the ray-one elements

Used byQuotient-to-ray-class map

DefinitionQuotient-to-ray-class map#✓fully proved

For a modulus \(\mathfrak m\) of a number field \(K\), the quotient-to-ray-class map is the group homomorphism from the quotient of the group of ray elements of \(\mathfrak m\) by the subgroup of ray-one elements to the ray class group \(\mathrm{Cl}_{\mathfrak m}\) induced by the ray-element class map: the class of a ray element \(x\) goes to the ray class of its principal fractional ideal \((x)\). It is well defined because ray-one elements lie in the kernel of the ray-element class map.

noncomputable def rayQuotientToRayClassGroup (m : Modulus K) :
    (rayElements m ⧸ rayOneElements m) →* RayClassGroup m :=
  QuotientGroup.lift (rayOneElements m) (rayElementClassMap m)
    (rayOneElements_le_rayElementClassMap_ker m)

Sources

• ATLAS exactSeq_map3.

Uses 7 · Used by 12

Statement usesRay class group · Fractional ideals coprime to a modulus · Ray-element class map · Elements coprime to a modulus · The ray group of a modulus · Ray-one subgroup · Ray-one elements have trivial ray class

Used byExactness at the ray-element quotient · The ray class exact sequence · Kernel of the projection from the ray class group to the class group · Projecting the image of a ray element to the class group · Exactness at the ray-element quotient (kernel form) · Quotient-to-ray-class map on representatives · Exactness at the ray class group · Ray class map on residues and signs · Residue-sign-to-ray-class map through the quotient isomorphism · Kernel of the ray class map on residue-sign values · Exactness at the ray class group, residue-sign form · Ray class map on residue-sign values

TheoremQuotient-to-ray-class map on representatives#✓fully proved

Let \(\mathfrak m\) be a modulus of a number field \(K\). For every ray element \(x\) of \(\mathfrak m\), the quotient-to-ray-class map sends the class of \(x\) modulo the ray-one elements to the image of \(x\) under the ray-element class map.

@[simp] theorem rayQuotientToRayClassGroup_mk (m : Modulus K)
    (x : rayElements m) :
    rayQuotientToRayClassGroup m (QuotientGroup.mk x) =
      rayElementClassMap m x

Uses 9 · Used by 4

Statement usesRay class group · Fractional ideals coprime to a modulus · Ray-element class map · Elements coprime to a modulus · The ray group of a modulus · Ray-one subgroup · Quotient-to-ray-class map

Proof usesPrincipal ray ideal map · Ray class map

Used byKernel of the projection from the ray class group to the class group · Projecting the image of a ray element to the class group · Exactness at the ray-element quotient (kernel form) · Ray class map on residue-sign values

TheoremIntegral units generate the unit ideal#✓fully proved

Let \(\mathfrak m\) be a modulus of a number field \(K\). For every unit \(u \in \mathcal O_K^\times\), viewed as a ray element of \(\mathfrak m\), the principal fractional ideal \((u)\), as an element of the group of fractional ideals coprime to \(\mathfrak m\), is the identity element \(\mathcal O_K\).

theorem principalRayIdealMap_integralUnitsToRayElements (m : Modulus K)
    (u : (𝓞 K)ˣ) :
    principalRayIdealMap m (integralUnitsToRayElements m u) = 1

Sources

• ATLAS lines 1160--1175, an input to exactness at the quotient.

Uses 7 · Used by 1

Statement usesFractional ideals coprime to a modulus · Integral units as ray elements · Principal ray ideal map · Elements coprime to a modulus

Proof usesEmbedding of integral units into field units · Value of the principal ray ideal map · Principal ideals agree exactly up to an integral unit

Used byExactness at the ray-element quotient (kernel form)

TheoremExactness at the ray-element quotient (kernel form)#✓fully proved

Let \(\mathfrak m\) be a modulus of a number field \(K\). The kernel of the quotient-to-ray-class map, from the quotient of the ray elements of \(\mathfrak m\) by the ray-one elements to the ray class group \(\mathrm{Cl}_{\mathfrak m}\), equals the image of the map sending each unit \(u \in \mathcal O_K^\times\) to the class of \(u\) in that quotient.

theorem rayQuotientToRayClassGroup_ker (m : Modulus K) :
    (rayQuotientToRayClassGroup m).ker =
      MonoidHom.range (integralUnitsToRayQuotient m)

Sources

• ATLAS exactSeq_exact_at_quotient.

Uses 18 · Used by 2

Statement usesRay class group · Fractional ideals coprime to a modulus · Map from integral units to the ray quotient · Elements coprime to a modulus · The ray group of a modulus · Ray-one subgroup · Quotient-to-ray-class map

Proof usesIntegral units as ray elements · Value of the ray-quotient map on integral units · Principal ray ideal map · Value of the principal ray ideal map · Integral units generate the unit ideal · Ray class map · Ray-element class map · Value of the ray-element class map · The ray group is the image of the ray-one elements · Quotient-to-ray-class map on representatives · Principal ideals agree exactly up to an integral unit

Used byExactness at the ray-element quotient · Kernel of the ray class map on residue-sign values

TheoremExactness at the ray-element quotient#✓fully proved

Let \(\mathfrak m\) be a modulus of a number field \(K\), let \(K_{\mathfrak m}\) be the group of ray elements (elements of \(K^\times\) whose principal ideal is coprime to the finite part of \(\mathfrak m\)), let \(K_{\mathfrak m,1} \le K_{\mathfrak m}\) be the subgroup of ray-one elements, and let \(\mathrm{Cl}_{\mathfrak m}\) be the ray class group of \(\mathfrak m\). In the sequence \(\mathcal O_K^\times \to K_{\mathfrak m}/K_{\mathfrak m,1} \to \mathrm{Cl}_{\mathfrak m}\), where the first map sends a unit \(u\) to the class of \(u\) and the second sends the class of a ray element \(x\) to the ray class of the principal fractional ideal \((x)\), an element of \(K_{\mathfrak m}/K_{\mathfrak m,1}\) maps to the identity of \(\mathrm{Cl}_{\mathfrak m}\) if and only if it is the image of an integral unit.

theorem integralUnitsToRayQuotient_mulExact_rayQuotientToRayClassGroup
    (m : Modulus K) :
    Function.MulExact (integralUnitsToRayQuotient m)
      (rayQuotientToRayClassGroup m)

Sources

• ATLAS exactSeq_exact_at_quotient.

Uses 8 · Used by 1

Statement usesRay class group · Fractional ideals coprime to a modulus · Map from integral units to the ray quotient · Elements coprime to a modulus · The ray group of a modulus · Ray-one subgroup · Quotient-to-ray-class map

Proof usesExactness at the ray-element quotient (kernel form)

Used byThe ray class exact sequence

DefinitionRay class map on residues and signs#✓fully proved

Let \(\mathfrak m\) be a modulus of a number field \(K\) with finite part \(\mathfrak m_0\), let \(K_{\mathfrak m}\) be the group of elements of \(K^\times\) whose principal ideal is coprime to \(\mathfrak m_0\), and let \(K_{\mathfrak m,1}\) be its subgroup of elements congruent to \(1\) modulo \(\mathfrak m_0\) and positive at every real place of \(\mathfrak m\). Let \(T_{\mathfrak m}\) be the residue-sign target of \(\mathfrak m\) and let \(\mathrm{Cl}_{\mathfrak m}\) be the ray class group of \(\mathfrak m\). Let \(\psi : K_{\mathfrak m}/K_{\mathfrak m,1} \to T_{\mathfrak m}\) be the canonical isomorphism induced by sending \(x\) to its signs at the real places of \(\mathfrak m\) and its residue modulo \(\mathfrak m_0\), and let \(\phi : K_{\mathfrak m}/K_{\mathfrak m,1} \to \mathrm{Cl}_{\mathfrak m}\) be the homomorphism induced by sending \(x \in K_{\mathfrak m}\) to the ray class of its principal ideal \((x)\). The residue-sign-to-ray-class map is the group homomorphism \(\phi \circ \psi^{-1} : T_{\mathfrak m} \to \mathrm{Cl}_{\mathfrak m}\).

noncomputable def residueSignToRayClassGroup (m : Modulus K) :
    ResidueSignTarget m →* RayClassGroup m :=
  (rayQuotientToRayClassGroup m).comp
    (rayElementsQuotientEquivResidueSign m).symm.toMonoidHom

Uses 8 · Used by 8

Statement usesRay class group · Residue-sign target · Fractional ideals coprime to a modulus · Elements coprime to a modulus · The residue-sign isomorphism · The ray group of a modulus · Ray-one subgroup · Quotient-to-ray-class map

Used byExactness at the residue-sign group · The ray class exact sequence, sign and residue form · Projecting the image of a residue-sign value to the class group · The residue-sign transport square commutes · Residue-sign-to-ray-class map through the quotient isomorphism · Kernel of the ray class map on residue-sign values · Exactness at the ray class group, residue-sign form · Ray class map on residue-sign values

TheoremResidue-sign-to-ray-class map through the quotient isomorphism#✓fully proved

Let \(\mathfrak m\) be a modulus of a number field \(K\) with finite part \(\mathfrak m_0\), let \(K_{\mathfrak m}\) be the group of elements of \(K^\times\) whose principal ideal is coprime to \(\mathfrak m_0\), and let \(K_{\mathfrak m,1}\) be its subgroup of elements congruent to \(1\) modulo \(\mathfrak m_0\) and positive at every real place of \(\mathfrak m\). Let \(T_{\mathfrak m}\) be the residue-sign target of \(\mathfrak m\), let \(\mathrm{Cl}_{\mathfrak m}\) be the ray class group of \(\mathfrak m\), let \(\psi : K_{\mathfrak m}/K_{\mathfrak m,1} \to T_{\mathfrak m}\) be the canonical isomorphism induced by sending \(x\) to its signs at the real places of \(\mathfrak m\) and its residue modulo \(\mathfrak m_0\), and let \(\phi : K_{\mathfrak m}/K_{\mathfrak m,1} \to \mathrm{Cl}_{\mathfrak m}\) be the homomorphism induced by sending \(x\) to the ray class of its principal ideal \((x)\). Then for every \(q \in K_{\mathfrak m}/K_{\mathfrak m,1}\), the residue-sign-to-ray-class map \(T_{\mathfrak m} \to \mathrm{Cl}_{\mathfrak m}\) sends \(\psi(q)\) to \(\phi(q)\).

@[simp] theorem residueSignToRayClassGroup_equiv (m : Modulus K)
    (q : rayElements m ⧸ rayOneElements m) :
    residueSignToRayClassGroup m (rayElementsQuotientEquivResidueSign m q) =
      rayQuotientToRayClassGroup m q

Uses 9 · Used by 1

Statement usesRay class group · Residue-sign target · Fractional ideals coprime to a modulus · Elements coprime to a modulus · The residue-sign isomorphism · The ray group of a modulus · Ray-one subgroup · Quotient-to-ray-class map · Ray class map on residues and signs

Used byRay class map on residue-sign values

TheoremRay class map on residue-sign values#✓fully proved

Let \(\mathfrak m\) be a modulus of a number field \(K\) and let \(x\) be a ray element of \(\mathfrak m\), that is, \(x \in K^\times\) with principal ideal coprime to the finite part of \(\mathfrak m\). Then the residue-sign-to-ray-class map sends the residue-sign value of \(x\) (its signs at the real places of \(\mathfrak m\) together with its residue modulo the finite part) to the ray class of the principal ideal \((x)\).

theorem residueSignToRayClassGroup_residueSignMap (m : Modulus K)
    (x : rayElements m) :
    residueSignToRayClassGroup m (residueSignMap m x) =
      rayElementClassMap m x

Uses 14 · Used by 2

Statement usesRay class group · Residue-sign target · Fractional ideals coprime to a modulus · Ray-element class map · Elements coprime to a modulus · The ray group of a modulus · Residue-sign map · Ray class map on residues and signs

Proof usesThe residue-sign isomorphism · The residue-sign isomorphism on classes · Ray-one subgroup · Quotient-to-ray-class map · Quotient-to-ray-class map on representatives · Residue-sign-to-ray-class map through the quotient isomorphism

Used byProjecting the image of a residue-sign value to the class group · The residue-sign transport square commutes

TheoremThe residue-sign transport square commutes#✓fully proved

Let \(\mathfrak m\) be a modulus of a number field \(K\). The residue-sign map from the ray elements of \(\mathfrak m\) to the residue-sign target, followed by the transported residue-sign-to-ray-class map, equals the ray-element class map.

theorem residueSignToRayClassGroup_comp_residueSignMap (m : Modulus K) :
    (residueSignToRayClassGroup m).comp (residueSignMap m) =
      rayElementClassMap m

Uses 9

Statement usesRay class group · Residue-sign target · Fractional ideals coprime to a modulus · Ray-element class map · Elements coprime to a modulus · The ray group of a modulus · Residue-sign map · Ray class map on residues and signs

Proof usesRay class map on residue-sign values

TheoremKernel of the ray class map on residue-sign values#✓fully proved

Let \(\mathfrak m\) be a modulus of a number field \(K\). The kernel of the residue-sign-to-ray-class map from the residue-sign target of \(\mathfrak m\) to the ray class group of \(\mathfrak m\) equals the image of the homomorphism \(\mathcal O_K^\times \to\) (residue-sign target) that sends a unit \(u\) to its residue-sign value, namely its signs at the real places of \(\mathfrak m\) together with its residue modulo the finite part of \(\mathfrak m\).

theorem residueSignToRayClassGroup_ker (m : Modulus K) :
    (residueSignToRayClassGroup m).ker =
      MonoidHom.range (integralUnitsToResidueSign m)

Uses 12 · Used by 1

Statement usesRay class group · Residue-sign target · Fractional ideals coprime to a modulus · Residue-sign map on integral units · The ray group of a modulus · Ray class map on residues and signs

Proof usesMap from integral units to the ray quotient · Elements coprime to a modulus · The residue-sign isomorphism · Ray-one subgroup · Quotient-to-ray-class map · Exactness at the ray-element quotient (kernel form)

Used byExactness at the residue-sign group

TheoremExactness at the residue-sign group#✓fully proved

Let \(\mathfrak m\) be a modulus of a number field \(K\) with finite part \(\mathfrak m_0\) and set of real places \(\mathfrak m_\infty\), let \(\mathrm{Cl}_{\mathfrak m}\) be its ray class group, and let \(R_{\mathfrak m} = \{\pm 1\}^{\mathfrak m_\infty} \times (\mathcal O_K/\mathfrak m_0)^\times\). Consider the maps \(\mathcal O_K^\times \to R_{\mathfrak m} \to \mathrm{Cl}_{\mathfrak m}\). The first sends a unit \(u\) to its signs at the places in \(\mathfrak m_\infty\) together with its class in \((\mathcal O_K/\mathfrak m_0)^\times\). The second is the quotient-to-ray-class map transported along the canonical isomorphism from the quotient of the ray elements by the ray-one elements onto \(R_{\mathfrak m}\), so it sends the image in \(R_{\mathfrak m}\) of a ray element \(x\) to the ray class of the principal fractional ideal \((x)\). An element of \(R_{\mathfrak m}\) maps to the identity of \(\mathrm{Cl}_{\mathfrak m}\) if and only if it is the image of an integral unit.

theorem integralUnitsToResidueSign_mulExact_residueSignToRayClassGroup
    (m : Modulus K) :
    Function.MulExact (integralUnitsToResidueSign m)
      (residueSignToRayClassGroup m)

Uses 7 · Used by 1

Statement usesRay class group · Residue-sign target · Fractional ideals coprime to a modulus · Residue-sign map on integral units · The ray group of a modulus · Ray class map on residues and signs

Proof usesKernel of the ray class map on residue-sign values

Used byThe ray class exact sequence, sign and residue form

DefinitionIdeal-class map on coprime fractional ideals#✓fully proved

Let \(K\) be a number field, \(\mathfrak m\) a modulus of \(K\), and \(I_{\mathfrak m}\) the group of nonzero fractional ideals of \(\mathcal O_K\) coprime to the finite part of \(\mathfrak m\). The coprime ideal-class map is the group homomorphism \(I_{\mathfrak m} \to \mathrm{Cl}(\mathcal O_K)\) that sends \(I\) to its ideal class \([I]\): the inclusion of \(I_{\mathfrak m}\) into the group of nonzero fractional ideals followed by the class map.

noncomputable def coprimeIdealClassMap (m : Modulus K) :
    coprimeFractionalIdeals m →* ClassGroup (𝓞 K) :=
  (ClassGroup.mk K).comp (coprimeFractionalIdeals m).subtype

Sources

• ATLAS exactSeq_map4, before the quotient lift.

Uses 1 · Used by 10

Statement usesFractional ideals coprime to a modulus

Used byValue of the ideal-class map on a coprime ideal · Every ideal class contains a fractional ideal coprime to the modulus · Projection from the ray class group to the class group · The ideal-class map factors through the ray class group · Kernel of the projection from the ray class group to the class group · Projection to the class group on ray class representatives · Projecting the image of a ray element to the class group · Projecting the image of a residue-sign value to the class group · The ray class group surjects onto the class group · The ray group lies in the kernel of the ideal-class map

TheoremValue of the ideal-class map on a coprime ideal#✓fully proved

Let \(K\) be a number field, \(\mathfrak m\) a modulus of \(K\), and \(I_{\mathfrak m}\) the group of nonzero fractional ideals of \(\mathcal O_K\) coprime to the finite part of \(\mathfrak m\). For every \(I \in I_{\mathfrak m}\), the coprime ideal-class map sends \(I\) to the class \([I]\) in the class group \(\mathrm{Cl}(\mathcal O_K)\) of \(I\) viewed as a nonzero fractional ideal.

@[simp] theorem coprimeIdealClassMap_apply (m : Modulus K)
    (I : coprimeFractionalIdeals m) :
    coprimeIdealClassMap m I =
      ClassGroup.mk K ((coprimeFractionalIdeals m).subtype I)

Uses 2 · Used by 3

Statement usesFractional ideals coprime to a modulus · Ideal-class map on coprime fractional ideals

Used byEvery ideal class contains a fractional ideal coprime to the modulus · Kernel of the projection from the ray class group to the class group · The ray group lies in the kernel of the ideal-class map

TheoremThe ray group lies in the kernel of the ideal-class map#✓fully proved

Let \(K\) be a number field, \(\mathfrak m\) a modulus of \(K\), \(I_{\mathfrak m}\) the group of nonzero fractional ideals of \(\mathcal O_K\) coprime to the finite part of \(\mathfrak m\), and \(P_{\mathfrak m} \subseteq I_{\mathfrak m}\) the ray group. Then \(P_{\mathfrak m}\) is contained in the kernel of the coprime ideal-class map \(I_{\mathfrak m} \to \mathrm{Cl}(\mathcal O_K)\), \(I \mapsto [I]\): every ideal in \(P_{\mathfrak m}\) has trivial class in \(\mathrm{Cl}(\mathcal O_K)\).

theorem rayGroup_le_coprimeIdealClassMap_ker (m : Modulus K) :
    rayGroup m ≤ (coprimeIdealClassMap m).ker

Uses 9 · Used by 1

Statement usesFractional ideals coprime to a modulus · Ideal-class map on coprime fractional ideals · The ray group of a modulus

Proof usesValue of the ideal-class map on a coprime ideal · Principal ray ideal map · Value of the principal ray ideal map · Elements coprime to a modulus · The ray group is the image of the ray-one elements · Ray-one subgroup

Used byProjection from the ray class group to the class group

DefinitionProjection from the ray class group to the class group#✓fully proved

Let \(K\) be a number field, \(\mathfrak m\) a modulus of \(K\), \(I_{\mathfrak m}\) the group of nonzero fractional ideals of \(\mathcal O_K\) coprime to the finite part of \(\mathfrak m\), \(P_{\mathfrak m}\) the ray group, and \(\mathrm{Cl}_{\mathfrak m} = I_{\mathfrak m}/P_{\mathfrak m}\) the ray class group. The projection \(\mathrm{Cl}_{\mathfrak m} \to \mathrm{Cl}(\mathcal O_K)\) is the group homomorphism induced by the coprime ideal-class map \(I_{\mathfrak m} \to \mathrm{Cl}(\mathcal O_K)\), \(I \mapsto [I]\), which is trivial on \(P_{\mathfrak m}\); it sends the ray class of \(I\) to \([I]\).

noncomputable def rayClassToClassGroup (m : Modulus K) :
    RayClassGroup m →* ClassGroup (𝓞 K) :=
  QuotientGroup.lift (rayGroup m) (coprimeIdealClassMap m)
    (rayGroup_le_coprimeIdealClassMap_ker m)

Sources

• ATLAS exactSeq_map4.

Uses 5 · Used by 10

Statement usesRay class group · Fractional ideals coprime to a modulus · Ideal-class map on coprime fractional ideals · The ray group of a modulus · The ray group lies in the kernel of the ideal-class map

Used byThe ray class exact sequence, sign and residue form · The ray class exact sequence · The ideal-class map factors through the ray class group · Kernel of the projection from the ray class group to the class group · Projection to the class group on ray class representatives · Projecting the image of a ray element to the class group · Projecting the image of a residue-sign value to the class group · The ray class group surjects onto the class group · Exactness at the ray class group · Exactness at the ray class group, residue-sign form

TheoremProjection to the class group on ray class representatives#✓fully proved

Let \(K\) be a number field, \(\mathfrak m\) a modulus of \(K\), \(I_{\mathfrak m}\) the group of nonzero fractional ideals of \(\mathcal O_K\) coprime to the finite part of \(\mathfrak m\), and \(\mathrm{Cl}_{\mathfrak m}\) the ray class group. For every \(I \in I_{\mathfrak m}\), the projection \(\mathrm{Cl}_{\mathfrak m} \to \mathrm{Cl}(\mathcal O_K)\) sends the ray class of \(I\) to \([I]\), the value of the coprime ideal-class map at \(I\).

@[simp] theorem rayClassToClassGroup_rayClassMap (m : Modulus K)
    (I : coprimeFractionalIdeals m) :
    rayClassToClassGroup m (rayClassMap m I) = coprimeIdealClassMap m I

Uses 6 · Used by 5

Statement usesRay class group · Fractional ideals coprime to a modulus · Ideal-class map on coprime fractional ideals · Ray class map · Projection from the ray class group to the class group · The ray group of a modulus

Used byThe ideal-class map factors through the ray class group · Kernel of the projection from the ray class group to the class group · Projecting the image of a ray element to the class group · Projecting the image of a residue-sign value to the class group · The ray class group surjects onto the class group

TheoremThe ideal-class map factors through the ray class group#✓fully proved

Let \(K\) be a number field, \(\mathfrak m\) a modulus of \(K\), \(I_{\mathfrak m}\) the group of nonzero fractional ideals of \(\mathcal O_K\) coprime to the finite part of \(\mathfrak m\), \(P_{\mathfrak m} \subseteq I_{\mathfrak m}\) the ray group, and \(\mathrm{Cl}_{\mathfrak m} = I_{\mathfrak m}/P_{\mathfrak m}\) the ray class group. As group homomorphisms, the quotient map \(I_{\mathfrak m} \to \mathrm{Cl}_{\mathfrak m}\) followed by the projection \(\mathrm{Cl}_{\mathfrak m} \to \mathrm{Cl}(\mathcal O_K)\) equals the coprime ideal-class map \(I_{\mathfrak m} \to \mathrm{Cl}(\mathcal O_K)\), \(I \mapsto [I]\).

theorem rayClassToClassGroup_comp_rayClassMap (m : Modulus K) :
    (rayClassToClassGroup m).comp (rayClassMap m) = coprimeIdealClassMap m

Uses 7

Statement usesRay class group · Fractional ideals coprime to a modulus · Ideal-class map on coprime fractional ideals · Ray class map · Projection from the ray class group to the class group · The ray group of a modulus

Proof usesProjection to the class group on ray class representatives

TheoremProjecting the image of a ray element to the class group#✓fully proved

Let \(K\) be a number field, \(\mathfrak m\) a modulus of \(K\) with finite part \(\mathfrak m_0\), \(I_{\mathfrak m}\) the group of nonzero fractional ideals of \(\mathcal O_K\) coprime to \(\mathfrak m_0\), \(\mathrm{Cl}_{\mathfrak m}\) the ray class group, \(K_{\mathfrak m}\) the group of \(x \in K^\times\) with \(x\mathcal O_K \in I_{\mathfrak m}\), and \(K_{\mathfrak m,1} \subseteq K_{\mathfrak m}\) the subgroup of those \(x\) with \(x \equiv 1 \pmod{\mathfrak m_0}\) that are positive at every real place in \(\mathfrak m\). For every \(x \in K_{\mathfrak m}\), sending the class of \(x\) through the map \(K_{\mathfrak m}/K_{\mathfrak m,1} \to \mathrm{Cl}_{\mathfrak m}\) that takes the class of \(y\) to the ray class of \(y\mathcal O_K\), and then through the projection \(\mathrm{Cl}_{\mathfrak m} \to \mathrm{Cl}(\mathcal O_K)\), gives \([x\mathcal O_K]\), the value of the coprime ideal-class map at \(x\mathcal O_K \in I_{\mathfrak m}\).

theorem rayClassToClassGroup_rayQuotientToRayClassGroup (m : Modulus K)
    (x : rayElements m) :
    rayClassToClassGroup m (rayQuotientToRayClassGroup m (QuotientGroup.mk x)) =
      coprimeIdealClassMap m (principalRayIdealMap m x)

Uses 14

Statement usesRay class group · Fractional ideals coprime to a modulus · Ideal-class map on coprime fractional ideals · Principal ray ideal map · Projection from the ray class group to the class group · Elements coprime to a modulus · The ray group of a modulus · Ray-one subgroup · Quotient-to-ray-class map

Proof usesRay class map · Projection to the class group on ray class representatives · Ray-element class map · Value of the ray-element class map · Quotient-to-ray-class map on representatives

TheoremProjecting the image of a residue-sign value to the class group#✓fully proved

Let \(K\) be a number field, \(\mathfrak m\) a modulus of \(K\) with finite part \(\mathfrak m_0\), \(I_{\mathfrak m}\) the group of nonzero fractional ideals of \(\mathcal O_K\) coprime to \(\mathfrak m_0\), \(\mathrm{Cl}_{\mathfrak m}\) the ray class group, and \(K_{\mathfrak m}\) the group of \(x \in K^\times\) with \(x\mathcal O_K \in I_{\mathfrak m}\). Let \(T_{\mathfrak m}\) be the product of one group of order \(2\) for each real place in \(\mathfrak m\) with \((\mathcal O_K/\mathfrak m_0)^\times\), let \(\rho : K_{\mathfrak m} \to T_{\mathfrak m}\) be the residue-sign map, and let \(T_{\mathfrak m} \to \mathrm{Cl}_{\mathfrak m}\) be the residue-sign-to-ray-class map. For every \(x \in K_{\mathfrak m}\), sending \(\rho(x)\) through this map and then through the projection \(\mathrm{Cl}_{\mathfrak m} \to \mathrm{Cl}(\mathcal O_K)\) gives \([x\mathcal O_K]\), the value of the coprime ideal-class map at \(x\mathcal O_K \in I_{\mathfrak m}\).

theorem rayClassToClassGroup_residueSignToRayClassGroup (m : Modulus K)
    (x : rayElements m) :
    rayClassToClassGroup m
        (residueSignToRayClassGroup m (residueSignMap m x)) =
      coprimeIdealClassMap m (principalRayIdealMap m x)

Uses 15

Statement usesRay class group · Residue-sign target · Fractional ideals coprime to a modulus · Ideal-class map on coprime fractional ideals · Principal ray ideal map · Projection from the ray class group to the class group · Elements coprime to a modulus · The ray group of a modulus · Residue-sign map · Ray class map on residues and signs

Proof usesRay class map · Projection to the class group on ray class representatives · Ray-element class map · Value of the ray-element class map · Ray class map on residue-sign values

TheoremKernel of the projection from the ray class group to the class group#✓fully proved

Let \(K\) be a number field, \(\mathfrak m\) a modulus of \(K\) with finite part \(\mathfrak m_0\), \(I_{\mathfrak m}\) the group of nonzero fractional ideals of \(\mathcal O_K\) coprime to \(\mathfrak m_0\), \(\mathrm{Cl}_{\mathfrak m}\) the ray class group, \(K_{\mathfrak m}\) the group of \(x \in K^\times\) with \(x\mathcal O_K \in I_{\mathfrak m}\), and \(K_{\mathfrak m,1} \subseteq K_{\mathfrak m}\) the subgroup of those \(x\) with \(x \equiv 1 \pmod{\mathfrak m_0}\) that are positive at every real place in \(\mathfrak m\). The kernel of the projection \(\mathrm{Cl}_{\mathfrak m} \to \mathrm{Cl}(\mathcal O_K)\) equals the image of the homomorphism \(K_{\mathfrak m}/K_{\mathfrak m,1} \to \mathrm{Cl}_{\mathfrak m}\) that sends the class of \(x\) to the ray class of \(x\mathcal O_K\).

theorem rayClassToClassGroup_ker (m : Modulus K) :
    (rayClassToClassGroup m).ker =
      MonoidHom.range (rayQuotientToRayClassGroup m)

Sources

• ATLAS exactSeq_exact_at_ray_class.

Uses 16 · Used by 2

Statement usesRay class group · Fractional ideals coprime to a modulus · Projection from the ray class group to the class group · Elements coprime to a modulus · The ray group of a modulus · Ray-one subgroup · Quotient-to-ray-class map

Proof usesIdeal-class map on coprime fractional ideals · Value of the ideal-class map on a coprime ideal · Principal ray ideal map · Value of the principal ray ideal map · Ray class map · Projection to the class group on ray class representatives · Ray-element class map · Value of the ray-element class map · Quotient-to-ray-class map on representatives

Used byExactness at the ray class group · Exactness at the ray class group, residue-sign form

TheoremExactness at the ray class group#✓fully proved

Let \(K\) be a number field, \(\mathfrak m\) a modulus of \(K\) with finite part \(\mathfrak m_0\), \(I_{\mathfrak m}\) the group of nonzero fractional ideals of \(\mathcal O_K\) coprime to \(\mathfrak m_0\), \(\mathrm{Cl}_{\mathfrak m}\) the ray class group, \(K_{\mathfrak m}\) the group of \(x \in K^\times\) with \(x\mathcal O_K \in I_{\mathfrak m}\), and \(K_{\mathfrak m,1} \subseteq K_{\mathfrak m}\) the subgroup of those \(x\) with \(x \equiv 1 \pmod{\mathfrak m_0}\) that are positive at every real place in \(\mathfrak m\). The sequence \(K_{\mathfrak m}/K_{\mathfrak m,1} \to \mathrm{Cl}_{\mathfrak m} \to \mathrm{Cl}(\mathcal O_K)\) is exact at \(\mathrm{Cl}_{\mathfrak m}\), where the first map sends the class of \(x\) to the ray class of \(x\mathcal O_K\) and the second is the projection: a ray class maps to the identity of \(\mathrm{Cl}(\mathcal O_K)\) if and only if it lies in the image of the first map.

theorem rayQuotientToRayClassGroup_mulExact_rayClassToClassGroup
    (m : Modulus K) :
    Function.MulExact (rayQuotientToRayClassGroup m)
      (rayClassToClassGroup m)

Sources

• ATLAS exactSeq_exact_at_ray_class.

Uses 8 · Used by 1

Statement usesRay class group · Fractional ideals coprime to a modulus · Projection from the ray class group to the class group · Elements coprime to a modulus · The ray group of a modulus · Ray-one subgroup · Quotient-to-ray-class map

Proof usesKernel of the projection from the ray class group to the class group

Used byThe ray class exact sequence

TheoremExactness at the ray class group, residue-sign form#✓fully proved

Let \(\mathfrak m\) be a modulus of a number field \(K\), with finite part the nonzero ideal \(\mathfrak m_0\) of \(\mathcal O_K\) and infinite part the finite set \(\mathfrak m_\infty\) of real places of \(K\). Let \(\varphi\) be the homomorphism from the residue-sign group \(\{\pm 1\}^{\mathfrak m_\infty} \times (\mathcal O_K/\mathfrak m_0)^\times\) to the ray class group \(\mathrm{Cl}_{\mathfrak m}(K)\) that sends the signs at the places in \(\mathfrak m_\infty\) and the residue class modulo \(\mathfrak m_0\) of an element \(x \in K^\times\) coprime to \(\mathfrak m_0\) to the ray class of the principal ideal \((x)\), and let \(\pi \colon \mathrm{Cl}_{\mathfrak m}(K) \to \mathrm{Cl}(K)\) be the projection to the ideal class group. Then a ray class \(c\) satisfies \(\pi(c) = 1\) if and only if \(c\) lies in the image of \(\varphi\); that is, the sequence is exact at \(\mathrm{Cl}_{\mathfrak m}(K)\).

theorem residueSignToRayClassGroup_mulExact_rayClassToClassGroup
    (m : Modulus K) :
    Function.MulExact (residueSignToRayClassGroup m)
      (rayClassToClassGroup m)

Uses 11 · Used by 1

Statement usesRay class group · Residue-sign target · Fractional ideals coprime to a modulus · Projection from the ray class group to the class group · The ray group of a modulus · Ray class map on residues and signs

Proof usesKernel of the projection from the ray class group to the class group · Elements coprime to a modulus · The residue-sign isomorphism · Ray-one subgroup · Quotient-to-ray-class map

Used byThe ray class exact sequence, sign and residue form

TheoremNonzero integral ideals coprime to the modulus are coprime fractional ideals#✓fully proved

Let \(K\) be a number field with ring of integers \(\mathcal O_K\), let \(\mathfrak m\) be a modulus of \(K\) with finite part \(\mathfrak m_0\), and let \(I\) be a nonzero ideal of \(\mathcal O_K\) with \(I + \mathfrak m_0 = \mathcal O_K\). Then \(I\), viewed as an invertible fractional ideal of \(K\), belongs to the group of fractional ideals coprime to \(\mathfrak m_0\): its exponent at every prime dividing \(\mathfrak m_0\) is \(0\).

theorem fractionalIdealMk0_mem_coprimeFractionalIdeals
    (m : Modulus K) (I : nonZeroDivisors (Ideal (𝓞 K)))
    (hI : IsCoprime (I : Ideal (𝓞 K))
      (m.finitePart : Ideal (𝓞 K))) :
    FractionalIdeal.mk0 K I ∈ coprimeFractionalIdeals m

Sources

• E5 mk0 membership/count bridge for ATLAS lines 1431--1465.

Uses 2 · Used by 1

Statement usesFractional ideals coprime to a modulus

Proof usesPrimes dividing a modulus

Used byEvery ideal class contains a fractional ideal coprime to the modulus

TheoremEvery ideal class contains a fractional ideal coprime to the modulus#✓fully proved

Let \(K\) be a number field and \(\mathfrak m\) a modulus of \(K\) with finite part \(\mathfrak m_0\). The homomorphism from the group of fractional ideals of \(K\) coprime to \(\mathfrak m_0\) (those whose exponent at every prime dividing \(\mathfrak m_0\) is \(0\)) to the class group of \(\mathcal O_K\), sending each such fractional ideal to its ideal class, is surjective.

theorem coprimeIdealClassMap_surjective (m : Modulus K) :
    Function.Surjective (coprimeIdealClassMap m)

Sources

• ATLAS lines 1466--1476; Lemma 21.7 at lines 958--1010 is reused via the stronger ClassGroup.exists_mk0_eq_and_isCoprime.

Uses 5 · Used by 1

Statement usesFractional ideals coprime to a modulus · Ideal-class map on coprime fractional ideals

Proof usesIdeal classes have representatives coprime to a given ideal · Value of the ideal-class map on a coprime ideal · Nonzero integral ideals coprime to the modulus are coprime fractional ideals

Used byThe ray class group surjects onto the class group

TheoremThe ray class group surjects onto the class group#✓fully proved

Let \(K\) be a number field and \(\mathfrak m\) a modulus of \(K\). The homomorphism from the ray class group of \(\mathfrak m\) to the class group of \(\mathcal O_K\), sending the ray class of a fractional ideal coprime to the finite part of \(\mathfrak m\) to its ideal class, is surjective.

theorem rayClassToClassGroup_surjective (m : Modulus K) :
    Function.Surjective (rayClassToClassGroup m)

Sources

• ATLAS lines 1478--1480.

Uses 8 · Used by 2

Statement usesRay class group · Fractional ideals coprime to a modulus · Projection from the ray class group to the class group · The ray group of a modulus

Proof usesIdeal-class map on coprime fractional ideals · Every ideal class contains a fractional ideal coprime to the modulus · Ray class map · Projection to the class group on ray class representatives

Used byThe ray class exact sequence, sign and residue form · The ray class exact sequence

TheoremThe ray class exact sequence#✓fully proved

Let \(K\) be a number field with ring of integers \(\mathcal O_K\), and let \(\mathfrak m\) be a modulus of \(K\) with finite part \(\mathfrak m_0\) (a nonzero ideal of \(\mathcal O_K\)) and infinite part \(\mathfrak m_\infty\) (a finite set of real places). Let \(K_{\mathfrak m}\) be the group of \(x \in K^\times\) whose principal fractional ideal is coprime to \(\mathfrak m_0\), and let \(K_{\mathfrak m,1} \subseteq K_{\mathfrak m}\) be the subgroup of those \(x\) that are positive at every real place in \(\mathfrak m_\infty\) and satisfy, for every prime \(\mathfrak p \mid \mathfrak m_0\), either \(x = 1\) or \(v_{\mathfrak p}(x - 1) \ge v_{\mathfrak p}(\mathfrak m_0)\), where \(v_{\mathfrak p}\) of an element of \(K^\times\) or of a nonzero ideal is the exponent of \(\mathfrak p\) in its fractional ideal. Let \(U_{\mathfrak m,1}\) be the group of units of \(\mathcal O_K\) lying in \(K_{\mathfrak m,1}\), let \(\mathrm{Cl}_{\mathfrak m}\) be the ray class group (fractional ideals coprime to \(\mathfrak m_0\) modulo the subgroup generated by the principal ideals \((x)\) with \(x \in K_{\mathfrak m,1}\)), and let \(\mathrm{Cl}(\mathcal O_K)\) be the class group. Then the sequence

\[ 1 \to U_{\mathfrak m,1} \to \mathcal O_K^\times \to K_{\mathfrak m}/K_{\mathfrak m,1} \to \mathrm{Cl}_{\mathfrak m} \to \mathrm{Cl}(\mathcal O_K) \to 1 \]

is exact, where the maps are the inclusion, the map sending a unit to its class modulo \(K_{\mathfrak m,1}\), the map sending the class of \(x\) to the ray class of \((x)\), and the map sending the ray class of a fractional ideal to its ideal class.

theorem rayClass_six_term_exact (m : Modulus K) :
    Function.Injective (integralRayOneUnitsInclusion m) ∧
    Function.MulExact (integralRayOneUnitsInclusion m)
      (integralUnitsToRayQuotient m) ∧
    Function.MulExact (integralUnitsToRayQuotient m)
      (rayQuotientToRayClassGroup m) ∧
    Function.MulExact (rayQuotientToRayClassGroup m)
      (rayClassToClassGroup m) ∧
    Function.Surjective (rayClassToClassGroup m)

Sources

• ATLAS lines 1012--1480; this theorem aggregates the separately source-backed map, exactness and surjectivity declarations and is not a direct declaration port.

Uses 15

Statement usesRay class group · Fractional ideals coprime to a modulus · Ray-one integral units · Inclusion of the ray-one integral units · Map from integral units to the ray quotient · Projection from the ray class group to the class group · Elements coprime to a modulus · The ray group of a modulus · Ray-one subgroup · Quotient-to-ray-class map

Proof usesThe inclusion of the ray-one integral units is injective · Exactness at the ray-element quotient · Exactness of the ray sequence at the integral units · The ray class group surjects onto the class group · Exactness at the ray class group

TheoremThe ray class exact sequence, sign and residue form#✓fully proved

Let \(K\) be a number field with ring of integers \(\mathcal O_K\), and let \(\mathfrak m\) be a modulus of \(K\) with finite part \(\mathfrak m_0\) (a nonzero ideal of \(\mathcal O_K\)) and infinite part \(\mathfrak m_\infty\) (a finite set of real places). Let \(K_{\mathfrak m}\) be the group of \(x \in K^\times\) whose principal fractional ideal is coprime to \(\mathfrak m_0\), and let \(K_{\mathfrak m,1} \subseteq K_{\mathfrak m}\) be the subgroup of those \(x\) that are positive at every real place in \(\mathfrak m_\infty\) and satisfy, for every prime \(\mathfrak p \mid \mathfrak m_0\), either \(x = 1\) or \(v_{\mathfrak p}(x - 1) \ge v_{\mathfrak p}(\mathfrak m_0)\), where \(v_{\mathfrak p}\) of an element of \(K^\times\) or of a nonzero ideal is the exponent of \(\mathfrak p\) in its fractional ideal. Let \(U_{\mathfrak m,1}\) be the group of units of \(\mathcal O_K\) lying in \(K_{\mathfrak m,1}\), let \(\mathrm{Cl}_{\mathfrak m}\) be the ray class group (fractional ideals coprime to \(\mathfrak m_0\) modulo the subgroup generated by the principal ideals \((x)\) with \(x \in K_{\mathfrak m,1}\)), and let \(\mathrm{Cl}(\mathcal O_K)\) be the class group. For \(x \in K_{\mathfrak m}\), let \(\rho(x) \in \{\pm 1\}^{\mathfrak m_\infty} \times (\mathcal O_K/\mathfrak m_0)^\times\) record the sign of \(x\) at each real place in \(\mathfrak m_\infty\) and the residue class of \(x\) modulo \(\mathfrak m_0\) (the class of \(a b^{-1}\) when \(x = a/b\) with \(a, b \in \mathcal O_K\) prime to \(\mathfrak m_0\)); \(\rho\) is surjective with kernel \(K_{\mathfrak m,1}\). Then the sequence

\[ 1 \to U_{\mathfrak m,1} \to \mathcal O_K^\times \to \{\pm 1\}^{\mathfrak m_\infty} \times (\mathcal O_K/\mathfrak m_0)^\times \to \mathrm{Cl}_{\mathfrak m} \to \mathrm{Cl}(\mathcal O_K) \to 1 \]

is exact, where the maps are the inclusion, the restriction of \(\rho\) to units, the map sending \(\rho(x)\) to the ray class of \((x)\), and the map sending the ray class of a fractional ideal to its ideal class.

theorem rayClass_residueSign_six_term_exact (m : Modulus K) :
    Function.Injective (integralRayOneUnitsInclusion m) ∧
    Function.MulExact (integralRayOneUnitsInclusion m)
      (integralUnitsToResidueSign m) ∧
    Function.MulExact (integralUnitsToResidueSign m)
      (residueSignToRayClassGroup m) ∧
    Function.MulExact (residueSignToRayClassGroup m)
      (rayClassToClassGroup m) ∧
    Function.Surjective (rayClassToClassGroup m)

Sources

• ATLAS lines 1012--1480, aggregated from the separately source-backed map, exactness and surjectivity declarations (not a direct declaration port), and transported through the quotient equivalence backed by lines 2607--2647.

Uses 14

Statement usesRay class group · Residue-sign target · Fractional ideals coprime to a modulus · Ray-one integral units · Inclusion of the ray-one integral units · Residue-sign map on integral units · Projection from the ray class group to the class group · The ray group of a modulus · Ray class map on residues and signs

Proof usesThe inclusion of the ray-one integral units is injective · Exactness at the residue-sign group · Exactness at the integral units, residue-sign form · The ray class group surjects onto the class group · Exactness at the ray class group, residue-sign form

97 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.