Definitions/Def_LanglandsTunnell_TowerCounting.lean

Throughout, L is a number field that is Galois over \mathbb{Q}. Three counting objects are defined. First, oddJ is the finite set \{1,3,5,7\}\subseteq\mathbb{N} of odd residues modulo 8. Second, labelledCount takes \sigma\in\operatorname{Gal}(L/\mathbb{Q}), a finite set S_0 of naturals, a label m\in\mathbb{Z}/8 and a natural number \ell, and returns a natural number: it is 0 when \ell\in S_0 and when \ell is not prime; otherwise it is the number (as Set.ncard) of primes \mathfrak{q} of the ring of integers of the fixed field L^{\langle\sigma\rangle} — the intermediate field of invariants of the subgroup Subgroup.zpowers σ generated by \sigma — that lie over the ideal \ell\mathbb{Z}, subject to two conditions: the residue ring at \mathfrak{q} has exactly \ell elements (so \mathfrak{q} has residue degree one over \ell), and there exists a prime ideal Q of \mathcal{O}_L lying over both \mathfrak{q} and \ell\mathbb{Z} whose inertia subgroup in \operatorname{Gal}(L/\mathbb{Q}) is trivial and whose arithmetic Frobenius arithFrobAt ℤ (L ≃ₐ[ℚ] L) Q is equal, on the nose and not merely up to conjugacy, to \sigma^{m} for the natural number underlying m. Third, classIndicator takes \sigma and \ell and returns 1 or 0 according as \ell is prime and some prime Q of \mathcal{O}_L over \ell\mathbb{Z} has trivial inertia subgroup in \operatorname{Gal}(L/\mathbb{Q}) and arithmetic Frobenius conjugate to \sigma, or not. Two accompanying lemmas record the evident bounds: labelledCount_of_mem_S₀ states that labelledCount σ S₀ m ℓ vanishes for \ell\in S_0, and classIndicator_le_one that classIndicator σ ℓ \le 1. The finiteness of the residue rings needed to speak of Frobenius is supplied by the prime Q lying over \ell\mathbb{Z} with \ell prime.