English
A lattice viewed as a submodule over ℤ is free, hence admits a basis as a module over ℤ.
Русский
Решётка как подподмодуль над ℤ свободна, значит имеет базис как модуль над ℤ.
LaTeX
$$$\text{Module.Free}_{\mathbb{Z}}(L)$.$$
Lean4
instance instModuleFinite_of_discrete_submodule {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
[FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology L] : Module.Finite ℤ L :=
by
let f := (span ℝ (L : Set E)).subtype
let L₀ := L.comap (f.restrictScalars ℤ)
have h_img : f '' L₀ = L :=
by
rw [← LinearMap.coe_restrictScalars ℤ f, ← Submodule.map_coe (f.restrictScalars ℤ), Submodule.map_comap_eq_self]
exact fun x hx ↦ LinearMap.mem_range.mpr ⟨⟨x, Submodule.subset_span hx⟩, rfl⟩
suffices Module.Finite ℤ L₀
by
have : L₀.map (f.restrictScalars ℤ) = L := SetLike.ext'_iff.mpr h_img
convert this ▸ Module.Finite.map L₀ (f.restrictScalars ℤ)
have : DiscreteTopology L₀ :=
by
refine DiscreteTopology.preimage_of_continuous_injective (L : Set E) ?_ (injective_subtype _)
exact LinearMap.continuous_of_finiteDimensional f
have : IsZLattice ℝ L₀ :=
⟨by
rw [← (Submodule.map_injective_of_injective (injective_subtype _)).eq_iff, Submodule.map_span, Submodule.map_top,
range_subtype, h_img]⟩
exact ZLattice.module_finite ℝ L₀
