English
Let B be nondegenerate and b a basis of M over S. Then the dualSubmodule of the span of range(b) equals the span of the range of the dual basis: B.dualSubmodule(span_R(range b)) = span_R(range (B.dualBasis hB b)).
Русский
Пусть B нондеґенеративна, а b — базис M. Тогда дуальная подмодуля span(range(b)) совпадает с span диапазона двойственного базиса: B.dualSubmodule(span_R(range b)) = span_R(range (B.dualBasis hB b)).
LaTeX
$$$$ B.dualSubmodule(\mathrm{span}_R(\mathrm{range}\, b)) = \mathrm{span}_R(\mathrm{range}\, B.dualBasis(hB,b)). $$$$
Lean4
theorem dualSubmodule_span_of_basis {ι} [Finite ι] [DecidableEq ι] (hB : B.Nondegenerate) (b : Basis ι S M) :
B.dualSubmodule (Submodule.span R (Set.range b)) = Submodule.span R (Set.range <| B.dualBasis hB b) :=
by
cases nonempty_fintype ι
apply le_antisymm
· intro x hx
rw [← (B.dualBasis hB b).sum_repr x]
apply sum_mem
rintro i -
obtain ⟨r, hr⟩ := Submodule.mem_one.mp <| hx (b i) (Submodule.subset_span ⟨_, rfl⟩)
simp only [dualBasis_repr_apply, ← hr, algebraMap_smul]
apply Submodule.smul_mem
exact Submodule.subset_span ⟨_, rfl⟩
· rw [Submodule.span_le]
rintro _ ⟨i, rfl⟩ y hy
obtain ⟨f, rfl⟩ := (Submodule.mem_span_range_iff_exists_fun _).mp hy
simp only [map_sum]
apply sum_mem
rintro j -
rw [← IsScalarTower.algebraMap_smul S (f j), map_smul]
simp_rw [apply_dualBasis_left]
rw [smul_eq_mul, mul_ite, mul_one, mul_zero, ← (algebraMap R S).map_zero, ← apply_ite]
exact Submodule.mem_one.mpr ⟨_, rfl⟩
