Ray class characters

AbbreviationRay class character#✓fully proved

A ray class character of a modulus \(m\) of a number field \(K\) is a group homomorphism from the ray class group of \(m\) to the unit circle \(\{z \in \mathbb C : |z| = 1\}\).

abbrev RayClassCharacter (m : Modulus K) := RayClassGroup m →* Circle

Uses 3 · Used by 10

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

Used byComplex 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 · Primitive ray class character · Primitivity in terms of the level-change map · Pullback of a ray class character to ideals · Pulled-back ray class characters are trivial on the ray group · Trivial character

DefinitionTrivial character#✓fully proved

The trivial ray class character of a modulus \(m\) of a number field \(K\) is the ray class character sending every ray class of \(m\) to \(1\).

def trivialCharacter (m : Modulus K) : RayClassCharacter m := 1

Uses 4

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

DefinitionPullback of a ray class character to ideals#✓fully proved

For a ray class character \(\chi\) of a modulus \(m\) of a number field \(K\), its pullback is the group homomorphism from the group of nonzero fractional ideals of \(K\) coprime to the finite part of \(m\) to the unit circle sending \(\mathfrak a\) to \(\chi([\mathfrak a])\), where \([\mathfrak a]\) is the ray class of \(\mathfrak a\).

def pullback (chi : RayClassCharacter m) :
    coprimeFractionalIdeals m →* Circle :=
  chi.comp (rayClassMap m)

Uses 5 · Used by 2

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

Used byInduced characters agree on coprime ideals · Pulled-back ray class characters are trivial on the ray group

TheoremPulled-back ray class characters are trivial on the ray group#✓fully proved

Let \(\chi\) be a ray class character of a modulus \(m\) of a number field \(K\). If a nonzero fractional ideal \(\mathfrak a\) of \(K\) coprime to the finite part of \(m\) lies in the ray group of \(m\), then the pullback of \(\chi\) to the fractional ideals coprime to the finite part of \(m\) takes the value \(1\) at \(\mathfrak a\).

theorem pullback_eq_one_of_mem_rayGroup (chi : RayClassCharacter m)
    (x : coprimeFractionalIdeals m) (h : x ∈ rayGroup m) :
    pullback chi x = 1

Uses 6

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

Proof usesRay class group · Ray class map

DefinitionComplex value of a ray class character#✓fully proved

For a ray class character \(\chi\) of a modulus \(m\) and a ray class \(x\) of \(m\), the complex value of \(\chi\) at \(x\) is \(\chi(x)\), a point of the unit circle, regarded as a complex number.

def evalComplex (chi : RayClassCharacter m) (x : RayClassGroup m) : ℂ :=
  Circle.coeHom (chi x)

Uses 4 · Used by 1

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

Used byRay class characters take the complex value \(1\) on the ray group

TheoremRay class characters take the complex value \(1\) on the ray group#✓fully proved

Let \(m\) be a modulus of a number field \(K\) and \(\chi\) a ray class character of \(m\). If a nonzero fractional ideal \(\mathfrak a\) of \(K\) coprime to the finite part of \(m\) lies in the ray group of \(m\), then the value of \(\chi\) at the ray class of \(\mathfrak a\), regarded as a complex number, is \(1\).

theorem evalComplex_rayGroup (chi : RayClassCharacter m)
    (x : coprimeFractionalIdeals m) (h : x ∈ rayGroup m) :
    evalComplex chi (rayClassMap m x) = 1

Uses 6

Statement usesRay class character · Ray class group · Fractional ideals coprime to a modulus · Complex value of a ray class character · Ray class map · The ray group of a modulus

DefinitionExtension by zero of a ray class character#✓fully proved

Let \(\chi\) be a ray class character of a modulus \(m\) of a number field \(K\). Its extension by zero assigns to a nonzero fractional ideal \(\mathfrak a\) of \(K\) the complex number \(\chi([\mathfrak a])\) if \(\mathfrak a\) is coprime to the finite part of \(m\), where \([\mathfrak a]\) is the ray class of \(\mathfrak a\), and the value \(0\) otherwise.

noncomputable def extendByZero (chi : RayClassCharacter m)
    (I : (FractionalIdeal (𝓞 K)⁰ K)ˣ) : ℂ :=
  if h : I ∈ coprimeFractionalIdeals m then
    Circle.coeHom (chi (rayClassMap m ⟨I, h⟩))
  else
    0

Uses 5

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

TheoremExponents of a modulus grow under divisibility#✓fully proved

Let \(m_1\) and \(m_2\) be moduli of a number field \(K\) with \(m_1 \mid m_2\), that is, the finite part of \(m_2\) is contained in the finite part of \(m_1\) and every real place of \(m_1\) is a real place of \(m_2\). Then for every finite prime \(v\) of \(K\) (a height-one prime of the ring of integers \(\mathcal{O}_K\)), the exponent of \(v\) in the finite part of \(m_1\) is at most the exponent of \(v\) in the finite part of \(m_2\).

theorem finiteExponent_le_of_dvd (h : m1 ∣ m2)
    (v : IsDedekindDomain.HeightOneSpectrum (𝓞 K)) :
    finiteExponent m1 v ≤ finiteExponent m2 v

Uses 1 · Used by 1

Statement usesExponent of a modulus at a prime

Used byRay congruence to \(1\) passes to divisors of the modulus

DefinitionInclusion of coprime ideal groups under divisibility of moduli#✓fully proved

Let \(m_1\) and \(m_2\) be moduli of a number field \(K\) with \(m_1 \mid m_2\), that is, the finite part of \(m_2\) is contained in the finite part of \(m_1\) and every real place of \(m_1\) is a real place of \(m_2\). Then every fractional ideal of \(K\) coprime to \(m_2\) is coprime to \(m_1\), and this map is the inclusion homomorphism from the group of fractional ideals coprime to \(m_2\) into the group of fractional ideals coprime to \(m_1\).

def coprimeInclusion (h : m1 ∣ m2) :
    coprimeFractionalIdeals m2 →* coprimeFractionalIdeals m1 :=
  Subgroup.inclusion (coprime_le_of_dvd h)

Uses 2 · Used by 3

Statement usesFractional ideals coprime to a modulus · Primes dividing a modulus

Used byInduced characters agree on coprime ideals · Level-change map on ray class groups · The level-change map on ray classes

TheoremRay congruence to \(1\) passes to divisors of the modulus#✓fully proved

Let \(m_1\) and \(m_2\) be moduli of a number field \(K\) with \(m_1 \mid m_2\), that is, the finite part of \(m_2\) is contained in the finite part of \(m_1\) and every real place of \(m_1\) is a real place of \(m_2\). If a nonzero element \(x\) of \(K\) is congruent to \(1\) modulo \(m_2\) in the ray sense (its principal ideal is coprime to \(m_2\), for each prime \(v\) dividing the finite part of \(m_2\) either \(x = 1\) or the exponent of \(v\) in \(x - 1\) is at least its exponent in that finite part, and \(x\) is positive at every real place of \(m_2\)), then \(x\) is congruent to \(1\) modulo \(m_1\) in the same sense.

theorem IsRayElementOne.of_dvd (h : m1 ∣ m2) {x : Kˣ}
    (hx : IsRayElementOne m2 x) : IsRayElementOne m1 x

Uses 8 · Used by 1

Statement usesElements congruent to one modulo a modulus

Proof usesMultiplicative congruence to one at the finite part · Positivity at the infinite part of a modulus · Fractional ideals coprime to a modulus · Exponent of a modulus at a prime · Exponents of a modulus grow under divisibility · Primes dividing a modulus · Elements coprime to a modulus

Used byLevel-change map on ray class groups

DefinitionLevel-change map on ray class groups#✓fully proved

Let \(m_1\) and \(m_2\) be moduli of a number field \(K\) with \(m_1 \mid m_2\), that is, the finite part of \(m_2\) is contained in the finite part of \(m_1\) and every real place of \(m_1\) is a real place of \(m_2\). The inclusion of the group of fractional ideals coprime to \(m_2\) into the group of fractional ideals coprime to \(m_1\) maps the ray group modulo \(m_2\) into the ray group modulo \(m_1\), so it induces a group homomorphism from the ray class group modulo \(m_2\) to the ray class group modulo \(m_1\), sending the class of an ideal modulo \(m_2\) to its class modulo \(m_1\).

def RayClassGroup.mapOfDvd (h : m1 ∣ m2) : RayClassGroup m2 →* RayClassGroup m1 :=
  QuotientGroup.map (rayGroup m2) (rayGroup m1) (coprimeInclusion h) (rayGroup_le_comap_of_dvd h)

Uses 10 · Used by 4

Statement usesMultiplicative congruence to one at the finite part · Elements congruent to one modulo a modulus · Ray congruence to \(1\) passes to divisors of the modulus · Positivity at the infinite part of a modulus · Ray class group · Fractional ideals coprime to a modulus · Inclusion of coprime ideal groups under divisibility of moduli · Elements coprime to a modulus · Generators of the ray group · The ray group of a modulus

Used byInduced ray class character · Induced characters agree on coprime ideals · Primitivity in terms of the level-change map · The level-change map on ray classes

TheoremThe level-change map on ray classes#✓fully proved

Let \(m_1\) and \(m_2\) be moduli of a number field \(K\) with \(m_1 \mid m_2\), that is, the finite part of \(m_2\) is contained in the finite part of \(m_1\) and every real place of \(m_1\) is a real place of \(m_2\). For every fractional ideal \(\mathfrak{a}\) of \(K\) coprime to \(m_2\), the level-change homomorphism from the ray class group modulo \(m_2\) to the ray class group modulo \(m_1\) sends the ray class of \(\mathfrak{a}\) modulo \(m_2\) to the ray class of \(\mathfrak{a}\) modulo \(m_1\) (an ideal coprime to \(m_2\) is also coprime to \(m_1\)).

@[simp] theorem RayClassGroup.mapOfDvd_rayClassMap (h : m1 ∣ m2)
    (x : coprimeFractionalIdeals m2) :
    mapOfDvd h (rayClassMap m2 x) = rayClassMap m1 (coprimeInclusion h x)

Uses 6 · Used by 1

Statement usesRay class group · Level-change map on ray class groups · Fractional ideals coprime to a modulus · Inclusion of coprime ideal groups under divisibility of moduli · Ray class map · The ray group of a modulus

Used byInduced characters agree on coprime ideals

DefinitionInduced ray class character#✓fully proved

Let \(m_1\) and \(m_2\) be moduli of a number field \(K\) with \(m_1 \mid m_2\), that is, the finite part of \(m_2\) is contained in the finite part of \(m_1\) and every real place of \(m_1\) is a real place of \(m_2\). A ray class character \(\chi_2\) modulo \(m_2\) is induced by a ray class character \(\chi_1\) modulo \(m_1\) when \(\chi_2 = \chi_1 \circ \pi\), where \(\pi\) is the level-change homomorphism from the ray class group modulo \(m_2\) to the ray class group modulo \(m_1\) that sends the class of an ideal coprime to \(m_2\) to its class modulo \(m_1\).

def RayClassCharacter.IsInducedBy (chi2 : RayClassCharacter m2)
    (chi1 : RayClassCharacter m1) (h : m1 ∣ m2) : Prop :=
  chi2 = chi1.comp (RayClassGroup.mapOfDvd h)

Uses 5 · Used by 2

Statement usesRay class character · Ray class group · Level-change map on ray class groups · Fractional ideals coprime to a modulus · The ray group of a modulus

Used byInduced characters agree on coprime ideals · Primitive ray class character

TheoremInduced characters agree on coprime ideals#✓fully proved

Let \(m_1\) and \(m_2\) be moduli of a number field \(K\) with \(m_1 \mid m_2\), that is, the finite part of \(m_2\) is contained in the finite part of \(m_1\) and every real place of \(m_1\) is a real place of \(m_2\). Let \(\chi_1\) be a ray class character modulo \(m_1\) and \(\chi_2\) a ray class character modulo \(m_2\). Then \(\chi_2\) is induced by \(\chi_1\) if and only if, for every fractional ideal \(\mathfrak{a}\) of \(K\) coprime to \(m_2\), the value of \(\chi_2\) on the ray class of \(\mathfrak{a}\) modulo \(m_2\) equals the value of \(\chi_1\) on the ray class of \(\mathfrak{a}\) modulo \(m_1\) (an ideal coprime to \(m_2\) is also coprime to \(m_1\)).

theorem RayClassCharacter.isInducedBy_iff (chi2 : RayClassCharacter m2)
    (chi1 : RayClassCharacter m1) (h : m1 ∣ m2) :
    chi2.IsInducedBy chi1 h ↔ ∀ x : coprimeFractionalIdeals m2,
      pullback chi2 x = pullback chi1 (coprimeInclusion h x)

Uses 10

Statement usesRay class character · Induced ray class character · Fractional ideals coprime to a modulus · Inclusion of coprime ideal groups under divisibility of moduli · Pullback of a ray class character to ideals

Proof usesRay class group · Level-change map on ray class groups · The level-change map on ray classes · Ray class map · The ray group of a modulus

DefinitionPrimitive ray class character#✓fully proved

Let \(m\) be a modulus of a number field \(K\). A ray class character \(\chi\) modulo \(m\) is primitive when, for every modulus \(m_0\) of \(K\) with \(m_0 \mid m\) (the finite part of \(m\) is contained in the finite part of \(m_0\) and every real place of \(m_0\) is a real place of \(m\)) and every ray class character \(\chi_0\) modulo \(m_0\) by which \(\chi\) is induced, \(m_0 = m\).

def RayClassCharacter.IsPrimitive (chi : RayClassCharacter m2) : Prop :=
  ∀ (m0 : Modulus K) (chi0 : RayClassCharacter m0) (h : m0 ∣ m2),
    chi.IsInducedBy chi0 h → m0 = m2

Uses 2 · Used by 1

Statement usesRay class character · Induced ray class character

Used byPrimitivity in terms of the level-change map

TheoremPrimitivity in terms of the level-change map#✓fully proved

Let \(m\) be a modulus of a number field \(K\). A ray class character \(\chi\) modulo \(m\) is primitive if and only if, for every modulus \(m_0\) of \(K\) with \(m_0 \mid m\) (the finite part of \(m\) is contained in the finite part of \(m_0\) and every real place of \(m_0\) is a real place of \(m\)) and every ray class character \(\chi_0\) modulo \(m_0\) with \(\chi = \chi_0 \circ \pi\), where \(\pi\) is the level-change homomorphism from the ray class group modulo \(m\) to the ray class group modulo \(m_0\), we have \(m_0 = m\).

theorem RayClassCharacter.isPrimitive_iff (chi : RayClassCharacter m2) :
    chi.IsPrimitive ↔ ∀ (m0 : Modulus K) (chi0 : RayClassCharacter m0)
      (h : m0 ∣ m2), chi = chi0.comp (RayClassGroup.mapOfDvd h) → m0 = m2

Uses 6

Statement usesRay class character · Primitive ray class character · Ray class group · Level-change map on ray class groups · Fractional ideals coprime to a modulus · The ray group of a modulus

16 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.