English
The canonical embedding map evaluated at an element α equals the transpose of the basis matrix applied to the coordinate vector of α in the integral basis representation.
Русский
Каноническое вложение в точке α равняется транспонированной базисной матрице, примененной к вектору координат α в интегральной базе.
LaTeX
$$$$\\operatorname{canonicalEmbedding}(K,\\alpha) = (\\text{basisMatrix}(K))^{T} \\cdot \\big( \\text{repr}_{\\mathcal{O}_K}(\\alpha) \\big).$$$$
Lean4
theorem canonicalEmbedding_eq_basisMatrix_mulVec (α : K) :
canonicalEmbedding K α =
(basisMatrix K).transpose.mulVec (fun i ↦ (((integralBasis K).reindex (equivReindex K).symm).repr α i : ℂ)) :=
by
ext i
rw [← (latticeBasis K).sum_repr (canonicalEmbedding K α), ← Equiv.sum_comp (equivReindex K)]
simp only [canonicalEmbedding.integralBasis_repr_apply, mulVec, dotProduct, transpose_apply, of_apply,
Fintype.sum_apply, mul_comm, Basis.repr_reindex, Finsupp.mapDomain_equiv_apply, Equiv.symm_symm, Pi.smul_apply,
smul_eq_mul]
