English
There exists a canonical ℂ-basis of the space of complex-valued functions on embeddings which is also a ℤ-basis for the image lattice from O_K; this basis is built from the canonical embedding applied to the integral basis.
Русский
Существует канонический базис над ℂ для пространства функций, образованных вложением, который также является ℤ-базисом для образной решетки O_K; этот базис строится из канонического вложения, применённого к интегральному базису.
LaTeX
$$$\\text{latticeBasis}(K)$ is a Basis of $((K\\to\\mathbb{C})\\to\\mathbb{C})$ over $\\mathbb{C}$, coming from $(\\mathrm{integralBasis}(K))$ via the canonical embedding.$$
Lean4
@[simp]
theorem latticeBasis_apply [NumberField K] (i : Free.ChooseBasisIndex ℤ (𝓞 K)) :
latticeBasis K i = (canonicalEmbedding K) (integralBasis K i) := by
simp [latticeBasis, integralBasis_apply, coe_basisOfPiSpaceOfLinearIndependent, Function.comp_apply,
Equiv.apply_symm_apply]
