The goal

The goal of this miniproject is to develop the theory (i.e., the basic API) of Haar characters. “Haar character” is a name I've made up to describe a certain character of the units of a locally compact topological ring. The main result we need here is that if \(B\) is a finite-dimensional algebra over a number field \(K\), then \(B^\times\) is in the kernel of the Haar character of \(B\otimes_K\mathbb{A}_K\), where \(\mathbb{A}_K\) is the ring of adeles of \(K\). Most if not all of this should probably be in mathlib.

KMB would like to heartily thank Sébastien Gouëzel for the help he gave during the preparation of this material.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.