English
A ℤ-basis b of a lattice L in E yields a basis of E over the field K; i.e., the set of vectors given by b forms a basis of E as a K-vector space.
Русский
База ℤ-решетки b в пространстве L порождает базу пространства E над K; множество векторов, задаваемое b, образует базisу E над K.
LaTeX
$$$\\text{the family } (b_i)_{i\\in\\iota} \\text{ is a basis of } E \\text{ over } K$$$
Lean4
/-- Any `ℤ`-basis of `L` is also a `K`-basis of `E`. -/
def ofZLatticeBasis : Basis ι K E :=
by
have : Module.Finite ℤ L := ZLattice.module_finite K L
have : Free ℤ L := ZLattice.module_free K L
let e := (Free.chooseBasis ℤ L).indexEquiv b
have : Fintype ι := Fintype.ofEquiv _ e
refine basisOfTopLeSpanOfCardEqFinrank (L.subtype ∘ b) ?_ ?_
·
rw [← span_span_of_tower ℤ, Set.range_comp, ← map_span, Basis.span_eq, Submodule.map_top, range_subtype, top_le_iff,
hs.span_top]
· rw [← Fintype.card_congr e, ← finrank_eq_card_chooseBasisIndex, ZLattice.rank K L]
