English
If a finite collection of finsupp functions spans top, then the index set is finite.
Русский
Если Finite набора функций FinSupp порождает верхнюю грань, то множество индексов конечно.
LaTeX
$$$\\text{Finite}(s) \\land span\\ R\\ s = \\top \\Rightarrow \\#\\iota < \\infty$$$
Lean4
theorem finite_of_span_finite_eq_top_finsupp [Nontrivial M] {ι : Type*} {s : Set (ι →₀ M)} (hs : s.Finite)
(hsspan : span R s = ⊤) : Finite ι :=
suffices ⋃ i ∈ s, i.support.toSet = .univ from .of_finite_univ (this ▸ hs.biUnion fun _ _ ↦ by simp)
have ⟨x, hx⟩ := exists_ne (0 : M)
eq_univ_of_forall fun j ↦
(top_unique (hsspan.ge.trans (span_le_supported_biUnion_support R s)) ▸ mem_top (x := single j x))
((mem_support_single ..).mpr ⟨rfl, hx⟩)
-- One might hope that a finite spanning set implies that any linearly independent set is finite.
-- While this is true over a division ring
-- (simply because any linearly independent set can be extended to a basis),
-- or more generally over a ring satisfying the strong rank condition
-- (which covers all commutative rings; see `LinearIndependent.finite_of_le_span_finite`),
-- this is not true in general.
-- For example, the left ideal generated by the variables in a noncommutative polynomial ring
-- (`FreeAlgebra R ι`) in infinitely many variables (indexed by `ι`) is free
-- with an infinite basis (consisting of the variables).
-- As another example, for any commutative ring R, the ring of column-finite matrices
-- `Module.End R (ℕ →₀ R)` is isomorphic to `ℕ → Module.End R (ℕ →₀ R)` as a module over itself,
-- which also clearly contains an infinite linearly independent set.
