English
The latticeBasis element indexed by i is exactly the image under the canonical embedding of the i-th integral basis element of K.
Русский
Элемент базиса решетки с индексом i равен образу i-й интегральной базисной функции под каноническим вложением.
LaTeX
$$$\\text{latticeBasis}(K,i) = \\big(\\mathrm{canonicalEmbedding}(K)\\big)(\\mathrm{integralBasis}(K,i))$$$
Lean4
theorem integralBasis_repr_apply [NumberField K] (x : K) (i : Free.ChooseBasisIndex ℤ (𝓞 K)) :
(latticeBasis K).repr (canonicalEmbedding K x) i = (integralBasis K).repr x i :=
by
rw [← Basis.restrictScalars_repr_apply ℚ _ ⟨_, mem_rat_span_latticeBasis K x⟩, eq_ratCast, Rat.cast_inj]
let f := (canonicalEmbedding K).toRatAlgHom.toLinearMap.codRestrict _ (fun x ↦ mem_rat_span_latticeBasis K x)
suffices ((latticeBasis K).restrictScalars ℚ).repr.toLinearMap ∘ₗ f = (integralBasis K).repr.toLinearMap from
DFunLike.congr_fun (LinearMap.congr_fun this x) i
refine Basis.ext (integralBasis K) (fun i ↦ ?_)
have : f (integralBasis K i) = ((latticeBasis K).restrictScalars ℚ) i :=
by
apply Subtype.val_injective
rw [LinearMap.codRestrict_apply, AlgHom.toLinearMap_apply, Basis.restrictScalars_apply, latticeBasis_apply]
rfl
simp_rw [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, this, Basis.repr_self]
