Revision in response to the comments to earlier version:

To introduce the notion of a basis of a finite dimensional vector space over an arbitrary field $\Lambda$, without performing any computation on the data (any matrix manipulation, solution of a system of linear equations, Gauss elimination etc.), the following lemma can be proved:

Each $n-$frame (sequence of linearly independent vectors of length $n$) $\|e_j\|_n$ is maximal in its linear span $[\|e_j\|_n]$ (no longer frame exists in $[\|e_j\|_n]$).

From this lemma one can easily derive all the basic properties and definitions of a finite dimensional vector space including a lucid proof of the Steinitz's theorem on frame extension and many others.

This lemma is equivalent to the following proposition:

For every $n-$frame $\|f_j\|_n$, $f_i\in[\|e_j\|_n], i=1,...,n$,

$$ e_i\in[\|f_j\|_n], i=1,\ldots, n. $$

This system of inclusions can be proved by induction performed on the rank $n$ of the frame $\|e_j\|_n$. The assertion is evident for $n=1$ since in this case the linear span coincides with the family of vectors

$$ [\|e_j\|_1]=\left\{\lambda e_1|\, \lambda\in\Lambda\right\}. $$

Assuming that the assertion is proved for all natural $k\le n-1$, consider the case $k=n$. Introduce $n$ linear mappings

$$ L_i\in Hom\left([\|e_j\|_n], [\|f_1,\ldots,\hat f_i,\ldots,f_n\|]\right),\quad i=1,\ldots,n, $$

by defining $L_i$ on vectors $e_1,\ldots,e_n$ according to the equations

$$ L_ie_j=f_j,\ i\neq j,\ \ L_ie_i=0,\quad i,j=1,\ldots,n. $$

The kernel of $L_i$ coincides with the subspace

$$ ker L_i=\{\lambda e_i\bigr|\lambda\in\Lambda\}, $$

and the image --- with the linear span

$$ im\,L_i=[\|f_1,\ldots,\hat f_i,\ldots f_n\|]. $$

The restriction of $L_i$ on the subspace $[\|f_j\|_n]\subset [\|e_j\|_n]$ has a nonzero kernel since otherwise the $n$-frame $\|L_if_j\|, j=1,\ldots,n$ would be embedded in the linear span of an $(n-1)$-frame $\|f_1,\ldots,\hat f_i,\ldots,f_n\|$, which contradicts the inductive assumption. Hence,

$$ \lambda e_i\in ker L_i\Bigr|_{[\|f_j\|_n]} \ \forall\lambda\in\Lambda,\ i=1,\ldots,n, $$


$$ e_i\in[\|f_j\|_n]\ \forall i=1,\ldots,n. $$

The key point in this proof is that it is based on an argument much weaker than the reduction process - additionally to the list of axioms we only need the notion of the kernel of a linear mapping, without any special constructions performed on the data.

See https://arxiv.org/pdf/1712.04244.pdf for details.

A similar lemma was proved in J. Ford, Avoiding the Exchange Lemma, AMM, Vol. 102, issue 4, 1995, but the proof is based on the technique of matrix manipulations and works only with the fields of characteristic 0.

In our case, we can consider any field - finite or infinite, with any characteristic, without any calculations performed on the data.

And now the question: Is this approach already known?

By the best of my knowledge, all textbooks and articles on the subject use matrix manipulations (solution of linear equations, matrix inversion etc.) in obvious or hidden forms.

Thanks to Pietro Majer for style correction and Martin Sleziak for useful links.

  • 2
    $\begingroup$ This post on Mathematics site seems related: Is the Steinitz exchange lemma necessary to establish invariance of 'basis-size'? $\endgroup$ May 13, 2018 at 9:47
  • $\begingroup$ @MartinSleziak Slightly off-topic, but since I'm not on MSE: perhaps you would like to add a comment somewhere on that other question, that the argument attributed to Beardon was given in an American Math Monthly article of J. W. Ford: doi.org/10.1080/00029890.1995.11990583 $\endgroup$
    – Yemon Choi
    May 21, 2018 at 22:20
  • $\begingroup$ @YemonChoi I've posted a comment under the linked question - I hope approximately what you had in mind. If needed we can continue this discussion in chat - as not to leave here too many comments not directly related to the post. $\endgroup$ May 21, 2018 at 22:46
  • $\begingroup$ @MartinSleziak Both proofs of Beardon and Ford deal with the same problem discussed here, but they do it by matrix computations. Both are constructive proofs. However, the idea above is to give the existence proof of the same lemma as in Fords paper using only the notions of linear mappings and their kernel. $\endgroup$
    – hinkali
    May 22, 2018 at 19:44
  • $\begingroup$ @MartinSleziak Thanks for a useful link $\endgroup$
    – hinkali
    May 22, 2018 at 19:57


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.