English
Any basis of an R-lattice in V extends to a basis of V over K. In particular, given a lattice M and a basis of M as an R-module, there exists a K-basis of V extending it.
Русский
Любой базис R-решётки в V можно продолжить до базиса V над K; то есть существует K-базис V, который расширяет данный базис M над R.
LaTeX
$$$\text{There exists a basis } \tilde{b} \text{ of } V \text{ over } K \text{ such that } \tilde{b}|_M = b.$$$
Lean4
/-- Any basis of an `R`-lattice in `V` defines a `K`-basis of `V`. -/
noncomputable def _root_.Module.Basis.extendOfIsLattice [IsFractionRing R K] {κ : Type*} {M : Submodule R V}
[IsLattice K M] (b : Basis κ R M) : Basis κ K V :=
have hli : LinearIndependent K (fun i ↦ (b i).val) :=
by
rw [← LinearIndependent.iff_fractionRing (R := R), linearIndependent_iff']
intro s g hs
simp_rw [← Submodule.coe_smul_of_tower, ← Submodule.coe_sum, Submodule.coe_eq_zero] at hs
exact linearIndependent_iff'.mp b.linearIndependent s g hs
have hsp : ⊤ ≤ span K (Set.range fun i ↦ (M.subtype ∘ b) i) :=
by
rw [← Submodule.span_span_of_tower R, Set.range_comp, ← Submodule.map_span]
simp [b.span_eq, Submodule.map_top, span_eq_top]
Basis.mk hli hsp
