7.5. The Kummer logarithm determinant🔗

The p-adic part of the argument studies the logarithms of the real cyclotomic units at the prime above p. After passing to the completed local ring and reducing suitable logarithmic coordinates modulo p, one obtains a matrix over \mathbb{F}_p. Its columns are indexed by the generators \varepsilon_2,\ldots,\varepsilon_{(p-1)/2}, and its rows are indexed by the even powers which occur in the Kummer range.

The determinant has two parts. One part is a finite-field Vandermonde determinant in the Teichmuller nodes; this is nonzero because the nodes are distinct. The other part is the product of Bernoulli factors. Consequently the determinant is nonzero exactly when no Bernoulli numerator in Kummer's range is divisible by p.

Theorem7.5.1

Statement uses 3

Statement dependency previews

Preview

Theorem 3.4.1.1

Loading preview

Statement dependency preview content is loaded from the Blueprint HTML cache.

used by 1✓L∃∀N

Kummer logarithm determinant criterion. Assume p\ge 5. The Kummer logarithm matrix has nonzero determinant if and only if \forall j,\quad 1\le j,\ 2j\le p-3 \Longrightarrow p\nmid (B_{2j})_{\mathrm{num}}.

Definition 7.2.1 Theorem 3.4.1.1 Corollary 3.4.1.2

Lean code for Theorem7.5.1●5 theorems

theoremdefined in BernoulliRegular/CyclotomicUnits/KummerLogDeterminant.lean

complete

theorem BernoulliRegular.CyclotomicUnits.kummerLogMatrix_det_ne_zero_iff_bernoulli_nonzero.{u_1}
  (p : ℕ) [Fact (Nat.Prime p)] (K : Type u_1) [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K] [NumberField.IsCMField K]
  (hp_three : 3 ≤ p) (hp_five : 5 ≤ p) :
  (BernoulliRegular.CyclotomicUnits.concreteKummerLogMatrix p K hp_three
          hp_five).det ≠
      0 ↔
    ∀ (j : ℕ), 1 ≤ j → 2 * j ≤ p - 3 → ¬↑p ∣ (bernoulli (2 * j)).num

theorem BernoulliRegular.CyclotomicUnits.kummerLogMatrix_det_ne_zero_iff_bernoulli_nonzero.{u_1}
  (p : ℕ) [Fact (Nat.Prime p)]
  (K : Type u_1) [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K]
  [NumberField.IsCMField K]
  (hp_three : 3 ≤ p) (hp_five : 5 ≤ p) :
  (BernoulliRegular.CyclotomicUnits.concreteKummerLogMatrix
          p K hp_three hp_five).det ≠
      0 ↔
    ∀ (j : ℕ),
      1 ≤ j →
        2 * j ≤ p - 3 →
          ¬↑p ∣ (bernoulli (2 * j)).num

CU-13: Kummer's logarithm determinant is nonzero exactly when all
Bernoulli numerators in the classical even range are prime to `p`.

theoremdefined in BernoulliRegular/CyclotomicUnits/KummerLogDeterminant.lean

complete

theorem BernoulliRegular.CyclotomicUnits.concreteKummerLogMatrix_eq_diagonal_mul_vandermonde.{u_1}
  (p : ℕ) [Fact (Nat.Prime p)] (K : Type u_1) [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K] [NumberField.IsCMField K]
  (hp_three : 3 ≤ p) (hp_five : 5 ≤ p) :
  BernoulliRegular.CyclotomicUnits.concreteKummerLogMatrix p K hp_three
      hp_five =
    Matrix.diagonal
        (BernoulliRegular.CyclotomicUnits.kummerLogDetRowFactor p) *
      BernoulliRegular.CyclotomicUnits.vandermondeTeichmullerEvenSubOneMatrix
        p hp_three

theorem BernoulliRegular.CyclotomicUnits.concreteKummerLogMatrix_eq_diagonal_mul_vandermonde.{u_1}
  (p : ℕ) [Fact (Nat.Prime p)]
  (K : Type u_1) [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K]
  [NumberField.IsCMField K]
  (hp_three : 3 ≤ p) (hp_five : 5 ≤ p) :
  BernoulliRegular.CyclotomicUnits.concreteKummerLogMatrix
      p K hp_three hp_five =
    Matrix.diagonal
        (BernoulliRegular.CyclotomicUnits.kummerLogDetRowFactor
          p) *
      BernoulliRegular.CyclotomicUnits.vandermondeTeichmullerEvenSubOneMatrix
        p hp_three

The concrete Kummer logarithm matrix factors as a diagonal matrix of row
Bernoulli factors times the finite-field Vandermonde matrix from CU-12.

theoremdefined in BernoulliRegular/CyclotomicUnits/KummerLogDeterminant.lean

complete

theorem BernoulliRegular.CyclotomicUnits.concreteKummerLogMatrix_det_ne_zero_iff_forall_bernoulliFactor_ne_zero.{u_1}
  (p : ℕ) [Fact (Nat.Prime p)] (K : Type u_1) [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K] [NumberField.IsCMField K]
  (hp_three : 3 ≤ p) (hp_five : 5 ≤ p) :
  (BernoulliRegular.CyclotomicUnits.concreteKummerLogMatrix p K hp_three
          hp_five).det ≠
      0 ↔
    ∀ (j : Fin (BernoulliRegular.CyclotomicUnits.kummerLogRank p)),
      BernoulliRegular.CyclotomicUnits.bernoulliFactor p
          (BernoulliRegular.CyclotomicUnits.kummerLogRowIndex p j) ≠
        0

theorem BernoulliRegular.CyclotomicUnits.concreteKummerLogMatrix_det_ne_zero_iff_forall_bernoulliFactor_ne_zero.{u_1}
  (p : ℕ) [Fact (Nat.Prime p)]
  (K : Type u_1) [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K]
  [NumberField.IsCMField K]
  (hp_three : 3 ≤ p) (hp_five : 5 ≤ p) :
  (BernoulliRegular.CyclotomicUnits.concreteKummerLogMatrix
          p K hp_three hp_five).det ≠
      0 ↔
    ∀
      (j :
        Fin
          (BernoulliRegular.CyclotomicUnits.kummerLogRank
            p)),
      BernoulliRegular.CyclotomicUnits.bernoulliFactor
          p
          (BernoulliRegular.CyclotomicUnits.kummerLogRowIndex
            p j) ≠
        0

Kummer determinant nonvanishing reduced to the Bernoulli factors in each
matrix row.

theoremdefined in BernoulliRegular/CyclotomicUnits/KummerLogDeterminant.lean

complete

theorem BernoulliRegular.CyclotomicUnits.bernoulliFactor_ne_zero_iff_not_dvd_bernoulli_num
  (p : ℕ) [Fact (Nat.Prime p)] {j : ℕ} (hj : 1 ≤ j)
  (hjp : 2 * j ≤ p - 3) :
  BernoulliRegular.CyclotomicUnits.bernoulliFactor p j ≠ 0 ↔
    ¬↑p ∣ (bernoulli (2 * j)).num

theorem BernoulliRegular.CyclotomicUnits.bernoulliFactor_ne_zero_iff_not_dvd_bernoulli_num
  (p : ℕ) [Fact (Nat.Prime p)] {j : ℕ}
  (hj : 1 ≤ j) (hjp : 2 * j ≤ p - 3) :
  BernoulliRegular.CyclotomicUnits.bernoulliFactor
        p j ≠
      0 ↔
    ¬↑p ∣ (bernoulli (2 * j)).num

In the Kummer range, reducing `B_(2j)/(2j)` modulo `p` is nonzero
exactly when the numerator of `B_(2j)` is not divisible by `p`.

theoremdefined in BernoulliRegular/CyclotomicUnits/Vandermonde.lean

complete

theorem BernoulliRegular.CyclotomicUnits.vandermonde_teichmuller_even_sub_one_det_ne_zero
  (p : ℕ) [Fact (Nat.Prime p)] (hp_three : 3 ≤ p) :
  (BernoulliRegular.CyclotomicUnits.vandermondeTeichmullerEvenSubOneMatrix
        p hp_three).det ≠
    0

theorem BernoulliRegular.CyclotomicUnits.vandermonde_teichmuller_even_sub_one_det_ne_zero
  (p : ℕ) [Fact (Nat.Prime p)]
  (hp_three : 3 ≤ p) :
  (BernoulliRegular.CyclotomicUnits.vandermondeTeichmullerEvenSubOneMatrix
        p hp_three).det ≠
    0

Proof for Theorem 7.5.1

uses 0

The determinant computation factors the matrix as \operatorname{diag}(r_1,\ldots,r_g)\,V, g=(p-3)/2, where V is the finite-field Vandermonde matrix attached to the even Teichmuller nodes and r_j is the Bernoulli row factor attached to B_{2j}/(2j). The determinant is therefore \det(V)\prod_j r_j. The Vandermonde determinant is nonzero because the Teichmuller nodes are pairwise distinct in \mathbb{F}_p. Thus the determinant is nonzero exactly when every r_j is nonzero. For 1\le j and 2j\le p-3, the denominator of B_{2j} is prime to p by the integrality results for Bernoulli numbers below the boundary. Also 2j<p. Hence reducing B_{2j}/(2j) modulo p gives zero exactly when the integer numerator of B_{2j} is divisible by p. This identifies the non-vanishing of all row factors with the displayed Bernoulli non-divisibility condition.

Theorem7.5.2

Statement uses 3

Statement dependency previews

Preview

Definition 7.2.1

Loading preview

Statement dependency preview content is loaded from the Blueprint HTML cache.

used by 1✓L∃∀N

Determinant non-vanishing gives saturation. Assume p\ge 5. If the Kummer logarithm determinant is nonzero, then C^+_{\mathrm{sq}} is p-saturated in E^+.

Definition 7.3.1 Definition 7.2.1 Theorem 7.3.2

Lean code for Theorem7.5.2●5 theorems

theoremdefined in BernoulliRegular/CyclotomicUnits/LogDomain.lean

complete

theorem BernoulliRegular.CyclotomicUnits.cyclotomicUnits_pSaturated_of_kummerLog_det_ne_zero.{u_1}
  {p : ℕ} [Fact (Nat.Prime p)] {K : Type u_1} [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K] [NumberField.IsCMField K]
  (hp_three : 3 ≤ p) (hp_five : 5 ≤ p)
  (hdet :
    (BernoulliRegular.CyclotomicUnits.concreteKummerLogMatrix p K
          hp_three hp_five).det ≠
      0) :
  BernoulliRegular.pSaturated (BernoulliRegular.CPlus hp_three)
    BernoulliRegular.EPlus p

theorem BernoulliRegular.CyclotomicUnits.cyclotomicUnits_pSaturated_of_kummerLog_det_ne_zero.{u_1}
  {p : ℕ} [Fact (Nat.Prime p)]
  {K : Type u_1} [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K]
  [NumberField.IsCMField K]
  (hp_three : 3 ≤ p) (hp_five : 5 ≤ p)
  (hdet :
    (BernoulliRegular.CyclotomicUnits.concreteKummerLogMatrix
          p K hp_three hp_five).det ≠
      0) :
  BernoulliRegular.pSaturated
    (BernoulliRegular.CPlus hp_three)
    BernoulliRegular.EPlus p

CU-14f: Kummer matrix determinant nonvanishing gives exact `p`-saturation
of the real cyclotomic-unit subgroup in the full real-unit group.

theoremdefined in BernoulliRegular/CyclotomicUnits/LogDomain.lean

complete

theorem BernoulliRegular.CyclotomicUnits.completedLog_relation_of_CPlus_product_mem_powers.{u_1}
  {p : ℕ} [Fact (Nat.Prime p)] {K : Type u_1} [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K] [NumberField.IsCMField K]
  (hp_odd : p ≠ 2) (hp_three : 3 ≤ p) (s : ℤ)
  (e : Fin (BernoulliRegular.CyclotomicUnits.kummerLogRank p) → ℤ)
  (hpow :
    BernoulliRegular.CPlusExponentProduct hp_three s e ∈
      BernoulliRegular.pPowerSubgroup BernoulliRegular.EPlus p) :
  ∃ y,
    p • y =
      ∑ a,
        e a •
          BernoulliRegular.CyclotomicUnits.kummerLogFixedColumn p K
            hp_three a

theorem BernoulliRegular.CyclotomicUnits.completedLog_relation_of_CPlus_product_mem_powers.{u_1}
  {p : ℕ} [Fact (Nat.Prime p)]
  {K : Type u_1} [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K]
  [NumberField.IsCMField K]
  (hp_odd : p ≠ 2) (hp_three : 3 ≤ p)
  (s : ℤ)
  (e :
    Fin
        (BernoulliRegular.CyclotomicUnits.kummerLogRank
          p) →
      ℤ)
  (hpow :
    BernoulliRegular.CPlusExponentProduct
        hp_three s e ∈
      BernoulliRegular.pPowerSubgroup
        BernoulliRegular.EPlus p) :
  ∃ y,
    p • y =
      ∑ a,
        e a •
          BernoulliRegular.CyclotomicUnits.kummerLogFixedColumn
            p K hp_three a

CU-14b3: a `CPlus` exponent product that is a `p`th power in `EPlus`
gives a `p`-divisible completed logarithm relation in the fixed Dwork
subalgebra.

theoremdefined in BernoulliRegular/CyclotomicUnits/LogDomain.lean

complete

theorem BernoulliRegular.CyclotomicUnits.concreteKummerLogMatrix_mulVec_exponents_eq_zero.{u_1}
  {p : ℕ} [Fact (Nat.Prime p)] {K : Type u_1} [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K] [NumberField.IsCMField K]
  (hp_three : 3 ≤ p) (hp_five : 5 ≤ p)
  (e : Fin (BernoulliRegular.CyclotomicUnits.kummerLogRank p) → ℤ)
  (hlog :
    ∃ y,
      p • y =
        ∑ a,
          e a •
            BernoulliRegular.CyclotomicUnits.concreteKummerLogVector p K
              hp_three a) :
  ((BernoulliRegular.CyclotomicUnits.concreteKummerLogMatrix p K
          hp_three hp_five).mulVec
      fun a ↦ ↑(e a)) =
    0

theorem BernoulliRegular.CyclotomicUnits.concreteKummerLogMatrix_mulVec_exponents_eq_zero.{u_1}
  {p : ℕ} [Fact (Nat.Prime p)]
  {K : Type u_1} [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K]
  [NumberField.IsCMField K]
  (hp_three : 3 ≤ p) (hp_five : 5 ≤ p)
  (e :
    Fin
        (BernoulliRegular.CyclotomicUnits.kummerLogRank
          p) →
      ℤ)
  (hlog :
    ∃ y,
      p • y =
        ∑ a,
          e a •
            BernoulliRegular.CyclotomicUnits.concreteKummerLogVector
              p K hp_three a) :
  ((BernoulliRegular.CyclotomicUnits.concreteKummerLogMatrix
          p K hp_three hp_five).mulVec
      fun a ↦ ↑(e a)) =
    0

CU-14c: extracting Kummer coordinates from a `p`-divisible completed-log
relation gives the concrete Kummer matrix kernel equation over `ZMod p`.

theoremdefined in BernoulliRegular/CyclotomicUnits/KummerLogLinearAlgebra.lean

complete

theorem BernoulliRegular.CyclotomicUnits.exponents_modP_eq_zero_of_kummerLogMatrix_relation.{u_1}
  (p : ℕ) [Fact (Nat.Prime p)] (K : Type u_1) [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K] [NumberField.IsCMField K]
  (hp_three : 3 ≤ p) (hp_five : 5 ≤ p)
  (e : Fin (BernoulliRegular.CyclotomicUnits.kummerLogRank p) → ℤ)
  (hdet :
    (BernoulliRegular.CyclotomicUnits.concreteKummerLogMatrix p K
          hp_three hp_five).det ≠
      0)
  (hrel :
    ((BernoulliRegular.CyclotomicUnits.concreteKummerLogMatrix p K
            hp_three hp_five).mulVec
        fun a ↦ ↑(e a)) =
      0)
  (a : Fin (BernoulliRegular.CyclotomicUnits.kummerLogRank p)) :
  ↑(e a) = 0

theorem BernoulliRegular.CyclotomicUnits.exponents_modP_eq_zero_of_kummerLogMatrix_relation.{u_1}
  (p : ℕ) [Fact (Nat.Prime p)]
  (K : Type u_1) [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K]
  [NumberField.IsCMField K]
  (hp_three : 3 ≤ p) (hp_five : 5 ≤ p)
  (e :
    Fin
        (BernoulliRegular.CyclotomicUnits.kummerLogRank
          p) →
      ℤ)
  (hdet :
    (BernoulliRegular.CyclotomicUnits.concreteKummerLogMatrix
          p K hp_three hp_five).det ≠
      0)
  (hrel :
    ((BernoulliRegular.CyclotomicUnits.concreteKummerLogMatrix
            p K hp_three hp_five).mulVec
        fun a ↦ ↑(e a)) =
      0)
  (a :
    Fin
      (BernoulliRegular.CyclotomicUnits.kummerLogRank
        p)) :
  ↑(e a) = 0

If the concrete Kummer matrix has nonzero determinant, every vector in its
right kernel has all coordinates zero.

theoremdefined in BernoulliRegular/CyclotomicUnits/LogDomain.lean

complete

theorem BernoulliRegular.CyclotomicUnits.CPlusGenerator_exponents_modP_zero_of_kummerLog_det_ne_zero.{u_1}
  {p : ℕ} [Fact (Nat.Prime p)] {K : Type u_1} [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K] [NumberField.IsCMField K]
  (hp_three : 3 ≤ p) (hp_five : 5 ≤ p) (s : ℤ)
  (e : Fin (BernoulliRegular.CyclotomicUnits.kummerLogRank p) → ℤ)
  (hdet :
    (BernoulliRegular.CyclotomicUnits.concreteKummerLogMatrix p K
          hp_three hp_five).det ≠
      0)
  (hpow :
    BernoulliRegular.CPlusExponentProduct hp_three s e ∈
      BernoulliRegular.pPowerSubgroup BernoulliRegular.EPlus p)
  (a : Fin (BernoulliRegular.CyclotomicUnits.kummerLogRank p)) :
  ↑(e a) = 0

theorem BernoulliRegular.CyclotomicUnits.CPlusGenerator_exponents_modP_zero_of_kummerLog_det_ne_zero.{u_1}
  {p : ℕ} [Fact (Nat.Prime p)]
  {K : Type u_1} [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K]
  [NumberField.IsCMField K]
  (hp_three : 3 ≤ p) (hp_five : 5 ≤ p)
  (s : ℤ)
  (e :
    Fin
        (BernoulliRegular.CyclotomicUnits.kummerLogRank
          p) →
      ℤ)
  (hdet :
    (BernoulliRegular.CyclotomicUnits.concreteKummerLogMatrix
          p K hp_three hp_five).det ≠
      0)
  (hpow :
    BernoulliRegular.CPlusExponentProduct
        hp_three s e ∈
      BernoulliRegular.pPowerSubgroup
        BernoulliRegular.EPlus p)
  (a :
    Fin
      (BernoulliRegular.CyclotomicUnits.kummerLogRank
        p)) :
  ↑(e a) = 0

CU-14e: determinant nonvanishing forces the generator exponents in a
`p`th-power relation to vanish modulo `p`.

Proof for Theorem 7.5.2

uses 0

Suppose an element x=(-1)^s\prod_a \varepsilon_a^{e_a} is a p-th power in E^+. Taking completed p-adic logarithms of the local image of this relation gives an additive relation \sum_a e_a\,\log(\varepsilon_a) \in p\cdot L, where L is the completed logarithm lattice. The sign term disappears from the logarithmic coordinates, because p is odd and the sign is torsion. Reducing the coordinates of this relation modulo p gives M\,(e_a\bmod p)_a=0 for the Kummer logarithm matrix M. If \det(M)\ne0, then M is invertible over \mathbb{F}_p, so every coordinate e_a\bmod p is zero. The exponent criterion of Theorem 7.3.2 then proves p-saturation.