Kummer’s Criterion

1 The real cyclotomic-unit subgroup

Definition 1.1
✓
#

Lean declarations

For \(2\le a\le (p-1)/2\), the real cyclotomic unit is the unit of \(\mathcal O_{K^+}\) represented by

\[ \frac{1-\zeta _p^a}{1-\zeta _p}. \]
Definition 1.2
✓
#

Uses

Lean declarations

The finite family of standard generators is indexed by \(a=2,\ldots ,(p-1)/2\) and written as ‘CPlusGenerator‘.

Definition 1.3
✓
#

Uses

Lean declarations

The subgroup \(C^+\subseteq (\mathcal O_{K^+})^\times \) is generated by \(-1\) and the standard real cyclotomic units:

\[ C^+=\langle -1,\varepsilon _2,\ldots ,\varepsilon _{(p-1)/2}\rangle . \]
Definition 1.4
✓
#

Uses

Lean declarations

The normalized subgroup is generated by \(-1\) and normalized square roots of the standard real cyclotomic units.

Theorem 1.5
✓
#

Uses

Lean declarations

Each normalized generator squares to the corresponding generator of \(C^+\).

Proof ▶

This is the normalization property built into the definition of the normalized generators.

Theorem 1.6
✓
#

Uses

Lean declarations

For an odd prime \(p\),

\[ p\mid [(\mathcal O_{K^+})^\times :C^+] \Longleftrightarrow p\mid [(\mathcal O_{K^+})^\times :C^+_{\mathrm{norm}}]. \]
Proof ▶

The relative quotient between \(C^+\) and the normalized subgroup has order dividing a power of \(2\). Since \(p\) is odd, passing between the two indices does not change \(p\)-divisibility.