Theory Steinitz
section ‹The Steinitz exchange lemma and dimension over an arbitrary field›
theory Steinitz
imports Vector_Space
begin
text ‹Restore HOL's arithmetic notation, which ‹Vector_Space› (via its ancestor ‹Ring_Theory›)
suppresses to disambiguate locale-parameter binding. Steinitz does not bind ‹+› or ‹-› as
locale parameters, so it is safe (and needed for e.g.\ nat subtraction) to restore them.›
notation plus (infixl ‹+› 65)
notation minus (infixl ‹-› 65)
unbundle uminus_syntax
text ‹Basis-cardinality uniqueness over a ∗‹finite› field was obtained in ‹Vector_Space›
by a counting argument. Here we develop the general (any field, in particular an infinite base
such as ‹ℚ›) theory via the ∗‹Steinitz exchange lemma›: from a spanning set and a linearly
independent set, independent vectors can be exchanged into the spanning set one at a time, whence
@{text "|independent| ≤ |spanning|"} and any two bases have equal size. It is the linchpin for
a general field-extension degree @{text "[K:F]"} and for transitivity of algebraicity.›
context Vector_Space
begin
subsection ‹Span basics›
lemma span_closed:
assumes "S ⊆ V" and "x ∈ span S"
shows "x ∈ V"
using assms lincomb_closed span_def by auto
lemma span_mono:
assumes "S ⊆ T" shows "span S ⊆ span T"
using assms unfolding span_def by blast
text ‹Every vector of @{term S} lies in its span.›
lemma span_incl:
assumes "S ⊆ V" "v ∈ S"
shows "v ∈ span S"
using assms mod.span_incl by (meson in_mono)
lemma span_subset_V:
assumes "S ⊆ V" shows "span S ⊆ V"
using assms span_closed by blast
subsection ‹Extension of a linear combination by zero coefficients›
text ‹Scaling by the field zero gives the zero vector: from @{term "(𝟬 + 𝟬) ⊙ v = 𝟬 ⊙ v ⊕ 𝟬 ⊙ v"}
and cancellation.›
lemmas scale_zero_scalar = mod.scale_zero_scalar
text ‹Extending a linear combination's support by vectors with zero coefficient leaves it unchanged:
the extra terms @{term "𝟬 ⊙ v = 𝟬⇩V"} vanish in the vector sum.›
lemma lincomb_extend_zero:
assumes B: "B ⊆ V" and C: "finite C" "C ⊆ V" and c: "⋀v. v ∈ B ⟹ c v ∈ R"
and disj: "B ∩ C = {}" and czero: "⋀v. v ∈ C ⟹ c v = 𝟬"
and finB: "finite B"
shows "lincomb c (B ∪ C) = lincomb c B"
proof -
have Rc: "(λv. c v ⊙ v) ∈ B → V" using B c by (auto intro: scale_closed)
have RcC: "(λv. c v ⊙ v) ∈ C → V" using C czero by (auto simp: scale_zero_scalar)
have "lincomb c (B ∪ C) = vadd.fincomp (λv. c v ⊙ v) (B ∪ C)" by (simp add: lincomb_def)
also have "… = vadd.fincomp (λv. c v ⊙ v) B ⊕ vadd.fincomp (λv. c v ⊙ v) C"
using finB C(1) disj Rc RcC by (simp add: vadd.fincomp_Un_disjoint)
also have "vadd.fincomp (λv. c v ⊙ v) C = 𝟬⇩V"
using C czero by (auto intro!: vadd.fincomp_unit_eqI simp: scale_zero_scalar)
also have "vadd.fincomp (λv. c v ⊙ v) B ⊕ 𝟬⇩V = vadd.fincomp (λv. c v ⊙ v) B"
using Rc finB by (simp add: vadd.right_unit vadd.fincomp_closed)
finally show ?thesis by (simp add: lincomb_def)
qed
subsection ‹Span is a subspace›
text ‹Over a common finite support @{term B}, linear combinations add coefficientwise:
@{term "lincomb c B ⊕ lincomb d B = lincomb (λv. c v + d v) B"} (by @{thm [source] vadd.fincomp_comp}
and @{thm [source] scale_distrib_add}).›
lemma lincomb_add:
assumes B: "B ⊆ V" and finB: "finite B"
and c: "⋀v. v ∈ B ⟹ c v ∈ R" and d: "⋀v. v ∈ B ⟹ d v ∈ R"
shows "lincomb c B ⊕ lincomb d B = lincomb (λv. c v + d v) B"
proof -
have Rc: "(λv. c v ⊙ v) ∈ B → V" using B c by (auto intro: scale_closed)
have Rd: "(λv. d v ⊙ v) ∈ B → V" using B d by (auto intro: scale_closed)
have "lincomb c B ⊕ lincomb d B
= vadd.fincomp (λv. (c v ⊙ v) ⊕ (d v ⊙ v)) B"
using Rc Rd by (simp add: lincomb_def vadd.fincomp_comp)
also have "… = vadd.fincomp (λv. (c v + d v) ⊙ v) B"
by (rule vadd.fincomp_cong') (use assms in ‹auto simp: scale_distrib_add scale_closed›)
finally show ?thesis by (simp add: lincomb_def)
qed
text ‹A scalar pulls through a vector finite sum: @{term "a ⊙ vadd.fincomp g A = vadd.fincomp (λv. a ⊙ g v) A"}
(by @{thm [source] scale_distrib_vadd}, induction on @{term A}).›
lemmas scale_fincomp = mod.scale_fincomp
text ‹Scaling a linear combination scales its coefficients:
@{term "a ⊙ lincomb c B = lincomb (λv. a ⋅ c v) B"}.›
lemma lincomb_scale:
assumes B: "B ⊆ V" and finB: "finite B" and a: "a ∈ R"
and c: "⋀v. v ∈ B ⟹ c v ∈ R"
shows "a ⊙ lincomb c B = lincomb (λv. a ⋅ c v) B"
proof -
have Rc: "(λv. c v ⊙ v) ∈ B → V" using B c by (auto intro: scale_closed)
have "a ⊙ lincomb c B = vadd.fincomp (λv. a ⊙ (c v ⊙ v)) B"
by (simp add: Rc a finB lincomb_def scale_fincomp)
also have "… = vadd.fincomp (λv. (a ⋅ c v) ⊙ v) B"
using assms by (auto simp: scale_scale intro!: vadd.fincomp_cong' scale_closed)
finally show ?thesis by (simp add: lincomb_def)
qed
subsection ‹Span closure, idempotence and transitivity›
text ‹Two coefficient functions agreeing on the support give the same linear combination.›
lemma lincomb_cong:
assumes "B ⊆ V" and "⋀v. v ∈ B ⟹ d v ∈ R" and "⋀v. v ∈ B ⟹ c v = d v"
shows "lincomb c B = lincomb d B"
unfolding lincomb_def
using assms
by (force intro!: vadd.fincomp_cong'[OF refl] scale_closed)
text ‹Enlarging the support of a linear combination by vectors whose coefficient is @{term 𝟬} leaves
its value unchanged --- the general (non-disjoint) form of @{thm [source] lincomb_extend_zero},
obtained by taking the extra part to be the vectors of ‹D› outside ‹B›.›
lemma lincomb_zero_extend_eq:
assumes B: "B ⊆ V" and D: "finite D" "D ⊆ V" and BD: "B ⊆ D"
and c: "⋀v. v ∈ B ⟹ c v ∈ R" and czero: "⋀v. ⟦ v ∈ D; v ∉ B ⟧ ⟹ c v = 𝟬"
shows "lincomb c D = lincomb c B"
proof -
define E where "E ≡ {v ∈ D. v ∉ B}"
obtain finB: "finite B" and finE: "finite E" and "E ⊆ V"
using finite_subset D BD unfolding E_def by auto
have disj: "B ∩ E = {}" unfolding E_def by blast
have Ezero: "⋀v. v ∈ E ⟹ c v = 𝟬" using czero unfolding E_def by blast
have "lincomb c (B ∪ E) = lincomb c B"
by (rule lincomb_extend_zero[OF B finE ‹E ⊆ V› c disj Ezero finB])
moreover have "B ∪ E = D" using BD unfolding E_def by blast
ultimately show ?thesis by simp
qed
text ‹The zero vector is the empty linear combination, hence lies in every span.›
lemma span_zero: "𝟬⇩V ∈ span S"
by simp
text ‹A span is closed under scalar multiplication.›
lemmas span_scale = mod.span_scale_closed
text ‹A span is closed under vector addition.›
lemmas span_vadd = mod.span_madd_closed
text ‹Consequently a linear combination of vectors ∗‹drawn from a span› stays in the span: induction
on the support, using @{thm [source] span_zero}, @{thm [source] span_scale}, @{thm [source] span_vadd}.›
lemma span_lincomb_closed:
assumes S: "S ⊆ V" and finB: "finite B" and BS: "B ⊆ span S"
and cR: "⋀v. v ∈ B ⟹ c v ∈ R"
shows "lincomb c B ∈ span S"
using finB BS cR
proof (induct B rule: finite_induct)
case empty
have "lincomb c {} = 𝟬⇩V" by (simp add: lincomb_def)
then show ?case by (simp add: span_zero)
next
case (insert x F)
then have sF: "lincomb c F ∈ span S"
by blast
have split: "lincomb c (insert x F) = (c x ⊙ x) ⊕ lincomb c F"
using insert S by (simp add: lincomb_def scale_closed span_closed subset_eq)
have sx: "c x ⊙ x ∈ span S"
using S insert.prems(1,2) span_scale by auto
show ?case using split sx sF S by (auto intro: span_vadd)
qed
text ‹Span is idempotent, so it is a genuine closure operator.›
lemma span_span:
assumes S: "S ⊆ V" shows "span (span S) = span S"
by (simp add: assms mod.span_incl mod.span_minimal mod.span_submodule span_subset_V subset_antisym)
text ‹Transitivity: if @{term S} lies inside the span of @{term T}, its span does too.›
lemma span_trans:
assumes ST: "S ⊆ span T" and T: "T ⊆ V"
shows "span S ⊆ span T"
by (metis ST T span_mono span_span)
text ‹The membership form of transitivity, matching the shape used in the exchange lemma: absorbing a
spanned vector into the generating set does not enlarge the span.›
lemma span_trans_mem:
assumes "S ⊆ V" and "x ∈ span S" and "y ∈ span (insert x S)"
shows "y ∈ span S"
by (metis (no_types, opaque_lifting) assms insert_subset span_incl span_trans subset_eq)
subsection ‹Vector subtraction inside a span›
text ‹Negating a scalar coefficient negates the scaled vector: ‹(- a) ⊙ v› is the vector-group inverse
of ‹a ⊙ v›. From @{term "(a + (- a)) ⊙ v = 𝟬⇩V"}.›
lemmas scale_neg_scalar = mod.scale_neg_scalar
text ‹A span is closed under vector negation.›
lemma span_neg:
assumes "S ⊆ V" and "x ∈ span S"
shows "vadd.inverse x ∈ span S"
using mod.span_submodule mod.submodule_neg assms by presburger
text ‹A span is closed under vector subtraction.›
lemma span_diff:
assumes S: "S ⊆ V" and x: "x ∈ span S" and y: "y ∈ span S"
shows "x ⊕ vadd.inverse y ∈ span S"
by (simp add: S span_neg span_vadd x y)
subsection ‹The exchange step›
text ‹∗‹Exchange step.› If @{term a} lies in the span of @{term "insert b S"} but not in the span of
@{term S}, then @{term b} lies in the span of @{term "insert a S"} --- so @{term b} may be swapped
out for @{term a}. ›
lemma in_span_insert:
assumes S: "S ⊆ V" and b: "b ∈ V"
and a: "a ∈ span (insert b S)" and na: "a ∉ span S"
shows "b ∈ span (insert a S)"
proof -
have aV: "a ∈ V" using a S b span_closed by (metis insert_subset span_subset_V subsetD)
from a obtain c B where a_eq: "a = lincomb c B" and finB: "finite B"
and BbS: "B ⊆ insert b S" and cR: "⋀v. v ∈ B ⟹ c v ∈ R" unfolding span_def by blast
define B0 where "B0 = B ∖ {b}"
define k where "k = (if b ∈ B then c b else 𝟬)"
have kR: "k ∈ R" using cR by (auto simp: k_def additive.unit_closed)
have finB0: "finite B0" using finB by (simp add: B0_def)
have "B0 ⊆ S" "B0 ⊆ V" using BbS S by (auto simp: B0_def)
have bnB0: "b ∉ B0" by (simp add: B0_def)
have cR0: "⋀v. v ∈ B0 ⟹ c v ∈ R" using cR by (auto simp: B0_def)
define r where "r ≡ lincomb c B0"
have rspan: "r ∈ span S" using finB0 ‹B0 ⊆ S› cR0 unfolding r_def span_def by blast
have rV: "r ∈ V" using rspan S span_closed by blast
have a_split: "a = (k ⊙ b) ⊕ r"
proof (cases "b ∈ B")
case True
then have "lincomb c B = lincomb c (insert b B0)"
by (simp add: B0_def insert_absorb)
also have "… = (c b ⊙ b) ⊕ lincomb c B0"
unfolding lincomb_def using finB0 bnB0 cR0 ‹B0 ⊆ V› b cR True
by (subst vadd.fincomp_insert) (auto intro: scale_closed)
finally show ?thesis using True by (simp add: a_eq k_def r_def)
next
case False
then show ?thesis using rV na rspan by (force simp: B0_def r_def a_eq)
qed
have kb: "k ⊙ b ∈ V" using kR b by (rule scale_closed)
have knz: "k ≠ 𝟬"
using a_split b na rV rspan scale_zero_scalar by force
have kinv: "multiplicative.inverse k ∈ R" using kR knz field_inverse by simp
have kk: "multiplicative.inverse k ⋅ k = 𝟭"
using kR knz field_inverse by (simp add: multiplicative.invertible_left_inverse)
have "(k ⊙ b) = a ⊕ vadd.inverse r"
by (simp add: a_split kb rV vadd.associative)
then have b_eq: "b = multiplicative.inverse k ⊙ (a ⊕ vadd.inverse r)"
by (metis b kR kinv kk scale_one scale_scale)
have aS: "a ∈ span (insert a S)" "insert a S ⊆ V"
using aV S by (auto intro: span_incl)
have rS: "r ∈ span (insert a S)" using rspan span_mono[of S "insert a S"] by blast
have "a ⊕ vadd.inverse r ∈ span (insert a S)" using aS rS by (auto intro: span_diff)
then show ?thesis using aS kinv b_eq by (auto intro: span_scale)
qed
text ‹∗‹Delete form.› If @{term a} is spanned by @{term S} but not by @{term "S ∖ {b}"}, then @{term b}
can be exchanged into the generating set in place of @{term a}.›
lemma in_span_delete:
assumes S: "S ⊆ V" and b: "b ∈ V"
and a: "a ∈ span S" and na: "a ∉ span (S ∖ {b})"
shows "b ∈ span (insert a (S ∖ {b}))"
proof -
have "a ∈ span (insert b (S ∖ {b}))" using a span_mono[of S "insert b (S ∖ {b})"] by blast
with assms show ?thesis
by (meson Diff_subset in_span_insert subset_trans)
qed
subsection ‹Independence as irredundancy›
text ‹The geometric reading of linear independence: no member of an independent set lies in the span
of the others. This is the bridge from the coordinate definition @{const lin_indep} to the
span-theoretic exchange arguments. If some @{term "w ∈ B"} were in @{term "span (B ∖ {w})"}, its
witnessing combination, moved to one side with coefficient @{term "- 𝟭"} on @{term w}, would be a
nontrivial dependence.›
lemma lin_indep_not_in_span:
assumes ind: "lin_indep B" and w: "w ∈ B"
shows "w ∉ span (B ∖ {w})"
proof
assume "w ∈ span (B ∖ {w})"
then obtain d C where w_eq: "w = lincomb d C" and finC: "finite C"
and CB: "C ⊆ B ∖ {w}" and dR: "⋀v. v ∈ C ⟹ d v ∈ R" unfolding span_def by blast
have finB: "finite B" and "B ⊆ V" using ind by (auto simp: lin_indep_def)
have wV: "w ∈ V" using w ‹B ⊆ V› by blast
have wnC: "w ∉ C" using CB by blast
define c where "c ≡ (λv. if v = w then - 𝟭 else if v ∈ C then d v else 𝟬)"
have cR: "⋀v. v ∈ B ⟹ c v ∈ R" using dR by (auto simp: c_def additive.unit_closed)
have cPiE: "restrict c B ∈ B →⇩E R" using cR by (auto simp: c_def)
have CsubB: "C ⊆ B" using CB by blast
have insCB: "insert w C ⊆ B" using w CsubB by blast
have "lincomb (restrict c B) B = lincomb (restrict c B) (insert w C)"
proof (intro lincomb_zero_extend_eq finB ‹B ⊆ V› insCB)
show "insert w C ⊆ V" using insCB ‹B ⊆ V› by blast
show "⋀v. v ∈ insert w C ⟹ restrict c B v ∈ R" using insCB cR by auto
qed (auto simp add: c_def)
also have "… = lincomb c (insert w C)"
by (rule lincomb_cong) (use insCB ‹B ⊆ V› cR in auto)
also have "… = (c w ⊙ w) ⊕ lincomb c C"
unfolding lincomb_def using finC wnC wV cR[OF w] cR CsubB ‹B ⊆ V›
by (subst vadd.fincomp_insert) (auto intro!: scale_closed)
also have "lincomb c C = lincomb d C"
by (rule lincomb_cong) (use CsubB ‹B ⊆ V› dR wnC in ‹auto simp: c_def›)
also have "c w ⊙ w = vadd.inverse w" using wV by (simp add: c_def scale_neg_scalar scale_one)
also have "vadd.inverse w ⊕ lincomb d C = vadd.inverse w ⊕ w" using w_eq by simp
also have "… = 𝟬⇩V" using wV by simp
finally have zero: "lincomb (restrict c B) B = 𝟬⇩V" .
from ind cPiE zero have "restrict c B w = 𝟬" using w
using lin_indep_def by blast
then have "(- 𝟭) = 𝟬" using w by (simp add: c_def)
then show False
using additive.commute_iff_inverse nontrivial by fastforce
qed
text ‹Conversely, over a field, a finite set none of whose members lies in the span of the others is
linearly independent. Given a dependence @{term "lincomb c B = 𝟬⇩V"} with some @{term "c w ≠ 𝟬"},
solving for @{term w} exhibits @{term w} in the span of the rest.›
lemma not_in_span_lin_indep:
assumes finB: "finite B" and "B ⊆ V"
and irred: "⋀w. w ∈ B ⟹ w ∉ span (B ∖ {w})"
shows "lin_indep B"
unfolding lin_indep_def
proof (intro strip conjI assms)
show "c v = 𝟬" if cPiE: "c ∈ B →⇩E R" and zero: "lincomb c B = 𝟬⇩V" and v: "v ∈ B" for c v
proof (rule ccontr)
assume cwnz: "c v ≠ 𝟬"
define r where "r ≡ lincomb c (B ∖ {v})"
have rspan: "r ∈ span (B ∖ {v})" using finB cPiE unfolding r_def span_def by blast
have rV: "r ∈ V" using rspan ‹B ⊆ V› span_closed by blast
have wV: "v ∈ V" using v ‹B ⊆ V› by blast
have cwR: "c v ∈ R" using cPiE v by blast
have cww: "c v ⊙ v ∈ V" using cwR wV by (rule scale_closed)
have "B = insert v (B ∖ {v})" using v by blast
then have "lincomb c B = lincomb c (insert v (B ∖ {v}))" by simp
also have "… = (c v ⊙ v) ⊕ lincomb c (B ∖ {v})"
unfolding lincomb_def using finB wV cwR cPiE ‹B ⊆ V›
by (subst vadd.fincomp_insert) (auto intro!: scale_closed)
finally have "c v ⊙ v = vadd.inverse r"
using cww rV r_def vadd.commutative vadd.inverse_equality zero by metis
have cwinv: "multiplicative.inverse (c v) ∈ R" using cwR cwnz field_inverse by simp
have cwcw: "multiplicative.inverse (c v) ⋅ c v = 𝟭"
using cwR cwnz field_inverse by (simp add: multiplicative.invertible_left_inverse)
have "v = multiplicative.inverse (c v) ⊙ (c v ⊙ v)"
using cwinv cwR wV by (simp add: scale_scale[symmetric] cwcw scale_one)
also have "… = multiplicative.inverse (c v) ⊙ vadd.inverse r"
using ‹c v ⊙ v = vadd.inverse r› by simp
finally have "v = multiplicative.inverse (c v) ⊙ vadd.inverse r" .
moreover have "multiplicative.inverse (c v) ⊙ vadd.inverse r ∈ span (B ∖ {v})"
using ‹B ⊆ V› cwinv span_neg[OF _ rspan] by (auto intro: span_scale)
ultimately have "v ∈ span (B ∖ {v})" by simp
with irred[OF v] show False by simp
qed
qed
text ‹Adjoining a vector outside the span preserves linear independence.›
lemma lin_indep_insert:
assumes ind: "lin_indep A" and x: "x ∈ V" and outside: "x ∉ span A"
shows "lin_indep (insert x A)"
proof (rule not_in_span_lin_indep)
show "finite (insert x A)" using ind by (simp add: lin_indep_def)
show "insert x A ⊆ V" using ind x by (auto simp: lin_indep_def)
fix w assume w: "w ∈ insert x A"
have AV: "A ⊆ V" using ind by (simp add: lin_indep_def)
have xA: "x ∉ A"
using AV outside span_incl by blast
show "w ∉ span (insert x A ∖ {w})"
proof
assume wsp: "w ∈ span (insert x A ∖ {w})"
have wA: "w ∈ A" using w
using insert_iff outside wsp by fastforce
have w_outside: "w ∉ span (A ∖ {w})"
using ind wA by (rule lin_indep_not_in_span)
have w_span: "w ∈ span (insert x (A ∖ {w}))"
using wsp w_outside by (metis insert_Diff_if)
have diffV: "A ∖ {w} ⊆ V" using AV by auto
then show False
using outside in_span_insert wA w_outside w_span x by (metis insert_Diff)
qed
qed
subsection ‹Bases span and are independent›
text ‹A spanning set spans the whole space: every vector of @{term V} lies in its span.›
lemma spanning_span_all:
assumes "spanning B" "v ∈ V"
shows "v ∈ span B"
using assms mod.spanningD spanning_def spanning_iff_mod_spanning by meson
text ‹A basis is linearly independent: the coordinate map is injective, and the zero vector is
@{term "lincomb (λ_. 𝟬) B"}, so any coordinate vector mapping to @{term "𝟬⇩V"} must be the zero one.›
lemma basis_lin_indep:
assumes B: "basis B"
shows "lin_indep B"
proof -
have finB: "finite B" and "B ⊆ V" using B by (auto simp: basis_def)
have inj: "inj_on (λc. lincomb c B) (B →⇩E R)" using B by (simp add: basis_def bij_betw_def)
have "c v = 𝟬" if cPiE: "c ∈ B →⇩E R" and zero: "lincomb c B = 𝟬⇩V" and "v∈B" for c v
proof -
define z where "z ≡ restrict (λ_. 𝟬) B"
have zPiE: "z ∈ B →⇩E R" using additive.unit_closed by (auto simp: z_def)
have "lincomb z B = lincomb (λ_. 𝟬) B" by (rule lincomb_cong) (use ‹B ⊆ V› in ‹auto simp: z_def›)
also have "… = 𝟬⇩V" by (simp add: ‹B ⊆ V›)
finally have "lincomb z B = 𝟬⇩V" .
with zero inj cPiE zPiE have "c = z"
by (metis inj_on_eq_iff)
then show "c v = 𝟬"
using ‹v ∈ B› z_def by force
qed
with finB ‹B ⊆ V› show ?thesis unfolding lin_indep_def by blast
qed
text ‹A finite vector-space basis is also a basis in the underlying free-module sense.
This bridge lets constructions defined by the universal property of free modules consume the
coordinate-map basis used by the dimension theory.›
lemma basis_module_basis:
assumes B: "basis B"
shows "mod.module_basis B"
proof (rule mod.module_basisI)
have finB: "finite B" and BV: "B ⊆ V" using B by (auto simp: basis_def)
show "mod.spanning B"
using basis_spanning[OF B] spanning_iff_mod_spanning[OF finB BV] by simp
show "mod.lin_indep B"
using basis_lin_indep[OF B] lin_indep_iff_mod_lin_indep[OF finB BV] by simp
qed
text ‹∗‹Spanning forces equality with a containing independent set.› If @{term "T ⊆ S"}, @{term S} is
independent and @{term "S ⊆ span T"}, then @{term "S = T"}: any @{term "w ∈ S - T"} would lie in
@{term "span T ⊆ span (S ∖ {w})"}, contradicting independence.›
lemma spanning_subset_independent:
assumes TS: "T ⊆ S" and iS: "lin_indep S" and SsT: "S ⊆ span T"
shows "S = T"
proof (rule antisym[OF _ TS])
show "S ⊆ T"
proof (rule ccontr)
assume "¬ S ⊆ T"
then obtain w where w: "w ∈ S" "w ∉ T" "T ⊆ S ∖ {w}" using TS by blast
then have "w ∈ span (S ∖ {w})"
using SsT span_mono by blast
with lin_indep_not_in_span[OF iS w(1)] show False by simp
qed
qed
subsection ‹The Steinitz exchange lemma›
text ‹An independent set contained in the span of a set @{term T} is contained in the span of an
equinumerous ``exchanged'' set drawn from @{term "S ∪ T"}: independent vectors are traded into
@{term T} one at a time. Induction on @{term "card (T ∖ S)"}, following Steinitz.›
lemma exchange_lemma:
assumes "finite T" and "lin_indep S" and "S ⊆ span T" and "T ⊆ V"
shows "∃T'. card T' = card T ∧ finite T' ∧ S ⊆ T' ∧ T' ⊆ S ∪ T ∧ S ⊆ span T'"
using assms
proof (induct "card (T ∖ S)" arbitrary: S T rule: less_induct)
case less
note ft = ‹finite T› and iS = ‹lin_indep S› and spST = ‹S ⊆ span T› and TV = ‹T ⊆ V›
have SV: "S ⊆ V" using iS by (simp add: lin_indep_def)
have finS: "finite S" using iS by (simp add: lin_indep_def)
let ?P = "λT'. card T' = card T ∧ finite T' ∧ S ⊆ T' ∧ T' ⊆ S ∪ T ∧ S ⊆ span T'"
show ?case
proof (cases "S ⊆ T ∨ T ⊆ S")
case True
then show ?thesis
using ft iS spST spanning_subset_independent by auto
next
case False
then obtain b where "¬ S ⊆ T" and b: "b ∈ T" "b ∉ S" "T ∖ {b} ∖ S ⊂ T ∖ S" by blast
then have cardlt: "card (T ∖ {b} ∖ S) < card (T ∖ S)"
using ft by (auto intro: psubset_card_mono)
from b ft have ct0: "card T ≠ 0" by auto
show ?thesis
proof (cases "S ⊆ span (T ∖ {b})")
case True
from ft have ftb: "finite (T ∖ {b})" by auto
have TbV: "T ∖ {b} ⊆ V" using TV by blast
from less(1)[OF cardlt ftb iS True TbV]
obtain U where U: "card U = card (T ∖ {b})" "S ⊆ U" "U ⊆ S ∪ (T ∖ {b})" "S ⊆ span U"
and fu: "finite U" by blast
have bu: "b ∉ U" using b U by blast
then have th2: "card (insert b U) = card T" using card_insert_disjoint[OF fu bu] ct0
using U(1) b(1) ft by (metis card.remove)
have "S ⊆ span (insert b U)"
using U(4) span_mono by blast
then show ?thesis using U b th2 fu by blast
next
case False
then obtain a where a: "a ∈ S" "a ∉ span (T ∖ {b})" and aV: "a ∈ V" and ab: "a ≠ b"
using SV b(2) by blast
have at: "a ∉ T"
using a ab TV by (auto intro: span_incl)
have ft': "finite (insert a (T ∖ {b}))" using ft by auto
have insV: "insert a (T ∖ {b}) ⊆ V" using aV TV by blast
have sp': "S ⊆ span (insert a (T ∖ {b}))"
proof
fix x assume xs: "x ∈ S"
have TbV: "T ∖ {b} ⊆ V" using TV by blast
have aspan: "a ∈ span (insert b (T ∖ {b}))"
using a(1) spST b by (metis insert_Diff subsetD)
have bV: "b ∈ V" using b TV by blast
have bs: "b ∈ span (insert a (T ∖ {b}))"
by (rule in_span_insert[OF TbV bV aspan a(2)])
have xspanT: "x ∈ span T" using xs spST by blast
have "T ⊆ insert a (insert b (T ∖ {b}))" using b by auto
with xspanT have x: "x ∈ span (insert a (insert b (T ∖ {b})))"
using span_mono by blast
show "x ∈ span (insert a (T ∖ {b}))"
using span_trans_mem[OF insV bs] x by (simp add: insert_commute)
qed
have mlt: "card (insert a (T ∖ {b}) ∖ S) < card (T ∖ S)"
using cardlt ft a b by (auto intro: psubset_card_mono)
from less(1)[OF mlt ft' iS sp' insV] a b ft at ct0 ab show ?thesis by auto
qed
qed
qed
subsection ‹The cardinality bound and uniqueness of dimension›
text ‹∗‹Steinitz bound.› A linearly independent set is no larger than any set whose span contains
it --- in particular, than any spanning set.›
theorem independent_le_span:
assumes iS: "lin_indep S" and fT: "finite T" and TV: "T ⊆ V" and spST: "S ⊆ span T"
shows "card S ≤ card T"
by (metis exchange_lemma[OF fT iS spST TV] card_mono)
text ‹∗‹Uniqueness of dimension over an arbitrary field.› Any two bases of @{term V} have the same
cardinality: each is independent and spans, so each bounds the other by the Steinitz bound. This
generalises @{thm [source] basis_card_unique_finite}, dropping the finiteness of the base field.›
theorem basis_card_unique:
assumes B1: "basis B⇩1" and B2: "basis B⇩2"
shows "card B⇩1 = card B⇩2"
proof -
have sp1: "spanning B⇩1" and sp2: "spanning B⇩2" using B1 B2 by (auto intro: basis_spanning)
have i1: "lin_indep B⇩1" and i2: "lin_indep B⇩2" using B1 B2 by (auto intro: basis_lin_indep)
have "finite B⇩1" "finite B⇩2" and B1V: "B⇩1 ⊆ V" and B2V: "B⇩2 ⊆ V"
using B1 B2 by (auto simp: basis_def)
moreover have "B⇩1 ⊆ span B⇩2" "B⇩2 ⊆ span B⇩1"
using sp2 B1V sp1 B2V by (auto intro: spanning_span_all)
ultimately show ?thesis
by (simp add: antisym i1 i2 independent_le_span)
qed
text ‹Consequently the @{const dimension} is the size of ∗‹any› basis, over an arbitrary field ---
the finite-field hypothesis of @{thm [source] dimension_eq} is no longer needed.›
theorem dimension_eq_any_field:
assumes B: "basis B" shows "dimension = card B"
by (metis assms basis_card_unique dimension_def someI)
subsection ‹Existence of a basis›
text ‹@{const basis} is defined as bijectivity of the coordinate map, and
@{thm [source] basis_spanning} and @{thm [source] basis_lin_indep} take it apart. The converse ---
that spanning together with independence ∗‹gives› a basis --- is what one needs in order to
∗‹build› a basis, and it is the missing introduction rule: surjectivity of the coordinate map is
spanning, and injectivity is independence, applied to the difference of two coordinate vectors.›
lemma basisI:
assumes sp: "spanning B" and ind: "lin_indep B"
shows "basis B"
unfolding basis_def
proof (intro conjI)
show finB: "finite B" and BV: "B ⊆ V" using sp by (auto simp: spanning_def)
show "bij_betw (λc. lincomb c B) (B →⇩E R) V"
unfolding bij_betw_def
proof
show "inj_on (λc. lincomb c B) (B →⇩E R)"
proof (rule inj_onI)
fix c d assume c: "c ∈ B →⇩E R" and d: "d ∈ B →⇩E R" and eq: "lincomb c B = lincomb d B"
have cR: "⋀v. v ∈ B ⟹ c v ∈ R" and dR: "⋀v. v ∈ B ⟹ d v ∈ R" using c d by auto
define e where "e ≡ restrict (λv. c v + additive.inverse (d v)) B"
have eR: "⋀v. v ∈ B ⟹ e v ∈ R" using cR dR by (auto simp: e_def)
have ePiE: "e ∈ B →⇩E R" using eR by (simp add: e_def)
have sum_back: "⋀v. v ∈ B ⟹ e v + d v = c v"
using cR dR by (simp add: e_def additive.associative additive.inverse_composition_commute)
have "lincomb e B ⊕ lincomb d B = lincomb (λv. e v + d v) B"
using BV finB eR dR by (rule lincomb_add)
also have "… = lincomb c B" by (rule lincomb_cong) (use BV sum_back cR in auto)
finally have "lincomb e B ⊕ lincomb d B = lincomb d B" using eq by simp
then have "lincomb e B = 𝟬⇩V"
using BV finB eR dR
by (metis lincomb_closed vadd.invertible vadd.invertible_right_cancel vadd.left_unit
vzero_closed)
then have "⋀v. v ∈ B ⟹ e v = 𝟬" using ind ePiE by (simp add: lin_indep_def)
then have "⋀v. v ∈ B ⟹ c v = d v"
using cR dR sum_back by (metis additive.left_unit)
then show "c = d" using c d by (blast intro: PiE_ext)
qed
show "(λc. lincomb c B) ` (B →⇩E R) = V"
proof
show "(λc. lincomb c B) ` (B →⇩E R) ⊆ V"
using finB BV by (auto intro: lincomb_closed)
show "V ⊆ (λc. lincomb c B) ` (B →⇩E R)"
using sp by (auto simp: spanning_def)
qed
qed
qed
text ‹The zero vector space has the empty basis. This small introduction rule is useful when
dimension arguments reduce a kernel or intersection to the trivial subspace.›
lemma basis_empty_trivial:
assumes triv: "V = {𝟬⇩V}"
shows "basis {}"
proof (rule basisI)
show "spanning {}"
unfolding spanning_def
using mod.lincomb_empty triv by auto
show "lin_indep {}" by (simp add: lin_indep_def)
qed
text ‹∗‹Basis extension.› Every finite independent set extends to a basis inside its
union with any given basis. At each step, a basis vector outside the current span is adjoined;
the finite difference from the given basis is the termination measure.›
theorem basis_extension:
assumes ind: "lin_indep A" and B: "basis B"
shows "∃C. A ⊆ C ∧ C ⊆ A ∪ B ∧ basis C"
using assms
proof (induction "card (B ∖ A)" arbitrary: A rule: less_induct)
case less
note ind = less.prems(1) and B = less.prems(2)
have finA: "finite A" and AV: "A ⊆ V" using ind by (auto simp: lin_indep_def)
show ?case
proof (cases "spanning A")
case True
then show ?thesis
using basisI ind by blast
next
case False
have "¬ B ⊆ span A"
proof
assume Bspan: "B ⊆ span A"
have "⋀v. v ∈ V ⟹ v ∈ span A"
using AV B Bspan basis_spanning span_trans spanning_span_all by blast
with mod.spanningI[OF AV] have "spanning A"
unfolding spanning_iff_mod_spanning[OF finA AV] .
then show False using False by contradiction
qed
then obtain b where b: "b ∈ B" "b ∉ span A" by blast
have BV: "B ⊆ V" and finB: "finite B" using B by (auto simp: basis_def)
have bV: "b ∈ V" using b BV by blast
have bA: "b ∉ A"
using AV b(2) span_incl by blast
have "0 < card (B ∖ A)"
using finB b bA by (simp add: card_gt_0_iff) blast
then have measure: "card (B ∖ insert b A) < card (B ∖ A)"
by (simp add: b(1) bA)
obtain C where C: "insert b A ⊆ C" "C ⊆ insert b A ∪ B" "basis C"
using B b(2) bV ind less.hyps lin_indep_insert measure by meson
have "A ⊆ C" using C(1) by blast
moreover have "C ⊆ A ∪ B" using C b(1) by blast
ultimately show ?thesis using C(3) by blast
qed
qed
text ‹∗‹Every finitely spanned space has a basis, extracted from any finite spanning set.› Discard
redundant vectors one at a time: if some @{term "w ∈ B"} lies in the span of the others then
@{term "B ∖ {w}"} still spans (by @{thm [source] span_trans_mem}), and it is strictly smaller, so
the process terminates. What it terminates at is a set no member of which is spanned by the rest,
which by @{thm [source] not_in_span_lin_indep} is exactly independence.
This is the result that turns ``finite-dimensional'' into ``has a basis'', and hence the one that
lets the dimension theory above be applied to a space presented by generators.›
theorem basis_exists_from_spanning:
assumes "spanning B"
shows "∃B' ⊆ B. basis B'"
using assms
proof (induction "card B" arbitrary: B rule: less_induct)
case less
have finB: "finite B" and BV: "B ⊆ V" using less.prems by (auto simp: spanning_def)
show ?case
proof (cases "∃w ∈ B. w ∈ span (B ∖ {w})")
case True
then obtain w where w: "w ∈ B" and wsp: "w ∈ span (B ∖ {w})" by blast
have sub: "B ∖ {w} ⊆ V" using BV by blast
have "spanning (B ∖ {w})"
unfolding spanning_def
proof (intro conjI ballI finB sub)
show "finite (B ∖ {w})" using finB by blast
fix v assume v: "v ∈ V"
have "v ∈ span (B ∖ {w})" using sub wsp
using less.prems span_trans_mem spanning_span_all v w by (metis insert_Diff)
then show "∃c ∈ (B ∖ {w}) →⇩E R. v = lincomb c (B ∖ {w})"
proof -
obtain c C where veq: "v = lincomb c C" and finC: "finite C" and CB: "C ⊆ B ∖ {w}"
and cR: "⋀u. u ∈ C ⟹ c u ∈ R" using ‹v ∈ span (B ∖ {w})› unfolding span_def by blast
define d where "d ≡ restrict (λu. if u ∈ C then c u else 𝟬) (B ∖ {w})"
have dR: "⋀u. u ∈ B ∖ {w} ⟹ d u ∈ R" using cR by (auto simp: d_def)
have dPiE: "d ∈ (B ∖ {w}) →⇩E R" using dR by (simp add: d_def)
have "lincomb d (B ∖ {w}) = lincomb d C"
proof (intro CB sub lincomb_zero_extend_eq)
show "⋀u. ⟦ u ∈ B ∖ {w}; u ∉ C ⟧ ⟹ d u = 𝟬" by (simp add: d_def)
qed (use finB CB sub dR in auto)
also have "… = lincomb c C" by (rule lincomb_cong) (use CB sub cR in ‹auto simp: d_def›)
finally have "lincomb d (B ∖ {w}) = v" using veq by simp
then show ?thesis using dPiE by blast
qed
qed
moreover have "card (B ∖ {w}) < card B"
by (meson finB w card_Diff1_less_iff)
ultimately show ?thesis using less.hyps by blast
next
case False
then show ?thesis
using BV basisI finB less.prems not_in_span_lin_indep by auto
qed
qed
text ‹A finite vector space has cardinality @{term "card R ^ dimension"}.›
theorem card_eq_card_base_pow_dimension:
assumes finV: "finite V"
shows "card V = card R ^ dimension"
proof -
have spanV: "spanning V"
using finV mod.spanning_whole spanning_iff_mod_spanning by blast
obtain B where basis: "basis B"
using basis_exists_from_spanning[OF spanV] by blast
then show ?thesis
using card_eq_card_base_pow_dim dimension_eq_any_field by presburger
qed
text ‹A uniform finite bound on the cardinalities of independent sets already gives a basis. Choose
an independent set of maximum cardinality; if a vector lay outside its span, adjoining that vector
would produce a strictly larger independent set.›
theorem basis_exists_of_independent_card_bound:
assumes bound: "⋀A. lin_indep A ⟹ card A ≤ n"
shows "∃A. basis A"
proof -
define sizes where "sizes ≡ {card A | A. lin_indep A}"
obtain sizes_nonempty: "sizes ≠ {}" and sizes_bounded: "sizes ⊆ {..n}"
using assms unfolding sizes_def lin_indep_def by auto
have finite_sizes: "finite sizes"
using sizes_bounded by (rule finite_subset) simp
have "Max sizes ∈ sizes" by (rule Max_in[OF finite_sizes sizes_nonempty])
then obtain A where indA: "lin_indep A" and maxA: "Max sizes = card A"
unfolding sizes_def by blast
have finA: "finite A" and AV: "A ⊆ V" using indA by (auto simp: lin_indep_def)
have "mod.spanning A"
proof (rule mod.spanningI[OF AV])
fix x assume xV: "x ∈ V"
show "x ∈ span A"
proof (rule ccontr)
assume outside: "x ∉ span A"
have ind_insert: "lin_indep (insert x A)"
by (rule lin_indep_insert[OF indA xV outside])
have xA: "x ∉ A"
using AV outside span_incl by force
have "card (insert x A) ≤ Max sizes"
using Max_ge finite_sizes ind_insert sizes_def by blast
then show False
using finA maxA xA by force
qed
qed
then show ?thesis
using basisI finA indA mod.spanning_def spanning_iff_mod_spanning by meson
qed
text ‹Hence the dimension of a finitely spanned space is bounded by any spanning set.›
corollary dimension_le_spanning:
assumes "spanning B" shows "dimension ≤ card B"
proof -
obtain B' where B'B: "B' ⊆ B" and B': "basis B'"
using assms by (blast dest: basis_exists_from_spanning)
then show ?thesis using dimension_eq_any_field
using assms card_mono spanning_def by auto
qed
end
context vector_subspace
begin
text ‹Linear combinations and spans do not depend on whether their vectors are viewed in the
ambient space or in the subspace; only the carrier side-condition changes.›
lemma sub_fincomp_eq:
assumes finA: "finite A" and f: "f ∈ A → W"
shows "sub.vadd.fincomp f A = vadd.fincomp f A"
using finA f
proof (induction A rule: finite_induct)
case empty
then show ?case by simp
next
case (insert x A)
obtain fxV: "f x ∈ V" and fAV: "f ∈ A → V"
using Module.submodule_subset W_submodule insert.prems mod.Module_axioms by fastforce
with insert show ?case
by auto
qed
lemma sub_lincomb_eq:
assumes finA: "finite A" and AW: "A ⊆ W"
and c: "⋀v. v ∈ A ⟹ c v ∈ R"
shows "sub.lincomb c A = lincomb c A"
unfolding sub.lincomb_def lincomb_def
using AW c by (auto intro!: sub_fincomp_eq[OF finA] sub.scale_closed)
lemma sub_span_eq:
assumes AW: "A ⊆ W"
shows "sub.span A = span A"
proof
show "sub.span A ⊆ span A"
proof
fix x assume "x ∈ sub.span A"
then obtain c C where C: "finite C" "C ⊆ A" "sub.mod.coeffs_on c C"
"x = sub.lincomb c C" and CW: "C ⊆ W" using assms sub.mod.spanE by (metis subset_trans)
have x_eq: "x = lincomb c C" using C sub_lincomb_eq[OF C(1) CW] sub.mod.coeffs_onD by simp
show "x ∈ span A"
using C mod.spanI x_eq by force
qed
show "span A ⊆ sub.span A"
proof
fix x assume "x ∈ span A"
then obtain c C where C: "finite C" "C ⊆ A" "mod.coeffs_on c C" "x = lincomb c C"
and CW: "C ⊆ W" using assms mod.spanE by (metis subset_trans)
have x_eq: "x = sub.lincomb c C" using C sub_lincomb_eq[OF C(1) CW] mod.coeffs_onD by simp
show "x ∈ sub.span A"
using C sub.mod.spanI x_eq by force
qed
qed
lemma sub_lin_indep_iff:
assumes AW: "A ⊆ W"
shows "sub.lin_indep A ⟷ lin_indep A"
proof
assume ind: "sub.lin_indep A"
show "lin_indep A"
unfolding lin_indep_def
proof (intro conjI ballI impI)
show finA: "finite A"
using ind by (simp add: sub.lin_indep_def)
show "A ⊆ V" using AW W_submodule mod.submodule_subset by blast
fix c v
assume c: "c ∈ A →⇩E R" and zero: "lincomb c A = 𝟬⇩V" and v: "v ∈ A"
have coeff: "⋀u. u ∈ A ⟹ c u ∈ R" using c by auto
have "sub.lincomb c A = 𝟬⇩V" using zero sub_lincomb_eq[OF finA AW coeff] by simp
then show "c v = 𝟬" using ind c v by (simp add: sub.lin_indep_def)
qed
next
assume ind: "lin_indep A"
show "sub.lin_indep A"
unfolding sub.lin_indep_def
proof (intro conjI ballI impI AW)
show finA: "finite A"
using ind by (simp add: lin_indep_def)
fix c v
assume c: "c ∈ A →⇩E R" and zero: "sub.lincomb c A = 𝟬⇩V" and v: "v ∈ A"
have coeff: "⋀u. u ∈ A ⟹ c u ∈ R" using c by auto
have "lincomb c A = 𝟬⇩V" using zero sub_lincomb_eq[OF finA AW coeff] by simp
then show "c v = 𝟬" using ind c v by (simp add: lin_indep_def)
qed
qed
text ‹∗‹Subspaces of finite-dimensional spaces have bases.› The possible cardinalities of
independent subsets of @{term W} are bounded by the size of an ambient basis. Choose an
independent set of maximum cardinality; adjoining any vector outside its span would contradict
maximality, so it spans the subspace.›
theorem subspace_basis_exists:
assumes B: "basis B"
shows "∃A. sub.basis A"
proof -
define sizes where "sizes ≡ {card A | A. sub.lin_indep A}"
have finB: "finite B" and BV: "B ⊆ V" using B by (auto simp: basis_def)
have sizes_nonempty: "sizes ≠ {}"
unfolding sizes_def using sub.lin_indep_def by force
have sizes_bounded: "sizes ⊆ {..card B}"
proof
fix n assume "n ∈ sizes"
then obtain A where A: "sub.lin_indep A" "n = card A" and AW: "A ⊆ W"
using sizes_def sub.lin_indep_def by auto
then have indA: "lin_indep A" using sub_lin_indep_iff[OF AW] A by simp
have "A ⊆ span B" using basis_spanning[OF B]
using indA lin_indep_def spanning_span_all by blast
then show "n ∈ {..card B}" using A
by (simp add: BV finB indA independent_le_span)
qed
have finite_sizes: "finite sizes"
using sizes_bounded by (rule finite_subset) simp
have "Max sizes ∈ sizes" by (rule Max_in[OF finite_sizes sizes_nonempty])
then obtain A where indA: "sub.lin_indep A" and maxA: "Max sizes = card A"
and finA: "finite A" and AW: "A ⊆ W"
unfolding sizes_def using sub.lin_indep_def by auto
have "sub.mod.spanning A"
proof (rule sub.mod.spanningI[OF AW])
fix x assume xW: "x ∈ W"
show "x ∈ sub.span A"
proof (rule ccontr)
assume outside: "x ∉ sub.span A"
have ind_insert: "sub.lin_indep (insert x A)"
by (rule sub.lin_indep_insert[OF indA xW outside])
have insert_size: "card (insert x A) = Suc (card A)"
by (meson AW finA outside sub.span_incl card_insert_disjoint)
then show False
using insert_size maxA Max_ge finite_sizes ind_insert sizes_def by fastforce
qed
qed
then have "sub.basis A" using indA
by (simp add: AW finA sub.basisI sub.spanning_iff_mod_spanning)
then show ?thesis by blast
qed
text ‹A subspace of a finite-dimensional space cannot have larger dimension than the
ambient space. This is the set-based counterpart of the standard monotonicity theorem for
dimension: a subspace basis is also ambiently independent, so Steinitz bounds it by any
ambient basis.›
theorem subspace_dimension_le:
assumes B: "basis B"
shows "sub.dimension ≤ dimension"
proof -
obtain A where A: "sub.basis A" and AW: "A ⊆ W" and indA: "lin_indep A"
using subspace_basis_exists[OF B] sub.basis_def sub.basis_lin_indep sub_lin_indep_iff by metis
have finB: "finite B" and BV: "B ⊆ V" using B by (auto simp: basis_def)
have AV: "A ⊆ V" using AW W_submodule mod.submodule_subset by blast
have "A ⊆ span B"
using basis_spanning[OF B] AV by (auto intro: spanning_span_all)
then show ?thesis
using sub.dimension_eq_any_field[OF A] dimension_eq_any_field[OF B]
by (simp add: BV finB indA independent_le_span)
qed
text ‹In finite dimension, a subspace has full dimension exactly when it is the whole
ambient space. For the non-trivial direction, extend a subspace basis to an ambient basis;
equality of dimensions leaves no additional basis vectors.›
theorem subspace_eq_ambient_iff_dimension_eq:
assumes B: "basis B"
shows "W = V ⟷ sub.dimension = dimension"
proof
assume WV: "W = V"
have subB: "sub.basis B" using B WV by simp
show "sub.dimension = dimension"
using sub.dimension_eq_any_field[OF subB] dimension_eq_any_field[OF B] by simp
next
assume dim: "sub.dimension = dimension"
obtain A where A: "sub.basis A"
using subspace_basis_exists[OF B] by blast
have AW: "A ⊆ W" using A by (simp add: sub.basis_def)
have indA: "lin_indep A"
using sub.basis_lin_indep[OF A] sub_lin_indep_iff[OF AW] by simp
obtain C where AC: "A ⊆ C" and C: "basis C" and finC: "finite C"
using basis_extension[OF indA B] basis_def by blast
then have "A=C"
using A card_subset_eq dim dimension_eq_any_field sub.dimension_eq_any_field by auto
then have "V ⊆ W"
using C basis_spanning spanning_span_all AW W_submodule mod.span_minimal by blast
then show "W = V"
using W_submodule mod.submodule_subset by blast
qed
text ‹The only zero-dimensional subspace is the trivial one. The ambient basis assumption
supplies a basis of the subspace; dimension zero then forces that basis to be empty.›
theorem subspace_dimension_eq_zero_iff:
assumes B: "basis B"
shows "sub.dimension = 0 ⟷ W = {𝟬⇩V}"
proof
assume dim: "sub.dimension = 0"
obtain A where A: "sub.basis A" "finite A"
using subspace_basis_exists[OF B] sub.basis_def by blast
then have "A = {}" using sub.dimension_eq_any_field dim by fastforce
then have empty_spanning: "sub.spanning {}"
using A sub.basis_spanning by blast
then show "W = {𝟬⇩V}"
unfolding sub.spanning_def by auto
next
assume W: "W = {𝟬⇩V}"
then show "sub.dimension = 0"
using sub.dimension_eq_any_field sub.basis_empty_trivial by force
qed
end
end