Vector-space freeness from maximal independence
ID: vector-space-freeness-from-maximal-independence
Order the linearly independent subsets of a vector space by inclusion. A chain's union is independent, since every finite relation is contained in one chain member. Zorn's lemma gives a maximal independent subset. A vector outside its span could be adjoined while preserving independence, so it spans. Sending finite-support coefficient families to their linear combinations gives an isomorphism from the free module on that subset to . This supplies an arbitrary, possibly infinite-dimensional basis using the axiom of choice; no pre-existing basis theorem is invoked.
New to topics? Read the docs here!