10.3. Component reflection🔗

Theorem10.3.1

uses 1used by 1✓L∃∀N

Component reflection. Let i be an even reflection index. If the i-component of \mathrm{Cl}(\mathcal{O}_K)/p\,\mathrm{Cl}(\mathcal{O}_K) is nonzero, then the reflected component is nonzero: A_i\ne0\Longrightarrow A_{1-i}\ne0.

Theorem 10.2.1

Lean code for Theorem10.3.1●1 theorem

theoremdefined in BernoulliRegular/Reflection/FinalReflection/Part2.lean

complete

theorem BernoulliRegular.weakReflection_componentNontrivial.{u} (p : ℕ)
  [Fact (Nat.Prime p)] (hp_odd : Odd p) (K : Type u) [Field K]
  [NumberField K] [IsCyclotomicExtension {p} ℚ K]
  [NumberField.IsCMField K] {i : ℕ}
  (hi : BernoulliRegular.IsReflectionComponentIndex p i)
  (hi_even : Even i)
  (hcomp : BernoulliRegular.eigenspaceComponentNontrivial p K i) :
  BernoulliRegular.eigenspaceComponentNontrivial p K
    (BernoulliRegular.reflectedComponentIndex p i)

theorem BernoulliRegular.weakReflection_componentNontrivial.{u}
  (p : ℕ) [Fact (Nat.Prime p)]
  (hp_odd : Odd p) (K : Type u) [Field K]
  [NumberField K]
  [IsCyclotomicExtension {p} ℚ K]
  [NumberField.IsCMField K] {i : ℕ}
  (hi :
    BernoulliRegular.IsReflectionComponentIndex
      p i)
  (hi_even : Even i)
  (hcomp :
    BernoulliRegular.eigenspaceComponentNontrivial
      p K i) :
  BernoulliRegular.eigenspaceComponentNontrivial
    p K
    (BernoulliRegular.reflectedComponentIndex
      p i)

**Weak reflection, component form.**

For the cyclotomic field `K = Q(zeta_p)`, if the even `i`-th character
component of `Cl(O_K) / p` is nontrivial, then the reflected component
`p - i`, equivalently `1 - i mod p - 1`, is nontrivial.

The proof uses the primary singular-pair extraction in the interior range and
the zero-character contradiction for the endpoint `i = p - 1`.  The only
remaining hard reciprocity input in this chain is
`oneSidedKummerPrincipalReciprocity_canonical`, through the WR-05
nontriviality theorem for the concrete Kummer bad-set character.

Proof for Theorem 10.3.1

uses 0

The proof has five mathematical steps. First, the nonzero component A_i gives a nonzero locally-primary singular pseudo-unit. More precisely, one obtains \eta\in\mathcal{O}_K, (\eta)=\mathfrak b^p, \eta\notin K^{\times p}, where \eta is prime to p, locally a p-th power at \zeta_p-1, and has Galois weight i up to multiplication by global p-th powers.

Second, use the residue symbol to define a character on ideal classes: \chi_\eta([\mathfrak a]) = \left(\frac{\eta}{\mathfrak a}\right)_p. The representative \mathfrak a is chosen coprime to a finite bad set containing the primes above p, the primes dividing (\eta), and the Kummer-Dedekind conductor. Such representatives exist by ideal avoidance. The principal-denominator vanishing consequence of Theorem 10.2.1 makes the value independent of this choice. Thus \chi_\eta descends to a character of A.

Third, the character is nonzero. If it were zero, then for every prime ideal \mathfrak q outside the bad set the residue symbol (\eta/\mathfrak q)_p would be trivial. Hence the reduction of \eta would be a p-th power in \mathcal{O}_K/\mathfrak q, so T^p-\eta would split modulo \mathfrak q. Kummer-Dedekind would then show that almost all primes of K split completely in K(\eta^{1/p})/K. The weak splitting lemma forces this extension to be trivial, contradicting \eta\notin K^{\times p}.

Fourth, the Galois weight of \eta gives the covariance relation \chi_\eta(\sigma_a x)=a^{1-i}\chi_\eta(x) (a\in(\mathbb{Z}/p\mathbb{Z})^\times). Thus the nonzero character is supported on the reflected component.

Finally, the boundary case i=p-1 is treated separately. The zero-character component of A is trivial: if an ideal class is fixed by all Galois conjugates, the product of all its conjugates is represented by a Galois-stable ideal, hence by a principal ideal. The class therefore has order dividing both p and p-1, so it is trivial. The remaining case is the interior even case handled by the preceding argument.