Definitions/Def_Stickelberger_Basic.lean

Fix a natural number p, an additive commutative group A carrying a \mathbb{Z}/p-module structure, and regard an action of \Delta=(\mathbb{Z}/p)^\times on A as a monoid homomorphism \rho\colon(\mathbb{Z}/p)^\times\to\operatorname{End}_{\mathbb{Z}/p}(A) rather than as a group-action instance. The indexing set exponentSet p is the finite set of natural numbers c<p with 0<c and 2c<p, i.e. the integers in the lower half interval 0<c<p/2; the accompanying membership lemma records that c lies in it exactly when 0<c and 2c<p, the bound c<p being automatic. The natural number eigenvalueScalar p is the sum \sum_{0<c<p/2}c of the elements of that set. For c:\mathbb{N}, expUnit p c is the unit of \mathbb{Z}/p determined by c when c is coprime to p (via Mathlib's ZMod.unitOfCoprime) and is 1 otherwise, so it is a total function on \mathbb{N} by a case split rather than a partially defined one.

Given \rho, the endomorphism stickelbergerEnd is \eta=\sum_{c\in\mathtt{exponentSet}\,p}\rho\bigl((\mathtt{expUnit}\,p\,c)^{-1}\bigr), the sum taken in the \mathbb{Z}/p-linear endomorphism ring; this is the integral half-interval Stickelberger operator \sum_{0<c<p/2}\sigma_c^{-1} acting through \rho. The predicate StickelbergerAnnihilates asserts that \eta a=0 for every a\in A, stated pointwise rather than as the equation \eta=0 in the endomorphism ring. The predicate IsOmegaEigenvector takes an exponent i:\mathbb{N} and an element a\in A, and asserts that \rho(d)\,a=\bigl(\bar d^{\,i}\bigr)\cdot a for every unit d of \mathbb{Z}/p, where \bar d\in\mathbb{Z}/p is the underlying residue: thus a lies in the \omega^i-eigenspace for the given action, with \omega the inclusion of \Delta into (\mathbb{Z}/p)^\times.