English
The commMap applied to the canonical embedding equals the mixed embedding: commMap(K)(canonicalEmbedding(K)(x)) = mixedEmbedding(K)(x).
Русский
Применение commMap к каноническому вложению равно смешанному вложению: commMap(K)(canonicalEmbedding(K)(x)) = mixedEmbedding(K)(x).
LaTeX
$$$\mathrm{commMap}(K)(\mathrm{canonicalEmbedding}(K)(x)) = \mathrm{mixedEmbedding}(K)(x).$$$
Lean4
/-- The linear map that makes `canonicalEmbedding` and `mixedEmbedding` commute, see
`commMap_canonical_eq_mixed`. -/
noncomputable def commMap : ((K →+* ℂ) → ℂ) →ₗ[ℝ] (mixedSpace K)
where
toFun := fun x => ⟨fun w => (x w.val.embedding).re, fun w => x w.val.embedding⟩
map_add' := by
simp only [Pi.add_apply, Complex.add_re, Prod.mk_add_mk, Prod.mk.injEq]
exact fun _ _ => ⟨rfl, rfl⟩
map_smul' :=
by
simp only [Pi.smul_apply, Complex.real_smul, Complex.mul_re, Complex.ofReal_re, Complex.ofReal_im, zero_mul,
sub_zero, RingHom.id_apply, Prod.smul_mk, Prod.mk.injEq]
exact fun _ _ => ⟨rfl, rfl⟩
