Definitions/Def_HeckeCharacter_FiniteOrder.lean

Fix a number field K, with ring of integers \mathcal{O}_K and adele ring \mathbb{A}_K = AdeleRing (𝓞 K) K, whose elements are pairs consisting of an infinite and a finite component. The module introduces three declarations concerning characters \chi : \mathbb{A}_K^\times \to \mathbb{C}^\times (monoid homomorphisms into \mathbb{C}^\times).

IsFiniteOrderHeckeChar K χ is a structure in Prop bundling three conditions on \chi: that AutomorphicForm.IsIdeleClassChar (𝓞 K) K χ holds, i.e. \chi kills the image of K^\times under the diagonal embedding K^\times \to \mathbb{A}_K^\times, so that \chi is a character of the idele class group; that \chi is continuous; and that \chi is of finite order in the (pointwise) group of characters, i.e. \chi^n = 1 for some n \ge 1, so all values of \chi are roots of unity of bounded order.

idealMultiplicity K v 𝔣 attaches to a height-one prime v of \mathcal{O}_K and an ideal \mathfrak{f} \subseteq \mathcal{O}_K the natural number counting how often the prime v occurs among the factors of \mathfrak{f}, taken in the associates monoid; for \mathfrak{f} = \mathcal{O}_K all these multiplicities vanish. No nonvanishing hypothesis is imposed on \mathfrak{f}.

AdmitsModulus K χ 𝔣 asserts that \chi is trivial on the congruence subgroup of level \mathfrak{f}: for every idele unit u whose infinite component is 1 and whose finite component satisfies, at every height-one prime v, both v(u_v) = 1 and v(u_v - 1) \le \exp(-n_v) with n_v = idealMultiplicity K v 𝔣 (valuations taken in ℤᵐ⁰ through Valued.v), one has \chi(u) = 1. Thus the conditions say u_v \in \mathcal{O}_v^\times at all finite places and u_v \equiv 1 \bmod \mathfrak{p}_v^{n_v} at the primes dividing \mathfrak{f}. This is a triviality condition on a subgroup, not the assertion that \mathfrak{f} is the conductor.