Algebras
Say \(F\) is a locally compact topological ring (for example \(\mathbb{R}\) or \(\mathbb{C}\) or \(\mathbb{Q}_p\), or the adeles of a number field), \(V\) is a finite free \(F\)-module, and \(\phi:V\to V\) is an invertible \(F\)-linear map. Then \(V\) with its module topology (which is the product topology if one picks a basis) is a locally compact topological abelian group, and \(\phi\) is additive. One can check that linearity implies continuity (this is IsModuleTopology.continuous_of_linearMap in mathlib), so in fact \(\phi\) is a homeomorphism and our theory applies. The following lemma gives a formula for the scale factor \(d_V(\phi)\).
LemmaMeasureTheory.addEquivAddHaarChar_eq_ringHaarChar_det, MeasureTheory.addEquivAddHaarChar_eq_ringHaarChar_det_of_existsListTransvecEtc#
Assume that there's an \(F\)-basis for \(V\) such that \(\phi\) is a product of elementary and diagonal matrices (note that this is automatic if \(F\) is a field and mathlib has this). Then \(d_V(\phi)=\delta_F(\det(\phi))\), where \(\det(\phi)\in F\) is the determinant of \(\phi\) as an \(F\)-linear map.
Proof
The proof is a generalization of Real.map_matrix_volume_pi_eq_smul_volume_pi, which crucially uses the induction principle Matrix.diagonal_transvection_induction_of_det_ne_zero. One checks it explicitly for diagonal matrices and for matrices which are the identity except that one off-diagonal entry is non-zero.
Note: we assume that \(F\) is second countable (but it shouldn't be necessary).
Lean
Formalized as MeasureTheory.addEquivAddHaarChar_eq_ringHaarChar_det, MeasureTheory.addEquivAddHaarChar_eq_ringHaarChar_det_of_existsListTransvecEtc.
Sources
Uses 2
Now say \(F\) is a locally compact topological field, and that \(R\) is a (possibly non-commutative) \(F\)-algebra. Recall that this means that (\(R=0\) or) \(F\) lies in the centre of \(R\). Assume that \(R\) is finite-dimensional as an \(F\)-vector space. Then if we give \(R\) the \(F\)-module topology (which is just the product topology if we pick a basis) then it is known that \(R\) becomes a topological ring. Now say \(u\in R^\times\), and recall \(\ell_u:R\to R\) is left multiplication by \(u\). Then \(\ell_u\) is easily checked to be an \(F\)-linear homeomorphism.
CorollaryMeasureTheory.algebra_ringHaarChar_eq_ringHaarChar_det#
If \(u\in R^\times\) then \(\delta_R(u)=\delta_F(\det(\ell_u))\).
Proof
Follows immediately from the preceding lemma.
Lean
Formalized as MeasureTheory.algebra_ringHaarChar_eq_ringHaarChar_det.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.