English
An element x lies in the integer lattice-span if and only if it lies in the image of the canonical embedding composed with the inclusion of O_K into K.
Русский
Элемент x лежит в линейной оболочке решетки целых, эквивалентно тому, что x лежит в образе канонического вложения, составленного с включением O_K в K.
LaTeX
$$$x \\in \\mathrm{span}_{\\mathbb{Z}}(\\mathrm{range}(\\text{latticeBasis}(K))) \\iff x \\in (\\mathrm{canonicalEmbedding}(K)\\circ \\mathrm{algebraMap}(\\mathcal{O}_K)\\;K).\\text{range}$$$
Lean4
theorem mem_span_latticeBasis [NumberField K] {x : (K →+* ℂ) → ℂ} :
x ∈ Submodule.span ℤ (Set.range (latticeBasis K)) ↔ x ∈ ((canonicalEmbedding K).comp (algebraMap (𝓞 K) K)).range :=
by
rw [show Set.range (latticeBasis K) = (canonicalEmbedding K).toIntAlgHom.toLinearMap '' (Set.range (integralBasis K))
by rw [← Set.range_comp]; exact congrArg Set.range (funext (fun i => latticeBasis_apply K i))]
rw [← Submodule.map_span, ← SetLike.mem_coe, Submodule.map_coe]
rw [← RingHom.map_range, Subring.mem_map, Set.mem_image]
simp only [SetLike.mem_coe, mem_span_integralBasis K]
rfl
