English
The map commMap is the linear map that makes canonical embedding and mixed embedding commute; it sends x to the pair of real and complex coordinate functionals given by the real and imaginary parts of x at each place.
Русский
Отображение commMap — линейное отображение, делающий каноническое вложение и смешанное вложение совместимыми; оно отправляет x в пару координатных функционалов на вещественных и комплексных местах, задаваемых по вещественной и мнимой частям x на месте.
LaTeX
$$$\text{commMap}(K): ((K \to_+^* \mathbb{C}) \to \mathbb{C}) \to_ℝ \mathrm{mixedSpace}(K), \; \text{toFun } x = \langle w \mapsto \operatorname{Re}(x(w.\text{embedding})), \; w \mapsto x(w.\text{embedding})\rangle.$$$
Lean4
/-- The set of points in the mixedSpace that are equal to `0` at a fixed (real) place has
volume zero. -/
theorem volume_eq_zero (w : { w // IsReal w }) : volume ({x : mixedSpace K | x.1 w = 0}) = 0 :=
by
let A : AffineSubspace ℝ (mixedSpace K) :=
Submodule.toAffineSubspace (Submodule.mk ⟨⟨{x | x.1 w = 0}, by simp_all⟩, rfl⟩ (by simp_all))
convert Measure.addHaar_affineSubspace volume A fun h ↦ ?_
simpa [A] using (h ▸ Set.mem_univ _ : 1 ∈ A)
