Don't understand the example about Basis

Stream: mathlib4

[Ching-Tsun Chou]

In sec.9.4.2 of "Mathematics in Lean" there is the following example:

noncomputable example (b : ι → V) (b_indep : LinearIndependent K b)
    (b_spans : ∀ v, v ∈ Submodule.span K (Set.range b)) : Basis ι K V :=
  Basis.mk b_indep (fun v _ ↦ b_spans v)

Where does the assumption that b has finite support come in? Does the theorem hold even when b doesn't have finite support?

[Andrew Yang]

I don’t think this lemma assumes b has finite support?

[Ching-Tsun Chou]

According to the discussion before the example (see below), it seems to me that the finite support property must be implied by one of the assumptions. But which one?

variable {ι : Type*} (B : Basis ι K V) (v : V) (i : ι)

-- the linear isomorphism with the model space given by ``B``
#check (B.repr : V ≃ₗ[K] ι →₀ K)

[Andrew Yang]

In paper maths, a basis is a family of vectors $v_i$ such that every $v$ can be represented by $v = \sum a_i v_i$ uniquely, where all but finitely many $a_i = 0$. So the "finite support" condition is happening on the coefficients and not on the family of vectors itself.

[Edward van de Meent]

this fact in this case is expressed by b_spans

[Ching-Tsun Chou]

Are you sure? It seems to me that the span of an infinite set of vectors makes perfect sense. Indeed, the following is the definition of span:

/-- The span of a set `s ⊆ M` is the smallest submodule of M that contains `s`. -/
def span (s : Set M) : Submodule R M :=
  sInf { p | s ⊆ p }

[Edward van de Meent]

right, however the fact that elements of the span are finite combinations is by definition.

[Edward van de Meent]

that is precisely what V ≃ₗ[K] ι →₀ K means: each element of V is a linear combination of a finite subset of the basis elements

[Ching-Tsun Chou]

But the definition of Submodule.span shown above doesn't say anything about linear combinations (finite or not), does it? It merely says that the span is the infimum of all submodules containing the set s.

[Ching-Tsun Chou]

Since the submodules of a module form a complete lattice, the infimum exists.

[Edward van de Meent]

however, since it is only closed under binary addition by definition, it has to be only finite combinations, no?

[Etienne Marion]

Yes but you can prove that this infimum is equal to the set of all finite linear combinations (because it is a submodule and must be contained in any submodule containing s)

[Edward van de Meent]

it doesn't even necessarily make sense in this context to talk about infinite sums

[Edward van de Meent]

so how could it include those?

[Patrick Massot]

Edward van de Meent said:

right, however the fact that elements of the span are finite combinations is by definition.

No, this is not the definition. You could define it that way but it would be really bad, and this is certainly not what Mathlib is doing.

[Ching-Tsun Chou]

Thinking more, I really don't understand this example. Suppose we define:

def b : ℕ → ℕ → ℝ := fun i j : ℕ ↦ if j = i then 1 else (0 : ℝ)

and define V to be the subtype of ℕ → ℝ consisting of all finite linear combinations of (b 0), (b 1), ... (Sorry, I still don't know enough Lean+Mathlib to know how to write this.) Then b_spans is true by definition and b_indep is true as well, right? But clearly b does not have finite support. Where did I go wrong in my reasoning?

[Antoine Chambert-Loir]

A basis $(e_i)_{i\in I}$ in a vector space $V$ over a field $F$ is a family of vectors such that every vector in $V$ is a linear combination of members of the basis, in a unique way. That is, for every vector $v\in V$, there exists a unique family of scalars $(a_i)_{i\in I}$, all but finitely many of them being zero, such that $v=\sum_{i\in I} a_i e_i$. In this expression, only finitely many terms $a_i e_i$ are nonzero, so that the “infinite” sum makes sense. As often in math, families are formalized as functions $e\colon I \to V$, and you see, that function does not need to have finite support—in fact, no $e_i$ can be zero. It is the family of scalars $a\colon I\to F$ which has finite support.

[Antoine Chambert-Loir]

To address your question, it is almost impossible in mathematics to make sense to an erroneous discussion, and, to be frank, I don't understand what you have in mind. So I invite you to write down explicitly (on a sheet of paper, not on Zulip) what you had in mind and spend enough time to track down what is wrong and fix your mental idea of a basis in a vector space.

[Ching-Tsun Chou]

Ah, I see where my confusion was! If (B : Basis ι K V), then (B.repr v) has finite support, but V itself may well be infinite-dimensional.

[Ching-Tsun Chou]

In my example, V is isomorphic to ℕ →₀ ℝ, which is infinite-dimensional even though each vector in it has finite support.