Kummer's Criterion and Regular Primes in Lean

7.7. The needed Sinnott index formula🔗

The index theorem used in the final argument is the odd-primary consequence of Sinnott's formula for real cyclotomic units. The family used in the regulator computation is the same squared family as above, but with the torsion subgroup adjoined explicitly.

Definition7.7.1
Statement uses 2
Statement dependency previews
Preview
Definition 7.1.2
Loading preview
Statement dependency preview content is loaded from the Blueprint HTML cache.
Used by 3
Reverse dependency previews
Preview
Lemma 7.7.2
Loading preview
Reverse dependency preview content is loaded from the Blueprint HTML cache.
✓L∃∀N

Sinnott's full-rank subgroup. For p\ge3, let C^+_{\mathrm{Sin}} = \left\langle \varepsilon_2,\varepsilon_3,\ldots,\varepsilon_{(p-1)/2} \right\rangle \vee E^+_{\mathrm{tors}} \le E^+ . Equivalently, C^+_{\mathrm{Sin}} is generated by the full-rank real cyclotomic-unit family used in the regulator determinant, together with all torsion units of E^+.

Definition 7.1.2 Definition 7.2.1

Lean code for Definition7.7.1●1 definition
  • defdefined in BernoulliRegular/CyclotomicUnits/IndexFormula.lean
    complete
    def BernoulliRegular.cyclotomicUnitIndexSubgroup {p : ℕ}
  [Fact (Nat.Prime p)] {K : Type} [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K] [NumberField.IsCMField K]
  (hp_odd : p ≠ 2) (hp_three : 3 ≤ p) :
  Subgroup
    (NumberField.RingOfIntegers ↥(NumberField.maximalRealSubfield K))ˣ
    def BernoulliRegular.cyclotomicUnitIndexSubgroup
  {p : ℕ} [Fact (Nat.Prime p)] {K : Type}
  [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K]
  [NumberField.IsCMField K]
  (hp_odd : p ≠ 2) (hp_three : 3 ≤ p) :
  Subgroup
    (NumberField.RingOfIntegers
        ↥(NumberField.maximalRealSubfield
            K))ˣ
    The full-rank real cyclotomic-unit subgroup used by the existing Sinnott
regulator/index infrastructure: the family generated by the squared real
cyclotomic units, together with torsion in `K⁺`.
Lemma7.7.2
Statement uses 2
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

Agreement with the squared subgroup. For p\ge3, C^+_{\mathrm{Sin}}=C^+_{\mathrm{sq}}.

Definition 7.7.1 Definition 7.2.1

Lean code for Lemma7.7.2●6 theorems
  • theoremdefined in BernoulliRegular/CyclotomicUnits/NormalizedIndex.lean
    complete
    theorem BernoulliRegular.cyclotomicUnitIndexSubgroup_eq_CPlus {p : ℕ}
  [Fact (Nat.Prime p)] {K : Type} [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K] [NumberField.IsCMField K]
  (hp_odd : p ≠ 2) (hp_three : 3 ≤ p) :
  BernoulliRegular.cyclotomicUnitIndexSubgroup hp_odd hp_three =
    BernoulliRegular.CPlus hp_three
    theorem BernoulliRegular.cyclotomicUnitIndexSubgroup_eq_CPlus
  {p : ℕ} [Fact (Nat.Prime p)] {K : Type}
  [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K]
  [NumberField.IsCMField K]
  (hp_odd : p ≠ 2) (hp_three : 3 ≤ p) :
  BernoulliRegular.cyclotomicUnitIndexSubgroup
      hp_odd hp_three =
    BernoulliRegular.CPlus hp_three
  • theoremdefined in BernoulliRegular/CyclotomicUnits/NormalizedIndex.lean
    complete
    theorem BernoulliRegular.CPlusGenerator_eq_cyclotomicUnitFamilyKplus {p : ℕ}
  [Fact (Nat.Prime p)] {K : Type} [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K] [NumberField.IsCMField K]
  (hp_three : 3 ≤ p) (i : Fin ((p - 3) / 2)) :
  BernoulliRegular.CPlusGenerator hp_three i =
    BernoulliRegular.FLT37.Sinnott.cyclotomicUnitFamilyKplus p K
      hp_three i
    theorem BernoulliRegular.CPlusGenerator_eq_cyclotomicUnitFamilyKplus
  {p : ℕ} [Fact (Nat.Prime p)] {K : Type}
  [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K]
  [NumberField.IsCMField K]
  (hp_three : 3 ≤ p)
  (i : Fin ((p - 3) / 2)) :
  BernoulliRegular.CPlusGenerator hp_three
      i =
    BernoulliRegular.FLT37.Sinnott.cyclotomicUnitFamilyKplus
      p K hp_three i
  • theoremdefined in BernoulliRegular/CyclotomicUnits/NormalizedIndex.lean
    complete
    theorem BernoulliRegular.range_cyclotomicUnitFamilyKplusFinRank_eq {p : ℕ}
  [Fact (Nat.Prime p)] {K : Type} [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K] [NumberField.IsCMField K]
  (hp_odd : p ≠ 2) (hp_three : 3 ≤ p) :
  Set.range
      (BernoulliRegular.FLT37.Sinnott.cyclotomicUnitFamilyKplusFinRank p
        K hp_odd hp_three) =
    Set.range
      (BernoulliRegular.FLT37.Sinnott.cyclotomicUnitFamilyKplus p K
        hp_three)
    theorem BernoulliRegular.range_cyclotomicUnitFamilyKplusFinRank_eq
  {p : ℕ} [Fact (Nat.Prime p)] {K : Type}
  [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K]
  [NumberField.IsCMField K]
  (hp_odd : p ≠ 2) (hp_three : 3 ≤ p) :
  Set.range
      (BernoulliRegular.FLT37.Sinnott.cyclotomicUnitFamilyKplusFinRank
        p K hp_odd hp_three) =
    Set.range
      (BernoulliRegular.FLT37.Sinnott.cyclotomicUnitFamilyKplus
        p K hp_three)
  • theoremdefined in BernoulliRegular/CyclotomicUnits/NormalizedIndex.lean
    complete
    theorem BernoulliRegular.torsionKplus_le_CPlus {p : ℕ} [Fact (Nat.Prime p)]
  {K : Type} [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K]
  [NumberField.IsCMField K] (hp_three : 3 ≤ p) :
  NumberField.Units.torsion ↥(NumberField.maximalRealSubfield K) ≤
    BernoulliRegular.CPlus hp_three
    theorem BernoulliRegular.torsionKplus_le_CPlus
  {p : ℕ} [Fact (Nat.Prime p)] {K : Type}
  [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K]
  [NumberField.IsCMField K]
  (hp_three : 3 ≤ p) :
  NumberField.Units.torsion
      ↥(NumberField.maximalRealSubfield
          K) ≤
    BernoulliRegular.CPlus hp_three
  • theoremdefined in BernoulliRegular/CyclotomicUnits/NormalizedIndex.lean
    complete
    theorem BernoulliRegular.CPlus_le_cyclotomicUnitIndexSubgroup {p : ℕ}
  [Fact (Nat.Prime p)] {K : Type} [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K] [NumberField.IsCMField K]
  (hp_odd : p ≠ 2) (hp_three : 3 ≤ p) :
  BernoulliRegular.CPlus hp_three ≤
    BernoulliRegular.cyclotomicUnitIndexSubgroup hp_odd hp_three
    theorem BernoulliRegular.CPlus_le_cyclotomicUnitIndexSubgroup
  {p : ℕ} [Fact (Nat.Prime p)] {K : Type}
  [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K]
  [NumberField.IsCMField K]
  (hp_odd : p ≠ 2) (hp_three : 3 ≤ p) :
  BernoulliRegular.CPlus hp_three ≤
    BernoulliRegular.cyclotomicUnitIndexSubgroup
      hp_odd hp_three
  • theoremdefined in BernoulliRegular/CyclotomicUnits/NormalizedIndex.lean
    complete
    theorem BernoulliRegular.cyclotomicUnitIndexSubgroup_le_CPlus {p : ℕ}
  [Fact (Nat.Prime p)] {K : Type} [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K] [NumberField.IsCMField K]
  (hp_odd : p ≠ 2) (hp_three : 3 ≤ p) :
  BernoulliRegular.cyclotomicUnitIndexSubgroup hp_odd hp_three ≤
    BernoulliRegular.CPlus hp_three
    theorem BernoulliRegular.cyclotomicUnitIndexSubgroup_le_CPlus
  {p : ℕ} [Fact (Nat.Prime p)] {K : Type}
  [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K]
  [NumberField.IsCMField K]
  (hp_odd : p ≠ 2) (hp_three : 3 ≤ p) :
  BernoulliRegular.cyclotomicUnitIndexSubgroup
      hp_odd hp_three ≤
    BernoulliRegular.CPlus hp_three
Proof for Lemma 7.7.2
uses 0

The full-rank family in C^+_{\mathrm{Sin}} is indexed by \operatorname{Fin}((p-3)/2), and the element with index i is exactly \varepsilon_{i+2}. Thus its range is the same generator range used for C^+_{\mathrm{sq}}. It remains to compare torsion. The torsion of the real cyclotomic unit group is \{\pm1\}. The unit 1 belongs to every subgroup, and -1 is one of the generators of C^+_{\mathrm{sq}}. Hence adjoining torsion to the full-rank family adds nothing beyond the subgroup already generated by -1,\varepsilon_2,\ldots,\varepsilon_{(p-1)/2}.

Theorem7.7.3
uses 1used by 1✓L∃∀N

Sinnott formula, odd-primary consequence. Assume the Kummer-Dirichlet determinant identity for the real cyclotomic-unit logarithm matrix. Then p\mid [E^+:C^+_{\mathrm{Sin}}] \quad\Longleftrightarrow\quad p\mid h^+ .

Definition 7.7.1

Lean code for Theorem7.7.3●6 theorems
  • theoremdefined in BernoulliRegular/CyclotomicUnits/IndexFormula.lean
    complete
    theorem BernoulliRegular.cyclotomicUnitIndex_primeConductor_pPrimary_of_sinnottIndexFormula
  {p : ℕ} [Fact (Nat.Prime p)] {K : Type} [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K] [NumberField.IsCMField K]
  (hp_odd : p ≠ 2) (hp_three : 3 ≤ p)
  (hSinnott :
    BernoulliRegular.FLT37.Sinnott.SinnottIndexFormula p K hp_odd
      hp_three) :
  p ∣
      (BernoulliRegular.cyclotomicUnitIndexSubgroup hp_odd
          hp_three).index ↔
    p ∣ BernoulliRegular.hPlus K
    theorem BernoulliRegular.cyclotomicUnitIndex_primeConductor_pPrimary_of_sinnottIndexFormula
  {p : ℕ} [Fact (Nat.Prime p)] {K : Type}
  [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K]
  [NumberField.IsCMField K]
  (hp_odd : p ≠ 2) (hp_three : 3 ≤ p)
  (hSinnott :
    BernoulliRegular.FLT37.Sinnott.SinnottIndexFormula
      p K hp_odd hp_three) :
  p ∣
      (BernoulliRegular.cyclotomicUnitIndexSubgroup
          hp_odd hp_three).index ↔
    p ∣ BernoulliRegular.hPlus K
    P-primary form of the real cyclotomic-unit index formula, conditional on
the existing explicit Sinnott index formula.
  • theoremdefined in BernoulliRegular/CyclotomicUnits/IndexFormula.lean
    complete
    theorem BernoulliRegular.cyclotomicUnitIndex_primeConductor_pPrimary_of_kummerDirichletDeterminant
  {p : ℕ} [Fact (Nat.Prime p)] {K : Type} [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K] [NumberField.IsCMField K]
  (hp_odd : p ≠ 2) (hp_three : 3 ≤ p)
  (hdet :
    BernoulliRegular.FLT37.Sinnott.KummerDirichletDeterminant p K hp_odd
      hp_three) :
  p ∣
      (BernoulliRegular.cyclotomicUnitIndexSubgroup hp_odd
          hp_three).index ↔
    p ∣ BernoulliRegular.hPlus K
    theorem BernoulliRegular.cyclotomicUnitIndex_primeConductor_pPrimary_of_kummerDirichletDeterminant
  {p : ℕ} [Fact (Nat.Prime p)] {K : Type}
  [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K]
  [NumberField.IsCMField K]
  (hp_odd : p ≠ 2) (hp_three : 3 ≤ p)
  (hdet :
    BernoulliRegular.FLT37.Sinnott.KummerDirichletDeterminant
      p K hp_odd hp_three) :
  p ∣
      (BernoulliRegular.cyclotomicUnitIndexSubgroup
          hp_odd hp_three).index ↔
    p ∣ BernoulliRegular.hPlus K
    P-primary cyclotomic-unit index formula from the named hard analytic input
`KummerDirichletDeterminant`.

The determinant input gives the squared-family index
`2^((p - 3) / 2) * hPlus K`; the final equivalence removes the power of `2`
using `p ≠ 2`.
  • theoremdefined in BernoulliRegular/FLT37/LehmerVandiver/PlusCoprime/Sinnott/LogEmbedding.lean
    complete
    theorem BernoulliRegular.FLT37.Sinnott.sinnottRegulatorIdentity_iff_kummerDirichletDeterminant
  (p : ℕ) [hp : Fact (Nat.Prime p)] (K : Type) [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K] [NumberField.IsCMField K]
  (hp_odd : p ≠ 2) (hp_three : 3 ≤ p) :
  BernoulliRegular.FLT37.Sinnott.KummerDirichletDeterminant p K hp_odd
      hp_three ↔
    BernoulliRegular.FLT37.Sinnott.SinnottRegulatorIdentity p K hp_odd
      hp_three
    theorem BernoulliRegular.FLT37.Sinnott.sinnottRegulatorIdentity_iff_kummerDirichletDeterminant
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  (K : Type) [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K]
  [NumberField.IsCMField K]
  (hp_odd : p ≠ 2) (hp_three : 3 ≤ p) :
  BernoulliRegular.FLT37.Sinnott.KummerDirichletDeterminant
      p K hp_odd hp_three ↔
    BernoulliRegular.FLT37.Sinnott.SinnottRegulatorIdentity
      p K hp_odd hp_three
    **`KummerDirichletDeterminant` = `SinnottRegulatorIdentity`**: as
formulated, both Props are literally the same equation.
  • theoremdefined in BernoulliRegular/FLT37/LehmerVandiver/PlusCoprime/Sinnott/IndexFormula.lean
    complete
    theorem BernoulliRegular.FLT37.Sinnott.sinnottIndexFormula_of_regulatorIdentity.{u_1}
  (p : ℕ) [hp : 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)
  (h :
    BernoulliRegular.FLT37.Sinnott.SinnottRegulatorIdentity p K hp_odd
      hp_three) :
  BernoulliRegular.FLT37.Sinnott.SinnottIndexFormula p K hp_odd hp_three
    theorem BernoulliRegular.FLT37.Sinnott.sinnottIndexFormula_of_regulatorIdentity.{u_1}
  (p : ℕ) [hp : 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)
  (h :
    BernoulliRegular.FLT37.Sinnott.SinnottRegulatorIdentity
      p K hp_odd hp_three) :
  BernoulliRegular.FLT37.Sinnott.SinnottIndexFormula
    p K hp_odd hp_three
    **Equivalence of Sinnott formula formulations**: the index version
follows from the regulator version (both encode the same content via
`regOfFamily_div_regulator`).
  • theoremdefined in BernoulliRegular/FLT37/LehmerVandiver/PlusCoprime/Sinnott/IndexFormula.lean
    complete
    theorem BernoulliRegular.FLT37.Sinnott.index_eq_twoPow_mul_hPlus_of_sinnottIndexFormula.{u_1}
  (p : ℕ) [hp : 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)
  (h :
    BernoulliRegular.FLT37.Sinnott.SinnottIndexFormula p K hp_odd
      hp_three) :
  (Subgroup.closure
          (Set.range
            (BernoulliRegular.FLT37.Sinnott.cyclotomicUnitFamilyKplusFinRank
              p K hp_odd hp_three)) ⊔
        NumberField.Units.torsion
          ↥(NumberField.maximalRealSubfield K)).index =
    2 ^ ((p - 3) / 2) * BernoulliRegular.hPlus K
    theorem BernoulliRegular.FLT37.Sinnott.index_eq_twoPow_mul_hPlus_of_sinnottIndexFormula.{u_1}
  (p : ℕ) [hp : 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)
  (h :
    BernoulliRegular.FLT37.Sinnott.SinnottIndexFormula
      p K hp_odd hp_three) :
  (Subgroup.closure
          (Set.range
            (BernoulliRegular.FLT37.Sinnott.cyclotomicUnitFamilyKplusFinRank
              p K hp_odd hp_three)) ⊔
        NumberField.Units.torsion
          ↥(NumberField.maximalRealSubfield
              K)).index =
    2 ^ ((p - 3) / 2) *
      BernoulliRegular.hPlus K
    **Sinnott formula bridge target**: under `SinnottIndexFormula` (step C/D),
the index identity gives `[E⁺ : ⟨family⟩ ⊔ torsion] = 2^((p-3)/2) · h⁺`
directly. The factor `2^((p-3)/2)` reflects the gap between the project's
squared cyclotomic family `⟨realCyclotomicUnit_k⟩` and the standard
cyclotomic units `C⁺`.
  • theoremdefined in BernoulliRegular/CyclotomicUnits/IndexFormula.lean
    complete
    theorem BernoulliRegular.prime_dvd_two_pow_mul_iff_dvd {p : ℕ}
  [Fact (Nat.Prime p)] (hp_odd : p ≠ 2) (r n : ℕ) :
  p ∣ 2 ^ r * n ↔ p ∣ n
    theorem BernoulliRegular.prime_dvd_two_pow_mul_iff_dvd
  {p : ℕ} [Fact (Nat.Prime p)]
  (hp_odd : p ≠ 2) (r n : ℕ) :
  p ∣ 2 ^ r * n ↔ p ∣ n
    The harmless `2^r` factor in the squared-family normalization has no
effect on p-primary divisibility for odd `p`.
Proof for Theorem 7.7.3
uses 0

Write g=(p-3)/2 and let R^+ = \operatorname{Reg}(E^+) be the regulator of the maximal real subfield. The determinant identity is the regulator identity \operatorname{Reg}(\varepsilon_2,\ldots,\varepsilon_{(p-1)/2}) = 2^g h^+ R^+. The passage from regulators to indices is the standard covolume comparison for the logarithmic unit lattice. Modulo torsion, the units E^+ form a lattice of rank g, and the family \varepsilon_2,\ldots,\varepsilon_{(p-1)/2} spans a full-rank sublattice. The covolume of the latter is its index in the former times the covolume of the former: \frac{\operatorname{Reg}(\varepsilon_2,\ldots,\varepsilon_{(p-1)/2})}{R^+} = [E^+:C^+_{\mathrm{Sin}}]. Since R^+>0, the displayed regulator identity therefore gives Sinnott's index formula in this normalization: [E^+:C^+_{\mathrm{Sin}}]=2^g h^+. Finally, p is odd, so p\nmid 2^g. Euclid's lemma gives p\mid 2^g h^+ \Longleftrightarrow p\mid h^+, and combining this with the index formula proves the stated equivalence.

Theorem7.7.4
Statement uses 3
Statement dependency previews
Preview
Definition 2.2.1
Loading preview
Statement dependency preview content is loaded from the Blueprint HTML cache.
used by 1✓L∃∀N

Deleted-Fourier determinant identity. Assume p\ge5. The logarithm matrix of the full-rank real cyclotomic-unit family satisfies the Kummer-Dirichlet determinant identity.

Definition 7.7.1 Definition 2.2.1 Definition 7.1.2

Lean code for Theorem7.7.4●1 theorem
  • theoremdefined in BernoulliRegular/CyclotomicUnits/NormalizedIndex.lean
    complete
    theorem BernoulliRegular.kummerDirichletDeterminant_of_deletedFourier {p : ℕ}
  [Fact (Nat.Prime p)] {K : Type} [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K] [NumberField.IsCMField K]
  (hp_odd : p ≠ 2) (hp_three : 3 ≤ p) (hp_two : 2 < p)
  (hp_ge_five : 5 ≤ p) :
  BernoulliRegular.FLT37.Sinnott.KummerDirichletDeterminant p K hp_odd
    hp_three
    theorem BernoulliRegular.kummerDirichletDeterminant_of_deletedFourier
  {p : ℕ} [Fact (Nat.Prime p)] {K : Type}
  [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K]
  [NumberField.IsCMField K]
  (hp_odd : p ≠ 2) (hp_three : 3 ≤ p)
  (hp_two : 2 < p) (hp_ge_five : 5 ≤ p) :
  BernoulliRegular.FLT37.Sinnott.KummerDirichletDeterminant
    p K hp_odd hp_three
Proof for Theorem 7.7.4
uses 0

The rows of the matrix are indexed by the non-trivial even characters modulo p, and the columns by \varepsilon_2,\ldots,\varepsilon_{(p-1)/2}. After the standard Fourier change of basis, the determinant separates into a deleted Fourier determinant and the product of the even character factors. The deleted Fourier determinant is nonzero: it is the determinant of the character table with the trivial row and the redundant column removed, and orthogonality of characters gives its inverse after multiplying by a power of p. The remaining product is the even part of the cyclotomic class-number formula. With the present squared-unit normalization, the regulator identity therefore has the form \operatorname{Reg}(\varepsilon_2,\ldots,\varepsilon_{(p-1)/2}) = 2^g h^+ R^+, g=(p-3)/2. This is precisely the Kummer-Dirichlet determinant identity used in the index calculation.

Corollary7.7.5
Statement uses 2
Statement dependency previews
Preview
Theorem 7.7.3
Loading preview
Statement dependency preview content is loaded from the Blueprint HTML cache.
used by 1✓L∃∀N

Sinnott formula for prime conductor. If p\ge5, then p\mid [E^+:C^+_{\mathrm{Sin}}] \quad\Longleftrightarrow\quad p\mid h^+ .

Theorem 7.7.3 Theorem 7.7.4

Lean code for Corollary7.7.5●3 theorems
  • theoremdefined in BernoulliRegular/CyclotomicUnits/NormalizedIndex.lean
    complete
    theorem BernoulliRegular.kummerDirichletDeterminant_of_deletedFourier {p : ℕ}
  [Fact (Nat.Prime p)] {K : Type} [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K] [NumberField.IsCMField K]
  (hp_odd : p ≠ 2) (hp_three : 3 ≤ p) (hp_two : 2 < p)
  (hp_ge_five : 5 ≤ p) :
  BernoulliRegular.FLT37.Sinnott.KummerDirichletDeterminant p K hp_odd
    hp_three
    theorem BernoulliRegular.kummerDirichletDeterminant_of_deletedFourier
  {p : ℕ} [Fact (Nat.Prime p)] {K : Type}
  [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K]
  [NumberField.IsCMField K]
  (hp_odd : p ≠ 2) (hp_three : 3 ≤ p)
  (hp_two : 2 < p) (hp_ge_five : 5 ≤ p) :
  BernoulliRegular.FLT37.Sinnott.KummerDirichletDeterminant
    p K hp_odd hp_three
  • theoremdefined in BernoulliRegular/CyclotomicUnits/NormalizedIndex.lean
    complete
    theorem BernoulliRegular.cyclotomicUnitIndex_primeConductor_pPrimary_aux {p : ℕ}
  [Fact (Nat.Prime p)] {K : Type} [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K] [NumberField.IsCMField K]
  (hp_odd : p ≠ 2) (hp_three : 3 ≤ p) (hp_two : 2 < p)
  (hp_ge_five : 5 ≤ p) :
  p ∣ (BernoulliRegular.normalizedCPlus hp_odd hp_three).index ↔
    p ∣ BernoulliRegular.hPlus K
    theorem BernoulliRegular.cyclotomicUnitIndex_primeConductor_pPrimary_aux
  {p : ℕ} [Fact (Nat.Prime p)] {K : Type}
  [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K]
  [NumberField.IsCMField K]
  (hp_odd : p ≠ 2) (hp_three : 3 ≤ p)
  (hp_two : 2 < p) (hp_ge_five : 5 ≤ p) :
  p ∣
      (BernoulliRegular.normalizedCPlus
          hp_odd hp_three).index ↔
    p ∣ BernoulliRegular.hPlus K
  • theoremdefined in BernoulliRegular/CyclotomicUnits/IndexFormula.lean
    complete
    theorem BernoulliRegular.cyclotomicUnitIndex_primeConductor_pPrimary_of_kummerDirichletDeterminant
  {p : ℕ} [Fact (Nat.Prime p)] {K : Type} [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K] [NumberField.IsCMField K]
  (hp_odd : p ≠ 2) (hp_three : 3 ≤ p)
  (hdet :
    BernoulliRegular.FLT37.Sinnott.KummerDirichletDeterminant p K hp_odd
      hp_three) :
  p ∣
      (BernoulliRegular.cyclotomicUnitIndexSubgroup hp_odd
          hp_three).index ↔
    p ∣ BernoulliRegular.hPlus K
    theorem BernoulliRegular.cyclotomicUnitIndex_primeConductor_pPrimary_of_kummerDirichletDeterminant
  {p : ℕ} [Fact (Nat.Prime p)] {K : Type}
  [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K]
  [NumberField.IsCMField K]
  (hp_odd : p ≠ 2) (hp_three : 3 ≤ p)
  (hdet :
    BernoulliRegular.FLT37.Sinnott.KummerDirichletDeterminant
      p K hp_odd hp_three) :
  p ∣
      (BernoulliRegular.cyclotomicUnitIndexSubgroup
          hp_odd hp_three).index ↔
    p ∣ BernoulliRegular.hPlus K
    P-primary cyclotomic-unit index formula from the named hard analytic input
`KummerDirichletDeterminant`.

The determinant input gives the squared-family index
`2^((p - 3) / 2) * hPlus K`; the final equivalence removes the power of `2`
using `p ≠ 2`.
Proof for Corollary 7.7.5
uses 0

For p\ge5, the deleted-Fourier determinant computation evaluates the logarithm determinant of the real cyclotomic units. The matrix rows are the even non-trivial characters, the columns are the units \varepsilon_2,\ldots,\varepsilon_{(p-1)/2}, and the determinant splits into a nonzero Fourier determinant times the product of the character factors. The class-number formula for the real subfield identifies this product with h^+R^+, with the extra factor 2^g coming from using the squared cyclotomic-unit family. Thus the Kummer-Dirichlet determinant identity holds, and Theorem 7.7.3 applies.

Theorem7.7.6
Statement uses 3
Statement dependency previews
Preview
Lemma 7.2.4
Loading preview
Statement dependency preview content is loaded from the Blueprint HTML cache.
used by 1✓L∃∀N

Prime-conductor cyclotomic-unit index theorem. For odd p, p \mid [E^+:C^+_{\mathrm{norm}}] \quad\Longleftrightarrow\quad p \mid h^+.

Corollary 7.7.5 Lemma 7.7.2 Lemma 7.2.4

Lean code for Theorem7.7.6●3 theorems
  • theoremdefined in BernoulliRegular/CyclotomicUnits/NormalizedIndex.lean
    complete
    theorem BernoulliRegular.cyclotomicUnitIndex_primeConductor_pPrimary {p : ℕ}
  [Fact (Nat.Prime p)] {K : Type} [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K] [NumberField.IsCMField K]
  (hp_odd : p ≠ 2) :
  p ∣ (BernoulliRegular.normalizedCPlus hp_odd ⋯).index ↔
    p ∣ BernoulliRegular.hPlus K
    theorem BernoulliRegular.cyclotomicUnitIndex_primeConductor_pPrimary
  {p : ℕ} [Fact (Nat.Prime p)] {K : Type}
  [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K]
  [NumberField.IsCMField K]
  (hp_odd : p ≠ 2) :
  p ∣
      (BernoulliRegular.normalizedCPlus
          hp_odd ⋯).index ↔
    p ∣ BernoulliRegular.hPlus K
    CU-06: the prime-conductor cyclotomic-unit index theorem for the TeX
normalized subgroup `C⁺ = <-1, ε₂, ..., ε_g>`, in odd-primary form.
  • theoremdefined in BernoulliRegular/CyclotomicUnits/NormalizedIndex.lean
    complete
    theorem BernoulliRegular.cyclotomicUnitIndex_primeConductor_pPrimary_of_eq_three
  {p : ℕ} [Fact (Nat.Prime p)] {K : Type} [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K] [NumberField.IsCMField K]
  (hp_odd : p ≠ 2) (hp_three : 3 ≤ p) (hp_eq : p = 3) :
  p ∣ (BernoulliRegular.normalizedCPlus hp_odd hp_three).index ↔
    p ∣ BernoulliRegular.hPlus K
    theorem BernoulliRegular.cyclotomicUnitIndex_primeConductor_pPrimary_of_eq_three
  {p : ℕ} [Fact (Nat.Prime p)] {K : Type}
  [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K]
  [NumberField.IsCMField K]
  (hp_odd : p ≠ 2) (hp_three : 3 ≤ p)
  (hp_eq : p = 3) :
  p ∣
      (BernoulliRegular.normalizedCPlus
          hp_odd hp_three).index ↔
    p ∣ BernoulliRegular.hPlus K
  • theoremdefined in BernoulliRegular/CyclotomicUnits/NormalizedIndex.lean
    complete
    theorem BernoulliRegular.cyclotomicUnitIndex_primeConductor_pPrimary_of_five_le
  {p : ℕ} [Fact (Nat.Prime p)] {K : Type} [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K] [NumberField.IsCMField K]
  (hp_ge_five : 5 ≤ p) :
  p ∣ (BernoulliRegular.normalizedCPlus ⋯ ⋯).index ↔
    p ∣ BernoulliRegular.hPlus K
    theorem BernoulliRegular.cyclotomicUnitIndex_primeConductor_pPrimary_of_five_le
  {p : ℕ} [Fact (Nat.Prime p)] {K : Type}
  [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K]
  [NumberField.IsCMField K]
  (hp_ge_five : 5 ≤ p) :
  p ∣
      (BernoulliRegular.normalizedCPlus ⋯
          ⋯).index ↔
    p ∣ BernoulliRegular.hPlus K
Proof for Theorem 7.7.6
uses 0

There are two cases. If p=3, then K^+=\mathbb{Q}. The plus class number is therefore h^+=1. The real unit rank is zero, so the normalised cyclotomic-unit subgroup is the whole unit group. Hence both sides are the assertion that 3 divides 1, and both are false. Now assume p\ne3. Since p is an odd prime, this gives p\ge5. By Corollary 7.7.5, p\mid [E^+:C^+_{\mathrm{Sin}}] \Longleftrightarrow p\mid h^+. The subgroup identification Lemma 7.7.2 replaces C^+_{\mathrm{Sin}} by C^+_{\mathrm{sq}}. Finally, the odd-primary comparison Lemma 7.2.4 replaces C^+_{\mathrm{sq}} by C^+_{\mathrm{norm}}, because the quotient between the two generated subgroups has exponent dividing a power of 2. Since p is odd, this quotient does not affect p-divisibility of the ambient index. The displayed equivalence follows.