Arakelov divisors

TheoremInvertible fractional ideals have nonzero absolute norm#✓fully proved

Let \(R\) be a Dedekind domain that is a free \(\mathbb{Z}\)-module of finite rank, and let \(F\) be its field of fractions. For every invertible fractional ideal \(I\) of \(R\) in \(F\), the absolute norm of \(I\), a rational number, is nonzero.

theorem absNorm_units_ne_zero (I : (FractionalIdeal R⁰ F)ˣ) :
    absNorm (I : FractionalIdeal R⁰ F) ≠ 0

Used by 1

Used byInvertible fractional ideals have positive absolute norm

TheoremInvertible fractional ideals have positive absolute norm#✓fully proved

Let \(R\) be a Dedekind domain that is a free \(\mathbb{Z}\)-module of finite rank, and let \(F\) be its field of fractions. For every invertible fractional ideal \(I\) of \(R\) in \(F\), the absolute norm of \(I\), a rational number, is positive.

theorem absNorm_units_pos (I : (FractionalIdeal R⁰ F)ˣ) :
    0 < absNorm (I : FractionalIdeal R⁰ F)

Uses 1 · Used by 2

Proof usesInvertible fractional ideals have nonzero absolute norm

Used byLarge Arakelov divisors have a nonzero section · Ideal norm of an Arakelov divisor

AbbreviationArakelov divisor#✓fully proved

Let \(K\) be a number field with ring of integers \(\mathcal{O}_K\). An Arakelov divisor on \(K\) is a pair \((I, r)\), where \(I\) is an invertible fractional ideal of \(\mathcal{O}_K\) in \(K\) and \(r\) assigns a positive real number \(r_w\) to each infinite place \(w\) of \(K\).

abbrev ArakelovDivisor :=
  (FractionalIdeal (𝓞 K)⁰ K)ˣ × (InfinitePlace K → { r : ℝ // 0 < r })

Used by 19

Used byArchimedean factor homomorphism · Archimedean factor · Archimedean factor as a real number · Degree-zero Arakelov divisors · Large Arakelov divisors have a nonzero section · Ideal norm homomorphism · Ideal norm of an Arakelov divisor · Real value of the ideal norm · Membership in the section set · Principal Arakelov divisor · Principal divisor homomorphism · Subgroup of principal Arakelov divisors · Principal Arakelov divisors have degree zero · Section set of an Arakelov divisor · Finiteness of section sets · Size of an Arakelov divisor · Size as a quotient of homomorphisms · Explicit formula for the size of an Arakelov divisor · Principal Arakelov divisors have size one

DefinitionArchimedean factor#✓fully proved

Let \(D = (I, r)\) be an Arakelov divisor on a number field \(K\). Its archimedean factor is the positive real number \(\prod_w r_w^{m_w}\), where the product runs over all infinite places \(w\) of \(K\) and \(m_w\) is \(1\) if \(w\) is real and \(2\) if \(w\) is complex.

noncomputable def ArakelovDivisor.archimedeanFactor (D : ArakelovDivisor K) :
    { r : ℝ // 0 < r } :=
  ∏ w : InfinitePlace K, D.2 w ^ w.mult

Uses 1 · Used by 3

Statement usesArakelov divisor

Used byArchimedean factor homomorphism · Archimedean factor as a real number · Explicit formula for the size of an Arakelov divisor

TheoremArchimedean factor as a real number#✓fully proved

Let \(D = (I, r)\) be an Arakelov divisor on a number field \(K\), and for each infinite place \(w\) of \(K\) let \(m_w\) be \(1\) if \(w\) is real and \(2\) if \(w\) is complex. Viewed as a real number, the archimedean factor of \(D\) equals the real product \(\prod_w r_w^{m_w}\) over all infinite places \(w\) of \(K\).

@[simp]
theorem ArakelovDivisor.archimedeanFactor_coe (D : ArakelovDivisor K) :
    (D.archimedeanFactor : ℝ) = ∏ w : InfinitePlace K, (D.2 w : ℝ) ^ w.mult

Uses 2 · Used by 2

Statement usesArakelov divisor · Archimedean factor

Used byArchimedean factor homomorphism · Explicit formula for the size of an Arakelov divisor

DefinitionIdeal norm of an Arakelov divisor#✓fully proved

For an Arakelov divisor \(D\) of a number field \(K\) with invertible fractional ideal \(I\), the ideal norm of \(D\) is the absolute norm \(N(I)\) of \(I\), regarded as a positive real number; it is positive because \(I\) is invertible.

noncomputable def ArakelovDivisor.idealNorm (D : ArakelovDivisor K) :
    { r : ℝ // 0 < r } :=
  ⟨((FractionalIdeal.absNorm (D.1 : FractionalIdeal (𝓞 K)⁰ K) : ℚ) : ℝ),
    by
      have h := FractionalIdeal.absNorm_units_pos (R := 𝓞 K) (F := K) D.1
      exact_mod_cast h⟩

Uses 2 · Used by 3

Statement usesInvertible fractional ideals have positive absolute norm · Arakelov divisor

Used byIdeal norm homomorphism · Real value of the ideal norm · Explicit formula for the size of an Arakelov divisor

TheoremReal value of the ideal norm#✓fully proved

For every Arakelov divisor \(D\) of a number field \(K\) with fractional ideal \(I\), the ideal norm of \(D\), viewed as a real number, equals the absolute norm \(N(I) \in \mathbb{Q}\) of \(I\), viewed as a real number.

@[simp]
theorem ArakelovDivisor.idealNorm_coe (D : ArakelovDivisor K) :
    (D.idealNorm : ℝ) =
      ((FractionalIdeal.absNorm (D.1 : FractionalIdeal (𝓞 K)⁰ K) : ℚ) : ℝ)

Uses 2 · Used by 2

Statement usesArakelov divisor · Ideal norm of an Arakelov divisor

Used byIdeal norm homomorphism · Explicit formula for the size of an Arakelov divisor

DefinitionArchimedean factor homomorphism#✓fully proved

For a number field \(K\), the map sending an Arakelov divisor on \(K\) to its archimedean factor is a monoid homomorphism from the Arakelov divisors on \(K\), multiplied componentwise, to the positive real numbers under multiplication.

NumberField.ArakelovDivisor.archHom · 18 lines

noncomputable def ArakelovDivisor.archHom :
    ArakelovDivisor K →* { r : ℝ // 0 < r } where
  toFun := ArakelovDivisor.archimedeanFactor K
  map_one' := Subtype.ext (by
    change ((ArakelovDivisor.archimedeanFactor K 1 : { r : ℝ // 0 < r }) : ℝ) =
      ((1 : { r : ℝ // 0 < r }) : ℝ)
    rw [ArakelovDivisor.archimedeanFactor_coe, Positive.val_one]
    simp)
  map_mul' D E := Subtype.ext (by
    change ((ArakelovDivisor.archimedeanFactor K (D * E) : { r : ℝ // 0 < r }) : ℝ) =
      ((ArakelovDivisor.archimedeanFactor K D * ArakelovDivisor.archimedeanFactor K E :
        { r : ℝ // 0 < r }) : ℝ)
    rw [ArakelovDivisor.archimedeanFactor_coe, Positive.val_mul,
      ArakelovDivisor.archimedeanFactor_coe, ArakelovDivisor.archimedeanFactor_coe,
      ← Finset.prod_mul_distrib]
    apply Finset.prod_congr rfl
    intro w _
    rw [Prod.snd_mul, Pi.mul_apply, Positive.val_mul, mul_pow])

Uses 3 · Used by 3

Statement usesArakelov divisor · Archimedean factor · Archimedean factor as a real number

Used bySize of an Arakelov divisor · Size as a quotient of homomorphisms · Explicit formula for the size of an Arakelov divisor

DefinitionIdeal norm homomorphism#✓fully proved

For a number field \(K\), the map sending an Arakelov divisor \((I, r)\) on \(K\) to the absolute norm of \(I\), viewed as a positive real number, is a monoid homomorphism from the Arakelov divisors on \(K\), multiplied componentwise, to the positive real numbers under multiplication.

NumberField.ArakelovDivisor.idealHom · 15 lines

noncomputable def ArakelovDivisor.idealHom :
    ArakelovDivisor K →* { r : ℝ // 0 < r } where
  toFun := ArakelovDivisor.idealNorm K
  map_one' := Subtype.ext (by
    change ((ArakelovDivisor.idealNorm K 1 : { r : ℝ // 0 < r }) : ℝ) =
      ((1 : { r : ℝ // 0 < r }) : ℝ)
    rw [ArakelovDivisor.idealNorm_coe, Positive.val_one, Prod.fst_one, Units.val_one,
      FractionalIdeal.absNorm_one, Rat.cast_one])
  map_mul' D E := Subtype.ext (by
    change ((ArakelovDivisor.idealNorm K (D * E) : { r : ℝ // 0 < r }) : ℝ) =
      ((ArakelovDivisor.idealNorm K D * ArakelovDivisor.idealNorm K E :
        { r : ℝ // 0 < r }) : ℝ)
    rw [ArakelovDivisor.idealNorm_coe, Positive.val_mul,
      ArakelovDivisor.idealNorm_coe, ArakelovDivisor.idealNorm_coe, Prod.fst_mul,
      Units.val_mul, map_mul, Rat.cast_mul])

Uses 3 · Used by 3

Statement usesArakelov divisor · Ideal norm of an Arakelov divisor · Real value of the ideal norm

Used bySize of an Arakelov divisor · Size as a quotient of homomorphisms · Explicit formula for the size of an Arakelov divisor

DefinitionSize of an Arakelov divisor#✓fully proved

For a number field \(K\), the size homomorphism sends an Arakelov divisor \(D = (I, (r_w)_w)\), with \(I\) an invertible fractional ideal of the ring of integers of \(K\) and \(r_w > 0\) for each infinite place \(w\), to the positive real number \(\prod_w r_w^{m_w} / N(I)\), where \(w\) runs over the infinite places of \(K\), \(m_w\) is \(1\) for a real place and \(2\) for a complex place, and \(N(I)\) is the absolute norm of \(I\). It is a group homomorphism from Arakelov divisors to the multiplicative group of positive reals.

noncomputable def ArakelovDivisor.sizeHom :
    ArakelovDivisor K →* { r : ℝ // 0 < r } :=
  ArakelovDivisor.archHom K / ArakelovDivisor.idealHom K

Uses 3 · Used by 6

Statement usesArakelov divisor · Archimedean factor homomorphism · Ideal norm homomorphism

Used byDegree-zero Arakelov divisors · Large Arakelov divisors have a nonzero section · Principal Arakelov divisors have degree zero · Size as a quotient of homomorphisms · Explicit formula for the size of an Arakelov divisor · Principal Arakelov divisors have size one

TheoremSize as a quotient of homomorphisms#✓fully proved

For every Arakelov divisor \(D\) of a number field \(K\), the size of \(D\) equals the archimedean-factor homomorphism evaluated at \(D\) divided by the ideal-norm homomorphism evaluated at \(D\), the quotient taken in the group of positive reals.

@[simp]
theorem ArakelovDivisor.sizeHom_apply (D : ArakelovDivisor K) :
    ArakelovDivisor.sizeHom K D =
      ArakelovDivisor.archHom K D / ArakelovDivisor.idealHom K D

Uses 4 · Used by 1

Statement usesArakelov divisor · Archimedean factor homomorphism · Ideal norm homomorphism · Size of an Arakelov divisor

Used byExplicit formula for the size of an Arakelov divisor

TheoremExplicit formula for the size of an Arakelov divisor#✓fully proved

Let \(D = (I, (r_w)_w)\) be an Arakelov divisor of a number field \(K\), where \(I\) is an invertible fractional ideal of the ring of integers of \(K\) and \(r_w > 0\) for each infinite place \(w\) of \(K\). For each \(w\) let \(m_w\) be \(1\) if \(w\) is real and \(2\) if \(w\) is complex, and let \(N(I)\) be the absolute norm of \(I\). Then the size of \(D\), as a real number, is

\[\frac{\prod_w r_w^{m_w}}{N(I)},\]

where the product runs over all infinite places \(w\) of \(K\).

theorem ArakelovDivisor.sizeHom_coe (D : ArakelovDivisor K) :
    (ArakelovDivisor.sizeHom K D : ℝ) =
      (∏ w : InfinitePlace K, (D.2 w : ℝ) ^ w.mult) /
        ((FractionalIdeal.absNorm (D.1 : FractionalIdeal (𝓞 K)⁰ K) : ℚ) : ℝ)

Uses 9 · Used by 2

Statement usesArakelov divisor · Size of an Arakelov divisor

Proof usesArchimedean factor homomorphism · Archimedean factor · Archimedean factor as a real number · Ideal norm homomorphism · Ideal norm of an Arakelov divisor · Real value of the ideal norm · Size as a quotient of homomorphisms

Used byLarge Arakelov divisors have a nonzero section · Principal Arakelov divisors have size one

DefinitionSection set of an Arakelov divisor#✓fully proved

Let \(D\) be an Arakelov divisor of a number field \(K\), with invertible fractional ideal \(I\) and positive real number \(r_w\) at each infinite place \(w\) of \(K\). The section set of \(D\) is the set of \(x \in I\) such that \(w(x) \le r_w\) for every infinite place \(w\) of \(K\).

At a complex place the bound is on \(w(x)\) itself, not on \(w(x)^2\); the squaring at complex places enters only in the size of \(D\).

noncomputable def ArakelovDivisor.sectionSet (D : ArakelovDivisor K) : Set K :=
  { x | x ∈ (D.1 : FractionalIdeal (𝓞 K)⁰ K) ∧
    ∀ w : InfinitePlace K, w x ≤ (D.2 w : ℝ) }

Uses 1 · Used by 3

Statement usesArakelov divisor

Used byLarge Arakelov divisors have a nonzero section · Membership in the section set · Finiteness of section sets

TheoremMembership in the section set#✓fully proved

Let \(D\) be an Arakelov divisor of a number field \(K\), with invertible fractional ideal \(I\) and positive real number \(r_w\) at each infinite place \(w\) of \(K\). An element \(x \in K\) lies in the section set of \(D\) if and only if \(x \in I\) and \(w(x) \le r_w\) for every infinite place \(w\) of \(K\).

@[simp]
theorem ArakelovDivisor.mem_sectionSet (D : ArakelovDivisor K) (x : K) :
    x ∈ D.sectionSet ↔
      x ∈ (D.1 : FractionalIdeal (𝓞 K)⁰ K) ∧
        ∀ w : InfinitePlace K, w x ≤ (D.2 w : ℝ)

Uses 2 · Used by 1

Statement usesArakelov divisor · Section set of an Arakelov divisor

Used byFiniteness of section sets

TheoremFiniteness of section sets#✓fully proved

For every Arakelov divisor \(D\) of a number field \(K\), the section set of \(D\) is finite.

Multiplying by a nonzero \(d \in \mathcal{O}_K\) that clears the denominators of the fractional ideal of \(D\) sends the section set into \(\mathcal{O}_K\), and the bounds at the infinite places give a uniform bound \(B\) on \(|\sigma(dx)|\) for all \(x\) in the section set and all complex embeddings \(\sigma\) of \(K\); only finitely many algebraic integers of \(K\) have all conjugates of absolute value at most \(B\).

theorem ArakelovDivisor.sectionSet_finite (D : ArakelovDivisor K) :
    D.sectionSet.Finite

Uses 3

Statement usesArakelov divisor · Section set of an Arakelov divisor

Proof usesMembership in the section set

DefinitionArchimedean part of a principal divisor#✓fully proved

For a nonzero element \(x\) of a number field \(K\), this is the family that assigns to each infinite place \(w\) of \(K\) the positive real number \(w(x)\).

noncomputable def principalArch (x : Kˣ) : InfinitePlace K → { r : ℝ // 0 < r } :=
  fun w => ⟨w (x : K), InfinitePlace.pos_iff.mpr (Units.ne_zero x)⟩

Used by 2

Used byPrincipal Arakelov divisor · Principal divisor homomorphism

DefinitionPrincipal Arakelov divisor#✓fully proved

For a nonzero element \(x\) of a number field \(K\), the principal Arakelov divisor of \(x\) consists of the principal fractional ideal \(x\mathcal{O}_K\) together with the positive real number \(w(x)\) at each infinite place \(w\) of \(K\).

noncomputable def principalDivisor (x : Kˣ) : ArakelovDivisor K :=
  (toPrincipalIdeal (𝓞 K) K x, principalArch K x)

Uses 2 · Used by 4

Statement usesArakelov divisor · Archimedean part of a principal divisor

Used byFinite component of a principal divisor · Infinite component of a principal divisor · Principal divisor homomorphism · Principal Arakelov divisors have size one

TheoremInfinite component of a principal divisor#✓fully proved

Let \(K\) be a number field, \(x \in K\) nonzero and \(w\) an infinite place of \(K\). The positive real number that the principal Arakelov divisor of \(x\) assigns to \(w\) is \(w(x)\), the absolute value of \(x\) at \(w\).

@[simp]
theorem coe_principalDivisor_snd (x : Kˣ) (w : InfinitePlace K) :
    (((principalDivisor K x).2 w : { r : ℝ // 0 < r }) : ℝ) = w (x : K)

Uses 1

Statement usesPrincipal Arakelov divisor

TheoremFinite component of a principal divisor#✓fully proved

Let \(K\) be a number field with ring of integers \(\mathcal{O}_K\). For every nonzero \(x \in K\), the fractional ideal component of the principal Arakelov divisor of \(x\) is the principal fractional ideal \(x\mathcal{O}_K\).

theorem coe_principalDivisor_fst (x : Kˣ) :
    ((principalDivisor K x).1 : FractionalIdeal (𝓞 K)⁰ K) =
      FractionalIdeal.spanSingleton (𝓞 K)⁰ (x : K)

Uses 1 · Used by 1

Statement usesPrincipal Arakelov divisor

Used byPrincipal Arakelov divisors have size one

DefinitionPrincipal divisor homomorphism#✓fully proved

For a number field \(K\), the map sending a nonzero element \(x \in K\) to its principal Arakelov divisor is a group homomorphism from the multiplicative group \(K^\times\) to the group of Arakelov divisors of \(K\).

NumberField.principalHom · 21 lines

noncomputable def principalHom : Kˣ →* ArakelovDivisor K where
  toFun := principalDivisor K
  map_one' := by
    apply Prod.ext
    · change toPrincipalIdeal (𝓞 K) K 1 = 1
      exact map_one _
    · funext w
      apply Subtype.ext
      change w (((1 : Kˣ) : K)) = ((1 : InfinitePlace K → { r : ℝ // 0 < r }) w : ℝ)
      rw [Units.val_one, Pi.one_apply, Positive.val_one]
      exact map_one w
  map_mul' x y := by
    apply Prod.ext
    · change toPrincipalIdeal (𝓞 K) K (x * y) = _
      rw [map_mul]
      rfl
    · funext w
      apply Subtype.ext
      change w (((x * y : Kˣ) : K)) = ((principalArch K x * principalArch K y) w : ℝ)
      rw [Units.val_mul, Pi.mul_apply, Positive.val_mul]
      exact map_mul w _ _

Uses 3 · Used by 3

Statement usesArakelov divisor · Archimedean part of a principal divisor · Principal Arakelov divisor

Used bySubgroup of principal Arakelov divisors · Principal Arakelov divisors have degree zero · Principal Arakelov divisors have size one

DefinitionSubgroup of principal Arakelov divisors#✓fully proved

For a number field \(K\), the principal subgroup is the image of the principal divisor homomorphism, that is, the subgroup of the group of Arakelov divisors of \(K\) consisting of the principal Arakelov divisors of the nonzero elements of \(K\).

noncomputable def principalSubgroup : Subgroup (ArakelovDivisor K) := (principalHom K).range

Uses 2 · Used by 1

Statement usesArakelov divisor · Principal divisor homomorphism

Used byPrincipal Arakelov divisors have degree zero

DefinitionDegree-zero Arakelov divisors#✓fully proved

For a number field \(K\), the degree-zero subgroup of the group of Arakelov divisors on \(K\) is the kernel of the size homomorphism, that is, the subgroup of Arakelov divisors of size \(1\).

noncomputable def degreeZero : Subgroup (ArakelovDivisor K) := (ArakelovDivisor.sizeHom K).ker

Uses 2 · Used by 1

Statement usesArakelov divisor · Size of an Arakelov divisor

Used byPrincipal Arakelov divisors have degree zero

TheoremPrincipal Arakelov divisors have size one#✓fully proved

Let \(K\) be a number field with ring of integers \(\mathcal{O}_K\). For every nonzero \(x \in K\), the principal Arakelov divisor of \(x\), formed by the principal fractional ideal \(x\mathcal{O}_K\) and the values \(w(x)\) at the infinite places \(w\) of \(K\), has size \(1\).

This is the product formula: with \(m_w\) equal to \(1\) at real and \(2\) at complex places, the archimedean factor \(\prod_w w(x)^{m_w}\) equals \(|N_{K/\mathbb{Q}}(x)|\), where \(N_{K/\mathbb{Q}}\) is the field norm from \(K\) to \(\mathbb{Q}\), and so does the absolute norm of \(x\mathcal{O}_K\).

theorem size_principal (x : Kˣ) : ArakelovDivisor.sizeHom K (principalHom K x) = 1

Uses 6 · Used by 1

Statement usesArakelov divisor · Size of an Arakelov divisor · Principal divisor homomorphism

Proof usesExplicit formula for the size of an Arakelov divisor · Finite component of a principal divisor · Principal Arakelov divisor

Used byPrincipal Arakelov divisors have degree zero

TheoremPrincipal Arakelov divisors have degree zero#✓fully proved

For a number field \(K\), the subgroup of principal Arakelov divisors of \(K\) is contained in the degree-zero subgroup.

theorem principalSubgroup_le_degreeZero : principalSubgroup K ≤ degreeZero K

Uses 6

Statement usesArakelov divisor · Degree-zero Arakelov divisors · Subgroup of principal Arakelov divisors

Proof usesSize of an Arakelov divisor · Principal divisor homomorphism · Principal Arakelov divisors have size one

TheoremLarge Arakelov divisors have a nonzero section#✓fully proved

Let \(K\) be a number field with \(s\) complex places and discriminant \(d_K\), and let \(D\) be an Arakelov divisor on \(K\). If the size of \(D\) is strictly greater than \((2/\pi)^s \sqrt{|d_K|}\), then the section set of \(D\) contains a nonzero element of \(K\).

theorem ArakelovDivisor.exists_ne_zero_mem_sectionSet_of_size_gt
    (D : ArakelovDivisor K)
    (hD : (2 / Real.pi) ^ InfinitePlace.nrComplexPlaces K *
        Real.sqrt |(NumberField.discr K : ℝ)| <
      (ArakelovDivisor.sizeHom K D : ℝ)) :
    ∃ x ∈ D.sectionSet, x ≠ 0

Sources

• Proposition 15.9 of ATLAS NumberTheoryI.

Uses 5

Statement usesArakelov divisor · Section set of an Arakelov divisor · Size of an Arakelov divisor

Proof usesInvertible fractional ideals have positive absolute norm · Explicit formula for the size of an Arakelov divisor

25 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.