Theory VectorSpace
section ‹Basic theory of vector spaces, using locales›
theory VectorSpace
imports Main
"HOL-Algebra.Module"
"HOL-Algebra.Coset"
RingModuleFacts
MonoidSums
LinearCombinations
SumSpaces
begin
subsection ‹Basic definitions and facts carried over from modules›
text ‹A ‹vectorspace› is a module where the ring is a field.
Note that we switch notation from $(R, M)$ to $(K, V)$.›
locale vectorspace =
module?: module K V + field?: field K
for K and V
text ‹A ‹subspace› of a vectorspace is a nonempty subset
that is closed under addition and scalar multiplication. These properties
have already been defined in submodule. Caution: W is a set, while V is
a module record. To get W as a vectorspace, write vs W.›
locale subspace =
fixes K and W and V (structure)
assumes vs: "vectorspace K V"
and submod: "submodule K W V"
lemma (in vectorspace) is_module[simp]:
"subspace K W V⟹submodule K W V"
by (unfold subspace_def, auto)
text ‹We introduce some basic facts and definitions copied from module.
We introduce some abbreviations, to match convention.›
abbreviation (in vectorspace) vs::"'c set ⇒ ('a, 'c, 'd) module_scheme"
where "vs W ≡ V⦇carrier :=W⦈"
lemma (in vectorspace) carrier_vs_is_self [simp]:
"carrier (vs W) = W"
by auto
lemma (in vectorspace) subspace_is_vs:
fixes W::"'c set"
assumes 0: "subspace K W V"
shows "vectorspace K (vs W)"
proof -
from 0 show ?thesis
apply (unfold vectorspace_def subspace_def, auto)
by (intro submodule_is_module, auto)
qed
abbreviation (in module) subspace_sum:: "['c set, 'c set] ⇒ 'c set"
where "subspace_sum W1 W2 ≡submodule_sum W1 W2"
lemma (in vectorspace) vs_zero_lin_dep:
assumes h2: "S⊆carrier V" and h3: "lin_indpt S"
shows "𝟬⇘V⇙ ∉ S"
proof -
have vs: "vectorspace K V"..
from vs have nonzero: "carrier K ≠{𝟬⇘K⇙}"
by (metis one_zeroI zero_not_one)
from h2 h3 nonzero show ?thesis by (rule zero_nin_lin_indpt)
qed
text ‹A ‹linear_map› is a module homomorphism between 2 vectorspaces
over the same field.›
locale linear_map =
V?: vectorspace K V + W?: vectorspace K W
+ mod_hom?: mod_hom K V W T
for K and V and W and T
context linear_map
begin
lemmas T_hom = f_hom
lemmas T_add = f_add
lemmas T_smult = f_smult
lemmas T_im = f_im
lemmas T_neg = f_neg
lemmas T_minus = f_minus
lemmas T_ker = f_ker
abbreviation imT:: "'e set"
where "imT ≡ mod_hom.im"
abbreviation kerT:: "'c set"
where "kerT ≡ mod_hom.ker"
lemmas T0_is_0[simp] = f0_is_0
lemma kerT_is_subspace: "subspace K ker V"
proof -
have vs: "vectorspace K V"..
from vs show ?thesis
apply (unfold subspace_def, auto)
by (rule ker_is_submodule)
qed
lemma imT_is_subspace: "subspace K imT W"
proof -
have vs: "vectorspace K W"..
from vs show ?thesis
apply (unfold subspace_def, auto)
by (rule im_is_submodule)
qed
end
lemma vs_criteria:
fixes K and V
assumes field: "field K"
and zero: "𝟬⇘V⇙∈ carrier V"
and add: "∀v w. v∈carrier V ∧ w∈carrier V⟶ v⊕⇘V⇙ w∈ carrier V"
and neg: "∀v∈carrier V. (∃neg_v∈carrier V. v⊕⇘V⇙neg_v=𝟬⇘V⇙)"
and smult: "∀c v. c∈ carrier K ∧ v∈carrier V⟶ c⊙⇘V⇙ v ∈ carrier V"
and comm: "∀v w. v∈carrier V ∧ w∈carrier V⟶ v⊕⇘V⇙ w=w⊕⇘V⇙ v"
and assoc: "∀v w x. v∈carrier V ∧ w∈carrier V ∧ x∈carrier V⟶ (v⊕⇘V⇙ w)⊕⇘V⇙ x= v⊕⇘V⇙ (w⊕⇘V⇙ x)"
and add_id: "∀v∈carrier V. (v⊕⇘V⇙ 𝟬⇘V⇙ =v)"
and compat: "∀a b v. a∈ carrier K ∧ b∈ carrier K ∧ v∈carrier V⟶ (a⊗⇘K⇙ b)⊙⇘V⇙ v =a⊙⇘V⇙ (b⊙⇘V⇙ v)"
and smult_id: "∀v∈carrier V. (𝟭⇘K⇙ ⊙⇘V⇙ v =v)"
and dist_f: "∀a b v. a∈ carrier K ∧ b∈ carrier K ∧ v∈carrier V⟶ (a⊕⇘K⇙ b)⊙⇘V⇙ v =(a⊙⇘V⇙ v) ⊕⇘V⇙ (b⊙⇘V⇙ v)"
and dist_add: "∀a v w. a∈ carrier K ∧ v∈carrier V ∧ w∈carrier V⟶ a⊙⇘V⇙ (v⊕⇘V⇙ w) =(a⊙⇘V⇙ v) ⊕⇘V⇙ (a⊙⇘V⇙ w)"
shows "vectorspace K V"
proof -
from field have 1: "cring K" by (unfold field_def domain_def, auto)
from assms 1 have 2: "module K V" by (intro module_criteria, auto)
from field 2 show ?thesis by (unfold vectorspace_def module_def, auto)
qed
text ‹For any set $S$, the space of functions $S\to K$ forms a vector space.›
lemma (in vectorspace) func_space_is_vs:
fixes S
shows "vectorspace K (func_space S)"
proof -
have 0: "field K"..
have 1: "module K (func_space S)" by (rule func_space_is_module)
from 0 1 show ?thesis by (unfold vectorspace_def module_def, auto)
qed
lemma direct_sum_is_vs:
fixes K V1 V2
assumes h1: "vectorspace K V1" and h2: "vectorspace K V2"
shows "vectorspace K (direct_sum V1 V2)"
proof -
from h1 h2 have mod: "module K (direct_sum V1 V2)" by (unfold vectorspace_def, intro direct_sum_is_module, auto)
from mod h1 show ?thesis by (unfold vectorspace_def, auto)
qed
lemma inj1_linear:
fixes K V1 V2
assumes h1: "vectorspace K V1" and h2: "vectorspace K V2"
shows "linear_map K V1 (direct_sum V1 V2) (inj1 V1 V2)"
proof -
from h1 h2 have mod: "mod_hom K V1 (direct_sum V1 V2) (inj1 V1 V2)" by (unfold vectorspace_def, intro inj1_hom, auto)
from mod h1 h2 show ?thesis
by (unfold linear_map_def vectorspace_def , auto, intro direct_sum_is_module, auto)
qed
lemma inj2_linear:
fixes K V1 V2
assumes h1: "vectorspace K V1" and h2: "vectorspace K V2"
shows "linear_map K V2 (direct_sum V1 V2) (inj2 V1 V2)"
proof -
from h1 h2 have mod: "mod_hom K V2 (direct_sum V1 V2) (inj2 V1 V2)" by (unfold vectorspace_def, intro inj2_hom, auto)
from mod h1 h2 show ?thesis
by (unfold linear_map_def vectorspace_def , auto, intro direct_sum_is_module, auto)
qed
text ‹For subspaces $V_1,V_2\subseteq V$, the map $V_1\oplus V_2\to V$ given by $(v_1,v_2)\mapsto
v_1+v_2$ is linear.›
lemma (in vectorspace) sum_map_linear:
fixes V1 V2
assumes h1: "subspace K V1 V" and h2: "subspace K V2 V"
shows "linear_map K (direct_sum (vs V1) (vs V2)) V (λ v. (fst v) ⊕⇘V⇙ (snd v))"
proof -
from h1 h2 have mod: "mod_hom K (direct_sum (vs V1) (vs V2)) V (λ v. (fst v) ⊕⇘V⇙ (snd v))"
by ( intro sum_map_hom, unfold subspace_def, auto)
from mod h1 h2 show ?thesis
apply (unfold linear_map_def, auto) apply (intro direct_sum_is_vs subspace_is_vs, auto)..
qed
lemma (in vectorspace) sum_is_subspace:
fixes W1 W2
assumes h1: "subspace K W1 V" and h2: "subspace K W2 V"
shows "subspace K (subspace_sum W1 W2) V"
proof -
from h1 h2 have mod: "submodule K (submodule_sum W1 W2) V"
by ( intro sum_is_submodule, unfold subspace_def, auto)
from mod h1 h2 show ?thesis
by (unfold subspace_def, auto)
qed
text ‹If $W_1,W_2\subseteq V$ are subspaces, $W_1\subseteq W_1 + W_2$›
lemma (in vectorspace) in_sum_vs:
fixes W1 W2
assumes h1: "subspace K W1 V" and h2: "subspace K W2 V"
shows "W1 ⊆ subspace_sum W1 W2"
proof -
from h1 h2 show ?thesis by (intro in_sum, unfold subspace_def, auto)
qed
lemma (in vectorspace) vsum_comm:
fixes W1 W2
assumes h1: "subspace K W1 V" and h2: "subspace K W2 V"
shows "(subspace_sum W1 W2) = (subspace_sum W2 W1)"
proof -
from h1 h2 show ?thesis by (intro msum_comm, unfold subspace_def, auto)
qed
text ‹If $W_1,W_2\subseteq V$ are subspaces, then $W_1+W_2$ is the minimal subspace such that
both $W_1\subseteq W$ and $W_2\subseteq W$.›
lemma (in vectorspace) vsum_is_minimal:
fixes W W1 W2
assumes h1: "subspace K W1 V" and h2: "subspace K W2 V" and h3: "subspace K W V"
shows "(subspace_sum W1 W2) ⊆ W ⟷ W1 ⊆ W ∧ W2 ⊆ W"
proof -
from h1 h2 h3 show ?thesis by (intro sum_is_minimal, unfold subspace_def, auto)
qed
lemma (in vectorspace) span_is_subspace:
fixes S
assumes h2: "S⊆carrier V"
shows "subspace K (span S) V"
proof -
have 0: "vectorspace K V"..
from h2 have 1: "submodule K (span S) V" by (rule span_is_submodule)
from 0 1 show ?thesis by (unfold subspace_def mod_hom_def linear_map_def, auto)
qed
subsubsection ‹Facts specific to vector spaces›
text ‹If $av = w$ and $a\neq 0$, $v=a^{-1}w$.›
lemma (in vectorspace) mult_inverse:
assumes h1: "a∈carrier K" and h2: "v∈carrier V" and h3: "a ⊙⇘V⇙ v = w" and h4: "a≠𝟬⇘K⇙"
shows "v = (inv⇘K⇙ a )⊙⇘V⇙ w"
proof -
from h1 h2 h3 have 1: "w∈carrier V" by auto
from h3 1 have 2: "(inv⇘K⇙ a )⊙⇘V⇙(a ⊙⇘V⇙ v) =(inv⇘K⇙ a )⊙⇘V⇙w" by auto
from h1 h4 have 3: "inv⇘K⇙ a∈carrier K" by auto
interpret g: group "(units_group K)" by (rule units_form_group)
have f: "field K"..
from f h1 h4 have 4: "a∈Units K"
by (unfold field_def field_axioms_def, simp)
from 4 h1 h4 have 5: "((inv⇘K⇙ a) ⊗⇘K⇙a) = 𝟭⇘K⇙"
by (intro Units_l_inv, auto)
from 5 have 6: "(inv⇘K⇙ a )⊙⇘V⇙(a ⊙⇘V⇙ v) = v"
proof -
from h1 h2 h4 have 7: "(inv⇘K⇙ a )⊙⇘V⇙(a ⊙⇘V⇙ v) =(inv⇘K⇙ a ⊗⇘K⇙a) ⊙⇘V⇙ v" by (auto simp add: smult_assoc1)
from 5 h2 have 8: "(inv⇘K⇙ a ⊗⇘K⇙a) ⊙⇘V⇙ v = v" by auto
from 7 8 show ?thesis by auto
qed
from 2 6 show ?thesis by auto
qed
text ‹If $w\in S$ and $\sum_{w\in S} a_ww=0$, we have $v=\sum_{w\not\in S}a_v^{-1}a_ww$›
lemma (in vectorspace) lincomb_isolate:
fixes A v
assumes h1: "finite A" and h2: "A⊆carrier V" and h3: "a∈A→carrier K" and h4: "v∈A"
and h5: "a v ≠ 𝟬⇘K⇙" and h6: "lincomb a A=𝟬⇘V⇙"
shows "v=lincomb (λw. ⊖⇘K⇙(inv⇘K⇙ (a v)) ⊗⇘K⇙ a w) (A-{v})" and "v∈ span (A-{v})"
proof -
from h1 h2 h3 h4 have 1: "lincomb a A = ((a v) ⊙⇘V⇙ v) ⊕⇘V⇙ lincomb a (A-{v})"
by (rule lincomb_del2)
from 1 have 2: "𝟬⇘V⇙= ((a v) ⊙⇘V⇙ v) ⊕⇘V⇙ lincomb a (A-{v})" by (simp add: h6)
from h1 h2 h3 have 5: "lincomb a (A-{v}) ∈carrier V" by auto
from 2 h1 h2 h3 h4 have 3: " ⊖⇘V⇙ lincomb a (A-{v}) = ((a v) ⊙⇘V⇙ v)"
by (auto intro!: M.minus_equality)
have 6: "v = (⊖⇘K⇙ (inv⇘K⇙ (a v))) ⊙⇘V⇙ lincomb a (A-{v})"
proof -
from h2 h3 h4 h5 3 have 7: "v = inv⇘K⇙ (a v) ⊙⇘V⇙ (⊖⇘V⇙ lincomb a (A-{v}))"
by (intro mult_inverse, auto)
from assms have 8: "inv⇘K⇙ (a v)∈carrier K" by auto
from assms 5 8 have 9: "inv⇘K⇙ (a v) ⊙⇘V⇙ (⊖⇘V⇙ lincomb a (A-{v}))
= (⊖⇘K⇙ (inv⇘K⇙ (a v))) ⊙⇘V⇙ lincomb a (A-{v})"
by (simp add: smult_assoc_simp smult_minus_1_back r_minus)
from 7 9 show ?thesis by auto
qed
from h1 have 10: "finite (A-{v})" by auto
from assms have 11 : "(⊖⇘K⇙ (inv⇘K⇙ (a v)))∈ carrier K" by auto
from assms have 12: "lincomb (λw. ⊖⇘K⇙(inv⇘K⇙ (a v)) ⊗⇘K⇙ a w) (A-{v}) =
(⊖⇘K⇙ (inv⇘K⇙ (a v))) ⊙⇘V⇙ lincomb a (A-{v})"
by (intro lincomb_smult, auto)
from 6 12 show "v=lincomb (λw. ⊖⇘K⇙(inv⇘K⇙ (a v)) ⊗⇘K⇙ a w) (A-{v})" by auto
with assms show "v∈ span (A-{v})"
unfolding span_def
by (force simp add: 11 ring_subset_carrier)
qed
text ‹The map $(S\to K)\mapsto V$ given by $(a_v)_{v\in S}\mapsto \sum_{v\in S} a_v v$ is linear.›
lemma (in vectorspace) lincomb_is_linear:
fixes S
assumes h: "finite S" and h2: "S⊆carrier V"
shows "linear_map K (func_space S) V (λa. lincomb a S)"
proof -
have 0: "vectorspace K V"..
from h h2 have 1: "mod_hom K (func_space S) V (λa. lincomb a S)" by (rule lincomb_is_mod_hom)
from 0 1 show ?thesis by (unfold vectorspace_def mod_hom_def linear_map_def, auto)
qed
subsection ‹Basic facts about span and linear independence›
text ‹If $S$ is linearly independent, then $v\in \text{span}S$ iff $S\cup \{v\}$ is linearly
dependent.›
theorem (in vectorspace) lin_dep_iff_in_span:
fixes A v S
assumes h1: "S ⊆ carrier V" and h2: "lin_indpt S" and h3: "v∈ carrier V" and h4: "v∉S"
shows "v∈ span S ⟷ lin_dep (S ∪ {v})"
proof -
let ?T = "S ∪ {v}"
have 0: "v∈?T " by auto
from h1 h3 have h1_1: "?T ⊆ carrier V" by auto
have a1:"lin_dep ?T ⟹ v∈ span S"
proof -
assume a11: "lin_dep ?T"
from a11 obtain a w A where a: "(finite A ∧ A⊆?T ∧ (a∈ (A→carrier K)) ∧ (lincomb a A = 𝟬⇘V⇙) ∧ (w∈A) ∧ (a w≠ 𝟬⇘K⇙))"
by (metis lin_dep_def)
from assms a have nz2: "∃v∈A-S. a v≠𝟬⇘K⇙"
by (intro lincomb_must_include[where ?v="w" and ?T="S∪{v}"], auto)
from a nz2 have singleton: "{v}=A-S" by auto
from singleton nz2 have nz3: "a v≠𝟬⇘K⇙" by auto
let ?b="(λw. ⊖⇘K⇙ (inv⇘K⇙ (a v)) ⊗⇘K⇙ (a w))"
from singleton have Ains: "(A∩S) = A-{v}" by auto
from assms a singleton nz3 have a31: "v= lincomb ?b (A∩S)"
apply (subst Ains)
by (intro lincomb_isolate(1), auto)
from a a31 nz3 singleton show ?thesis
apply (unfold span_def, auto)
apply (rule_tac x="?b" in exI)
apply (rule_tac x="A∩S" in exI)
by (auto intro!: m_closed)
qed
have a2: "v∈ (span S) ⟹ lin_dep ?T"
proof -
assume inspan: "v∈ (span S)"
from inspan obtain a A where a: "A⊆S ∧ finite A ∧ (v = lincomb a A)∧ a∈A→carrier K" by (simp add: span_def, auto)
let ?b = "λ w. if (w=v) then (⊖⇘K⇙ 𝟭⇘K⇙) else a w"
have lc0: " lincomb ?b (A∪{v})=𝟬⇘V⇙"
proof -
from assms a have lc_ins: "lincomb ?b (A∪{v}) = ((?b v) ⊙⇘V⇙ v) ⊕⇘V⇙ lincomb ?b A"
by (intro lincomb_insert, auto)
from assms a have lc_elim: "lincomb ?b A=lincomb a A" by (intro lincomb_elim_if, auto)
from assms lc_ins lc_elim a show ?thesis by (simp add: M.l_neg smult_minus_1)
qed
from a lc0 show ?thesis
apply (unfold lin_dep_def)
apply (rule_tac x="A∪{v}" in exI)
apply (rule_tac x="?b" in exI)
apply (rule_tac x="v" in exI)
by auto
qed
from a1 a2 show ?thesis by auto
qed
text ‹If $v\in \text{span} A$ then $\text{span}A =\text{span}(A\cup \{v\})$›
lemma (in vectorspace) already_in_span:
fixes v A
assumes inC: "A⊆carrier V" and inspan: "v∈span A"
shows "span A= span (A∪{v})"
proof -
from inC inspan have dir1: "span A ⊆ span (A∪{v})" by (intro span_is_monotone, auto)
from inC have inown: "A⊆span A" by (rule in_own_span)
from inC have subm: "submodule K (span A) V" by (rule span_is_submodule)
from inown inspan subm have dir2: "span (A ∪ {v}) ⊆ span A" by (intro span_is_subset, auto)
from dir1 dir2 show ?thesis by auto
qed
subsection ‹The Replacement Theorem›
text ‹If $A,B\subseteq V$ are finite, $A$ is linearly independent, $B$ generates $W$,
and $A\subseteq W$, then there exists $C\subseteq V$ disjoint from $A$ such that
$\text{span}(A\cup C) = W$ and $|C|\le |B|-|A|$. In other words, we can complete
any linearly independent set to a generating set of $W$ by adding at most $|B|-|A|$ more elements.›
theorem (in vectorspace) replacement:
fixes A B
assumes h1: "finite A"
and h2: "finite B"
and h3: "B⊆carrier V"
and h4: "lin_indpt A"
and h5: "A⊆span B"
shows "∃C. finite C ∧ C⊆carrier V ∧ C⊆span B ∧ C∩A={} ∧ int (card C) ≤ (int (card B)) - (int (card A)) ∧ (span (A ∪ C) = span B)"
(is "∃C. ?P A B C")
using h1 h2 h3 h4 h5
proof (induct "card A" arbitrary: A B)
case 0
from "0.prems"(1) "0.hyps" have a0: "A={}" by auto
from "0.prems"(3) have a3: "B⊆span B" by (rule in_own_span)
from a0 a3 "0.prems" show ?case by (rule_tac x="B" in exI, auto)
next
case (Suc m)
let ?W="span B"
from Suc.prems(3) have BinC: "span B⊆carrier V" by (rule span_is_subset2)
from Suc.prems Suc.hyps BinC have A: "finite A" "lin_indpt A" "A⊆span B" "Suc m = card A" "A⊆carrier V"
by auto
from Suc.prems have B: "finite B" "B⊆carrier V" by auto
from Suc.hyps(2) obtain v where v: "v∈A" by fastforce
let ?A'="A-{v}"
from A(2) have liA': "lin_indpt ?A'"
apply (intro subset_li_is_li[of "A" "?A'"])
by auto
from v liA' Suc.prems Suc.hyps(2) have "∃C'. ?P ?A' B C'"
apply (intro Suc.hyps(1))
by auto
from this obtain C' where C': "?P ?A' B C'" by auto
show ?case
proof (cases "v∈ C'")
case True
have vinC': "v∈C'" by fact
from vinC' v have seteq: "A - {v} ∪ C' = A ∪ (C' - {v})" by auto
from C' seteq have spaneq: "span (A ∪ (C' - {v})) = span (B)" by algebra
from Suc.prems Suc.hyps C' vinC' v spaneq show ?thesis
apply (rule_tac x="C'-{v}" in exI)
apply (subgoal_tac "card C' >0")
by auto
next
case False
have f: "v∉C'" by fact
from A v C' have "∃a. a∈(?A'∪C')→carrier K ∧ lincomb a (?A' ∪ C') =v"
by (intro finite_in_span, auto)
from this obtain a where a: "a∈(?A'∪C')→carrier K ∧ v= lincomb a (?A' ∪ C')" by metis
let ?b="(λ w. if (w=v) then ⊖⇘K⇙𝟭⇘K⇙ else a w)"
from a have b: "?b∈A∪C'→carrier K" by auto
from v have rewrite_ins: "A∪C'=(?A'∪C')∪{v}" by auto
from f have "v∉?A'∪C'" by auto
from this A C' v a f have lcb: "lincomb ?b (A ∪ C') = 𝟬⇘V⇙"
apply (subst rewrite_ins)
apply (subst lincomb_insert)
apply (simp_all add: ring_subset_carrier coeff_in_ring)
apply (auto split: if_split_asm)
apply (subst lincomb_elim_if)
by (auto simp add: smult_minus_1 l_neg ring_subset_carrier)
from C' f have rewrite_minus: "C'=(A∪C')-A" by auto
from A C' b lcb v have exw: "∃w∈ C'. ?b w≠𝟬⇘K⇙"
apply (subst rewrite_minus)
apply (intro lincomb_must_include[where ?T="A∪C'" and ?v="v"])
by auto
from exw obtain w where w: "w∈ C'" "?b w≠𝟬⇘K⇙" by auto
from A C' w f b lcb have w_in: "w∈span ((A∪ C') -{w})"
apply (intro lincomb_isolate[where a="?b"])
by auto
have spaneq2: "span (A∪(C'-{w})) = span B"
proof -
have 1: "span (?A'∪C') = span (A∪ C')"
proof -
from A C' v have m1: "span (?A'∪C') = span ((?A'∪ C')∪{v})"
apply (intro already_in_span)
by auto
from f m1 show ?thesis by (metis rewrite_ins)
qed
have 2: "span (A∪ (C'-{w})) = span (A∪ C')"
proof -
from C' w(1) f have b60: "A∪ (C'-{w}) = (A∪ C') -{w}" by auto
from w(1) have b61: "A∪ C'= (A∪ C' -{w})∪{w}" by auto
from A C' w_in show ?thesis
apply (subst b61)
apply (subst b60)
apply (intro already_in_span)
by auto
qed
from C' 1 2 show ?thesis by auto
qed
from A C' w f v spaneq2 show ?thesis
apply (rule_tac x="C'-{w}" in exI)
apply (subgoal_tac "card C' >0")
by auto
qed
qed
subsection ‹Defining dimension and bases.›
text ‹Finite dimensional is defined as having a finite generating set.›
definition (in vectorspace) fin_dim:: "bool"
where "fin_dim = (∃ A. ((finite A) ∧ (A ⊆ carrier V) ∧ (gen_set A)))"
text ‹The dimension is the size of the smallest generating set. For equivalent
characterizations see below.›
definition (in vectorspace) dim:: "nat"
where "dim = (LEAST n. (∃ A. ((finite A) ∧ (card A = n) ∧ (A ⊆ carrier V) ∧ (gen_set A))))"
text ‹A ‹basis› is a linearly independent generating set.›
definition (in vectorspace) basis:: "'c set ⇒ bool"
where "basis A = ((lin_indpt A) ∧ (gen_set A)∧ (A⊆carrier V))"
text ‹From the replacement theorem, any linearly independent set is smaller than any generating set.›
lemma (in vectorspace) li_smaller_than_gen:
fixes A B
assumes h1: "finite A" and h2: "finite B" and h3: "A⊆carrier V" and h4: "B⊆carrier V"
and h5: "lin_indpt A" and h6: "gen_set B"
shows "card A ≤ card B"
proof -
from h3 h6 have 1: "A⊆span B" by auto
from h1 h2 h4 h5 1 obtain C where
2: "finite C ∧ C⊆carrier V ∧ C⊆span B ∧ C∩A={} ∧ int (card C) ≤ int (card B) - int (card A) ∧ (span (A ∪ C) = span B)"
by (metis replacement)
from 2 show ?thesis by arith
qed
text ‹The dimension is the cardinality of any basis. (In particular, all bases are the same size.)›
lemma (in vectorspace) dim_basis:
fixes A
assumes fin: "finite A" and h2: "basis A"
shows "dim = card A"
proof -
have 0: "⋀B m. ((finite B) ∧ (card B = m) ∧ (B ⊆ carrier V) ∧ (gen_set B)) ⟹ card A ≤ m"
proof -
fix B m
assume 1: "((finite B) ∧ (card B = m) ∧ (B ⊆ carrier V) ∧ (gen_set B))"
from 1 fin h2 have 2: "card A ≤ card B"
apply (unfold basis_def)
apply (intro li_smaller_than_gen)
by auto
from 1 2 show "?thesis B m" by auto
qed
from fin h2 0 show ?thesis
apply (unfold dim_def basis_def)
apply (intro Least_equality)
apply (rule_tac x="A" in exI)
by auto
qed
text ‹A ‹maximal› set with respect to $P$ is such that if $B\supseteq A$ and $P$ is also
satisfied for $B$, then $B=A$.›
definition maximal::"'a set ⇒ ('a set ⇒ bool) ⇒ bool"
where "maximal A P = ((P A) ∧ (∀B. B⊇A ∧ P B ⟶ B = A))"
text ‹A ‹minimal› set with respect to $P$ is such that if $B\subseteq A$ and $P$ is also
satisfied for $B$, then $B=A$.›
definition minimal::"'a set ⇒ ('a set ⇒ bool) ⇒ bool"
where "minimal A P = ((P A) ∧ (∀B. B⊆A ∧ P B ⟶ B = A))"
text ‹A maximal linearly independent set is a generating set.›
lemma (in vectorspace) max_li_is_gen:
fixes A
assumes h1: "maximal A (λS. S⊆carrier V ∧ lin_indpt S)"
shows "gen_set A"
proof (rule ccontr)
assume 0: "¬(gen_set A)"
from h1 have 1: " A⊆ carrier V ∧ lin_indpt A" by (unfold maximal_def, auto)
from 1 have 2: "span A ⊆ carrier V" by (intro span_is_subset2, auto)
from 0 1 2 have 3: "∃v. v∈carrier V ∧ v ∉ (span A)"
by auto
from 3 obtain v where 4: "v∈carrier V ∧ v ∉ (span A)" by auto
have 5: "v∉A"
proof -
from h1 1 have 51: "A⊆span A" apply (intro in_own_span) by auto
from 4 51 show ?thesis by auto
qed
from lin_dep_iff_in_span have 6: "⋀S v. S ⊆ carrier V∧ lin_indpt S ∧ v∈ carrier V ∧ v∉S
∧ v∉ span S ⟹ (lin_indpt (S ∪ {v}))" by auto
from 1 4 5 have 7: "lin_indpt (A ∪ {v})" apply (intro 6) by auto
have 9: "¬(maximal A (λS. S⊆carrier V ∧ lin_indpt S))"
proof -
from 1 4 5 7 have 8: "(∃B. A ⊆ B ∧ B ⊆ carrier V ∧ lin_indpt B ∧ B ≠ A)"
apply (rule_tac x="A∪{v}" in exI)
by auto
from 8 show ?thesis
apply (unfold maximal_def)
by simp
qed
from h1 9 show False by auto
qed
text ‹A minimal generating set is linearly independent.›
lemma (in vectorspace) min_gen_is_li:
fixes A
assumes h1: "minimal A (λS. S⊆carrier V ∧ gen_set S)"
shows "lin_indpt A"
proof (rule ccontr)
assume 0: "¬lin_indpt A"
from h1 have 1: " A⊆ carrier V ∧ gen_set A" by (unfold minimal_def, auto)
from 1 have 2: "span A = carrier V" by auto
from 0 1 obtain a v A' where
3: "finite A' ∧ A'⊆A ∧ a ∈ A' → carrier K ∧ LinearCombinations.module.lincomb V a A' = 𝟬⇘V⇙ ∧ v ∈ A' ∧ a v ≠ 𝟬⇘K⇙"
by (unfold lin_dep_def, auto)
have 4: "gen_set (A-{v})"
proof -
from 1 3 have 5: "v∈span (A'-{v})"
apply (intro lincomb_isolate[where a="a" and v="v"])
by auto
from 3 5 have 51: "v∈span (A-{v})"
apply (intro subsetD[where ?A="span (A'-{v})" and ?B="span (A-{v})" and ?c="v"])
by (intro span_is_monotone, auto)
from 1 have 6: "A⊆span A" apply (intro in_own_span) by auto
from 1 51 have 7: "span (A-{v}) = span ((A-{v})∪{v})" apply (intro already_in_span) by auto
from 3 have 8: "A = ((A-{v})∪{v})" by auto
from 2 7 8 have 9:"span (A-{v}) = carrier V" by auto
from 9 show ?thesis by auto
qed
have 10: "¬(minimal A (λS. S⊆carrier V ∧ gen_set S))"
proof -
from 1 3 4 have 11: "(∃B. A ⊇ B ∧ B ⊆ carrier V ∧ gen_set B ∧ B ≠ A)"
apply (rule_tac x="A-{v}" in exI)
by auto
from 11 show ?thesis
apply (unfold minimal_def)
by auto
qed
from h1 10 show False by auto
qed
text ‹Given that some finite set satisfies $P$, there is a minimal set that satisfies $P$.›
lemma minimal_exists:
fixes A P
assumes h1: "finite A" and h2: "P A"
shows "∃B. B⊆A ∧ minimal B P"
using h1 h2
proof (induct "card A" arbitrary: A rule: less_induct)
case (less A)
show ?case
proof (cases "card A = 0")
case True
from True less.hyps less.prems show ?thesis
apply (rule_tac x="{}" in exI)
apply (unfold minimal_def)
by auto
next
case False
show ?thesis
proof (cases "minimal A P")
case True
then show ?thesis
apply (rule_tac x="A" in exI)
by auto
next
case False
have 2: "¬minimal A P" by fact
from less.prems 2 have 3: "∃B. P B ∧ B ⊆ A ∧ B≠A"
apply (unfold minimal_def)
by auto
from 3 obtain B where 4: "P B ∧ B ⊂ A ∧ B≠A" by auto
from 4 have 5: "card B < card A" by (metis less.prems(1) psubset_card_mono)
from less.hyps less.prems 3 4 5 have 6: "∃C⊆B. minimal C P"
apply (intro less.hyps)
apply auto
by (metis rev_finite_subset)
from 6 obtain C where 7: "C⊆B ∧ minimal C P" by auto
from 4 7 show ?thesis
apply (rule_tac x="C" in exI)
apply (unfold minimal_def)
by auto
qed
qed
qed
text ‹If $V$ is finite-dimensional, then any linearly independent set is finite.›
lemma (in vectorspace) fin_dim_li_fin:
assumes fd: "fin_dim" and li: "lin_indpt A" and inC: "A⊆carrier V"
shows fin: "finite A"
proof (rule ccontr)
assume A: "¬finite A"
from fd obtain C where C: "finite C ∧ C⊆carrier V ∧ gen_set C" by (unfold fin_dim_def, auto)
from A obtain B where B: "B⊆A∧ finite B ∧ card B = card C + 1"
by (metis infinite_arbitrarily_large)
from B li have liB: "lin_indpt B"
by (intro subset_li_is_li[where ?A="A" and ?B="B"], auto)
from B C liB inC have "card B ≤ card C" by (intro li_smaller_than_gen, auto)
from this B show False by auto
qed
text ‹If $V$ is finite-dimensional (has a finite generating set), then a finite basis exists.›
lemma (in vectorspace) finite_basis_exists:
assumes h1: "fin_dim"
shows "∃β. finite β ∧ basis β"
proof -
from h1 obtain A where 1: "finite A ∧ A⊆carrier V ∧ gen_set A" by (metis fin_dim_def)
hence 2: "∃β. β⊆A ∧ minimal β (λS. S⊆carrier V ∧ gen_set S)"
apply (intro minimal_exists)
by auto
then obtain β where 3: "β⊆A ∧ minimal β (λS. S⊆carrier V ∧ gen_set S)" by auto
hence 4: "lin_indpt β" apply (intro min_gen_is_li) by auto
moreover from 3 have 5: "gen_set β ∧ β⊆carrier V" apply (unfold minimal_def) by auto
moreover from 1 3 have 6: "finite β" by (auto simp add: finite_subset)
ultimately show ?thesis apply (unfold basis_def) by auto
qed
text‹
The proof is as follows.
\begin{enumerate}
\item Because $V$ is finite-dimensional, there is a finite generating set
(we took this as our definition of finite-dimensional).
\item Hence, there is a minimal $\beta \subseteq A$ such that $\beta$ generates $V$.
\item $\beta$ is linearly independent because a minimal generating set is linearly independent.
\end{enumerate}
Finally, $\beta$ is a basis because it is both generating and linearly independent.
›
text ‹Any linearly independent set has cardinality at most equal to the dimension.›
lemma (in vectorspace) li_le_dim:
fixes A
assumes fd: "fin_dim" and c: "A⊆carrier V" and l: "lin_indpt A"
shows "finite A" "card A ≤ dim"
proof -
from fd c l show fa: "finite A" by (intro fin_dim_li_fin, auto)
from fd obtain β where 1: "finite β ∧ basis β"
by (metis finite_basis_exists)
from assms fa 1 have 2: "card A ≤ card β"
apply (intro li_smaller_than_gen, auto)
by (unfold basis_def, auto)
from assms 1 have 3: "dim = card β" by (intro dim_basis, auto)
from 2 3 show "card A ≤ dim" by auto
qed
text ‹Any generating set has cardinality at least equal to the dimension.›
lemma (in vectorspace) gen_ge_dim:
fixes A
assumes fa: "finite A" and c: "A⊆carrier V" and l: "gen_set A"
shows "card A ≥ dim"
proof -
from assms have fd: "fin_dim" by (unfold fin_dim_def, auto)
from fd obtain β where 1: "finite β ∧ basis β" by (metis finite_basis_exists)
from assms 1 have 2: "card A ≥ card β"
apply (intro li_smaller_than_gen, auto)
by (unfold basis_def, auto)
from assms 1 have 3: "dim = card β" by (intro dim_basis, auto)
from 2 3 show ?thesis by auto
qed
text ‹If there is an upper bound on the cardinality of sets satisfying $P$, then there is a maximal
set satisfying $P$.›
lemma maximal_exists:
fixes P B N
assumes maxc: "⋀A. P A ⟹ finite A ∧ (card A ≤N)" and b: "P B"
shows "∃A. finite A ∧ maximal A P"
proof -
let ?S="{card A| A. P A}"
let ?n="Max ?S"
from maxc have 1:"finite ?S"
apply (simp add: finite_nat_set_iff_bounded_le) by auto
from 1 have 2: "?n∈?S"
by (metis (mono_tags, lifting) Collect_empty_eq Max_in b)
from assms 2 have 3: "∃A. P A ∧ finite A ∧ card A = ?n"
by auto
from 3 obtain A where 4: "P A ∧ finite A ∧ card A = ?n" by auto
from 1 maxc have 5: "⋀A. P A ⟹ finite A ∧ (card A ≤?n)"
by (metis (mono_tags, lifting) Max.coboundedI mem_Collect_eq)
from 4 5 have 6: "maximal A P"
apply (unfold maximal_def)
by (metis card_seteq)
from 4 6 show ?thesis by auto
qed
text ‹Any maximal linearly independent set is a basis.›
lemma (in vectorspace) max_li_is_basis:
fixes A
assumes h1: "maximal A (λS. S⊆carrier V ∧ lin_indpt S)"
shows "basis A"
proof -
from h1 have 1: "gen_set A" by (rule max_li_is_gen)
from assms 1 show ?thesis by (unfold basis_def maximal_def, auto)
qed
text ‹Any minimal linearly independent set is a generating set.›
lemma (in vectorspace) min_gen_is_basis:
fixes A
assumes h1: "minimal A (λS. S⊆carrier V ∧ gen_set S)"
shows "basis A"
proof -
from h1 have 1: "lin_indpt A" by (rule min_gen_is_li)
from assms 1 show ?thesis by (unfold basis_def minimal_def, auto)
qed
text ‹Any linearly independent set with cardinality at least the dimension is a basis.›
lemma (in vectorspace) dim_li_is_basis:
fixes A
assumes fd: "fin_dim" and fa: "finite A" and ca: "A⊆carrier V" and li: "lin_indpt A"
and d: "card A ≥ dim"
shows "basis A"
proof -
from fd have 0: "⋀S. S⊆carrier V ∧ lin_indpt S ⟹ finite S ∧ card S ≤dim"
by (auto intro: li_le_dim)
from 0 assms have h1: "finite A ∧ maximal A (λS. S⊆carrier V ∧ lin_indpt S)"
apply (unfold maximal_def)
apply auto
by (metis card_seteq eq_iff)
from h1 show ?thesis by (auto intro: max_li_is_basis)
qed
text ‹Any generating set with cardinality at most the dimension is a basis.›
lemma (in vectorspace) dim_gen_is_basis:
fixes A
assumes fa: "finite A" and ca: "A⊆carrier V" and li: "gen_set A"
and d: "card A ≤ dim"
shows "basis A"
proof -
have 0: "⋀S. finite S∧ S⊆carrier V ∧ gen_set S ⟹ card S ≥dim"
by (intro gen_ge_dim, auto)
from 0 assms have h1: "minimal A (λS. finite S ∧ S⊆carrier V ∧ gen_set S)"
apply (unfold minimal_def)
apply auto
by (metis card_seteq eq_iff)
from h1 have h: "⋀B. B ⊆ A ∧ B ⊆ carrier V ∧ LinearCombinations.module.gen_set K V B ⟹ B = A"
proof -
fix B
assume asm: "B ⊆ A ∧ B ⊆ carrier V ∧ LinearCombinations.module.gen_set K V B"
from asm h1 have "finite B"
apply (unfold minimal_def)
apply (intro finite_subset[where ?A="B" and ?B="A"])
by auto
from h1 asm this show "?thesis B" apply (unfold minimal_def) by simp
qed
from h1 h have h2: "minimal A (λS. S⊆carrier V ∧ gen_set S)"
apply (unfold minimal_def)
by presburger
from h2 show ?thesis by (rule min_gen_is_basis)
qed
text ‹$\beta$ is a basis iff for all $v\in V$, there exists a unique $(a_v)_{v\in S}$ such that
$\sum_{v\in S} a_v v=v$.›
lemma (in vectorspace) basis_criterion:
assumes A_fin: "finite A" and AinC: "A⊆carrier V"
shows "basis A ⟷ (∀v. v∈ carrier V ⟶(∃! a. a∈A →⇩E carrier K ∧ lincomb a A = v))"
proof -
have 1: "¬(∀v. v∈ carrier V ⟶(∃! a. a∈A →⇩E carrier K ∧ lincomb a A = v)) ⟹ ¬basis A"
proof -
assume "¬(∀v. v∈ carrier V ⟶(∃! a. a∈A →⇩E carrier K ∧ lincomb a A = v))"
then obtain v where v: "v∈ carrier V ∧ ¬(∃! a. a∈A →⇩E carrier K ∧ lincomb a A = v)" by metis
from v have vinC: "v∈carrier V" by auto
from v have "¬(∃ a. a∈A →⇩E carrier K ∧ lincomb a A = v) ∨ (∃ a b.
a∈A →⇩E carrier K ∧ lincomb a A = v ∧ b∈A →⇩E carrier K ∧ lincomb b A = v
∧ a≠b)" by metis
then show ?thesis
proof
assume a: "¬(∃ a. a∈A →⇩E carrier K ∧ lincomb a A = v)"
from A_fin AinC have "⋀a. a∈A → carrier K ⟹ lincomb a A = lincomb (restrict a A) A"
unfolding lincomb_def restrict_def
by (simp cong: finsum_cong add: ring_subset_carrier coeff_in_ring)
with a have "¬(∃ a. a∈A → carrier K ∧ lincomb a A = v)" by auto
with A_fin AinC have "v∉span A"
using finite_in_span by blast
with AinC v show "¬(basis A)" by (unfold basis_def, auto)
next
assume a2: "(∃ a b.
a∈A →⇩E carrier K ∧ lincomb a A = v ∧ b∈A →⇩E carrier K ∧ lincomb b A = v
∧ a≠b)"
then obtain a b where ab: "a∈A →⇩E carrier K ∧ lincomb a A = v ∧ b∈A →⇩E carrier K ∧ lincomb b A = v
∧ a≠b" by metis
from ab obtain w where w: "w∈A ∧ a w ≠ b w" apply (unfold PiE_def, auto)
by (metis extensionalityI)
let ?c="λ x. (if x∈A then ((a x) ⊖⇘K⇙ (b x)) else undefined)"
from ab have a_fun: "a∈A → carrier K"
and b_fun: "b∈A → carrier K"
by (unfold PiE_def, auto)
from w a_fun b_fun have abinC: "a w ∈carrier K" "b w ∈carrier K" by auto
from abinC w have nz: "a w ⊖⇘K⇙ b w ≠ 𝟬⇘K⇙"
by auto
from A_fin AinC a_fun b_fun ab vinC have a_b:
"LinearCombinations.module.lincomb V (λx. if x ∈ A then a x ⊖⇘K⇙ b x else undefined) A = 𝟬⇘V⇙"
by (simp cong: lincomb_cong add: coeff_in_ring lincomb_diff)
from A_fin AinC ab w v nz a_b have "lin_dep A"
apply (intro lin_dep_crit[where ?A="A" and ?a="?c" and ?v="w"])
apply (auto simp add: PiE_def)
by auto
thus "¬basis A" by (unfold basis_def, auto)
qed
qed
have 2: "(∀v. v∈ carrier V ⟶(∃! a. a∈A →⇩E carrier K ∧ lincomb a A = v)) ⟹ basis A"
proof -
assume b1: "(∀v. v∈ carrier V ⟶(∃! a. a∈A →⇩E carrier K ∧ lincomb a A = v))"
(is "(∀v. v∈ carrier V ⟶(∃! a. ?Q a v))")
from b1 have b2: "(∀v. v∈ carrier V ⟶(∃ a. a∈A → carrier K ∧ lincomb a A = v))"
apply (unfold PiE_def)
by blast
from A_fin AinC b2 have "gen_set A"
apply (unfold span_def)
by blast
from b1 have A_li: "lin_indpt A"
proof -
let ?z="λ x. (if (x∈A) then 𝟬⇘K⇙ else undefined)"
from A_fin AinC have zero: "?Q ?z 𝟬⇘V⇙"
by (unfold PiE_def extensional_def lincomb_def, auto simp add: ring_subset_carrier)
from A_fin AinC show ?thesis
proof (rule finite_lin_indpt2)
fix a
assume a_fun: "a ∈ A → carrier K" and
lc_a: "LinearCombinations.module.lincomb V a A = 𝟬⇘V⇙"
from a_fun have a_res: "restrict a A ∈ A →⇩E carrier K" by auto
from a_fun A_fin AinC lc_a have
lc_a_res: "LinearCombinations.module.lincomb V (restrict a A) A = 𝟬⇘V⇙"
apply (unfold lincomb_def restrict_def)
by (simp cong: finsum_cong2 add: coeff_in_ring ring_subset_carrier)
from a_fun a_res lc_a_res zero b1 have "restrict a A = ?z" by auto
from this show "∀v∈A. a v = 𝟬⇘K⇙"
apply (unfold restrict_def)
by meson
qed
qed
have A_gen: "gen_set A"
proof -
from AinC have dir1: "span A⊆carrier V" by (rule span_is_subset2)
have dir2: "carrier V⊆span A"
proof (auto)
fix v
assume v: "v∈carrier V"
from v b2 obtain a where "a∈A → carrier K ∧ lincomb a A = v" by auto
from this A_fin AinC show "v∈span A" by (subst finite_span, auto)
qed
from dir1 dir2 show ?thesis by auto
qed
from A_li A_gen AinC show "basis A" by (unfold basis_def, auto)
qed
from 1 2 show ?thesis by satx
qed
lemma (in linear_map) surj_imp_imT_carrier:
assumes surj: "T` (carrier V) = carrier W"
shows "(imT) = carrier W"
by (simp add: surj im_def)
subsection ‹The rank-nullity (dimension) theorem›
text ‹If $V$ is finite-dimensional and $T:V\to W$ is a linear map, then $\text{dim}(\text{im}(T))+
\text{dim}(\text{ker}(T)) = \text{dim} V$. Moreover, we prove that if $T$ is surjective
linear-map between $V$ and $W$, where $V$ is finite-dimensional, then also $W$ is finite-dimensional.›
theorem (in linear_map) rank_nullity_main:
assumes fd: "V.fin_dim"
shows "(vectorspace.dim K (W.vs imT)) + (vectorspace.dim K (V.vs kerT)) = V.dim"
"T ` (carrier V) = carrier W ⟹ W.fin_dim"
proof -
have subs_ker: "subspace K kerT V" by (intro kerT_is_subspace)
from subs_ker have vs_ker: "vectorspace K (V.vs kerT)" by (rule V.subspace_is_vs)
from vs_ker interpret ker: vectorspace K "(V.vs kerT)" by auto
have kerInC: "kerT⊆carrier V" by (unfold ker_def, auto)
have subs_im: "subspace K imT W" by (intro imT_is_subspace)
from subs_im have vs_im: "vectorspace K (W.vs imT)" by (rule W.subspace_is_vs)
from vs_im interpret im: vectorspace K "(W.vs imT)" by auto
have imInC: "imT⊆carrier W" by (unfold im_def, auto)
have zero_same[simp]: "𝟬⇘V.vs kerT⇙ = 𝟬⇘V⇙" apply (unfold ker_def) by auto
have every_li_small: "⋀A. (A ⊆ kerT)∧ ker.lin_indpt A ⟹
finite A ∧ card A ≤ V.dim"
proof -
fix A
assume eli_asm: "(A ⊆ kerT)∧ ker.lin_indpt A"
note V.module.span_li_not_depend(2)[where ?N="kerT" and ?S="A"]
from this subs_ker fd eli_asm kerInC show "?thesis A"
apply (intro conjI)
by (auto intro!: V.li_le_dim)
qed
from every_li_small have exA:
"∃A. finite A ∧ maximal A (λS. S⊆carrier (V.vs kerT) ∧ ker.lin_indpt S)"
apply (intro maximal_exists[where ?N="V.dim" and ?B="{}"])
apply auto
by (unfold ker.lin_dep_def, auto)
from exA obtain A where A:" finite A ∧ maximal A (λS. S⊆carrier (V.vs kerT) ∧ ker.lin_indpt S)"
by blast
hence finA: "finite A" and Ainker: "A⊆carrier (V.vs kerT)" and AinC: "A⊆carrier V"
by (unfold maximal_def ker_def, auto)
from A have Abasis: "ker.basis A"
by (intro ker.max_li_is_basis, auto)
from subs_ker Abasis have spanA: "V.module.span A = kerT"
apply (unfold ker.basis_def)
by (subst sym[OF V.module.span_li_not_depend(1)[where ?N="kerT"]], auto)
from Abasis have Akerli: "ker.lin_indpt A"
apply (unfold ker.basis_def)
by auto
from subs_ker Ainker Akerli have Ali: "V.module.lin_indpt A"
by (auto simp add: V.module.span_li_not_depend(2))
txt‹Use the replacement theorem to find C such that $A\cup C$ is a basis of V.›
from fd obtain B where B: "finite B∧ V.basis B" by (metis V.finite_basis_exists)
from B have Bfin: "finite B" and Bbasis:"V.basis B" by auto
from B have Bcard: "V.dim = card B" by (intro V.dim_basis, auto)
from Bbasis have 62: "V.module.span B = carrier V"
by (unfold V.basis_def, auto)
from A Abasis Ali B vs_ker have "∃C. finite C ∧ C⊆carrier V ∧ C⊆ V.module.span B ∧ C∩A={}
∧ int (card C) ≤ (int (card B)) - (int (card A)) ∧ (V.module.span (A ∪ C) = V.module.span B)"
apply (intro V.replacement)
apply (unfold vectorspace.basis_def V.basis_def)
by (unfold ker_def, auto)
txt ‹From replacement we got $|C|\leq |B|-|A|$. Equality must actually hold, because no generating set
can be smaller than $B$. Now $A\cup C$ is a maximal generating set, hence a basis; its cardinality
equals the dimension.›
txt ‹We claim that $T(C)$ is basis for $\text{im}(T)$.›
then obtain C where C: "finite C ∧ C⊆carrier V ∧ C⊆ V.module.span B ∧ C∩A={}
∧ int (card C) ≤ (int (card B)) - (int (card A)) ∧ (V.module.span (A ∪ C) = V.module.span B)" by auto
hence Cfin: "finite C" and CinC: "C⊆carrier V" and CinspanB: " C⊆V.module.span B" and CAdis: "C∩A={}"
and Ccard: "int (card C) ≤ (int (card B)) - (int (card A))"
and ACspanB: "(V.module.span (A ∪ C) = V.module.span B)" by auto
from C have cardLe: "card A + card C ≤ card B" by auto
from B C have ACgen: "V.module.gen_set (A∪C)" apply (unfold V.basis_def) by auto
from finA C ACgen AinC B have cardGe: "card (A∪C) ≥ card B" by (intro V.li_smaller_than_gen, unfold V.basis_def, auto)
from finA C have cardUn: "card (A∪C)≤ card A + card C"
by (metis Int_commute card_Un_disjoint le_refl)
from cardLe cardUn cardGe Bcard have cardEq:
"card (A∪C) = card A + card C"
"card (A∪C) = card B"
"card (A∪C) = V.dim"
by auto
from Abasis C cardEq have disj: "A∩C={}" by auto
from finA AinC C cardEq 62 have ACfin: "finite (A∪C)" and ACbasis: "V.basis (A∪C)"
by (auto intro!: V.dim_gen_is_basis)
have lm: "linear_map K V W T"..
txt ‹Let $C'$ be the image of $C$ under $T$. We will show $C'$ is a basis for $\text{im}(T)$.›
let ?C' = "T`C"
from Cfin have C'fin: "finite ?C'" by auto
from AinC C have cim: "?C'⊆imT" by (unfold im_def, auto)
txt ‹"There is a subtle detail: we first have to show $T$ is injective on $C$.›
txt ‹We establish that no nontrivial linear combination of $C$ can have image 0 under $T$,
because that would mean it is a linear combination of $A$, giving that $A\cup C$ is linearly dependent,
contradiction. We use this result in 2 ways: (1) if $T$ is not injective on $C$, then we obtain $v$, $w\in C$
such that $v-w$ is in the kernel, contradiction, (2) if $T(C)$ is linearly dependent,
taking the inverse image of that linear combination gives a linear combination of $C$ in the kernel,
contradiction. Hence $T$ is injective on $C$ and $T(C)$ is linearly independent.›
have lc_in_ker: "⋀d D v. ⟦D⊆C; d∈D→carrier K; T (V.module.lincomb d D) = 𝟬⇘W⇙;
v∈D; d v ≠𝟬⇘K⇙⟧⟹False"
proof -
fix d D v
assume D: "D⊆C" and d: "d∈D→carrier K" and T0: "T (V.module.lincomb d D) = 𝟬⇘W⇙"
and v: "v∈D" and dvnz: "d v ≠𝟬⇘K⇙"
from D Cfin have Dfin: "finite D" by (auto intro: finite_subset)
from D CinC have DinC: "D⊆carrier V" by auto
from T0 d Dfin DinC have lc_d: "V.module.lincomb d D∈kerT"
by (unfold ker_def, auto)
from lc_d spanA AinC have "∃a' A'. A'⊆A ∧ a'∈A'→carrier K ∧
V.module.lincomb a' A'= V.module.lincomb d D"
by (intro V.module.in_span, auto)
then obtain a' A' where a': "A'⊆A ∧ a'∈A'→carrier K ∧
V.module.lincomb d D = V.module.lincomb a' A'"
by metis
hence A'sub: "A'⊆A" and a'fun: "a'∈A'→carrier K"
and a'_lc:"V.module.lincomb d D = V.module.lincomb a' A'" by auto
from a' finA Dfin have A'fin: "finite (A')" by (auto intro: finite_subset)
from AinC A'sub have A'inC: "A'⊆carrier V" by auto
let ?e = "(λv. if v ∈ A' then a' v else ⊖⇘K⇙𝟭⇘K⇙⊗⇘K⇙ d v)"
from a'fun d have e_fun: "?e ∈ A' ∪ D → carrier K"
apply (unfold Pi_def)
by auto
from
A'fin Dfin
A'inC DinC
a'fun d e_fun
disj D A'sub
have lccomp1:
"V.module.lincomb a' A' ⊕⇘V⇙ ⊖⇘K⇙𝟭⇘K⇙⊙⇘V⇙ V.module.lincomb d D =
V.module.lincomb (λv. if v∈A' then a' v else ⊖⇘K⇙𝟭⇘K⇙⊗⇘K⇙ d v) (A'∪D)"
apply (subst sym[OF V.module.lincomb_smult])
apply (simp_all)
apply (subst V.module.lincomb_union2)
by (auto)
from
A'fin
A'inC
a'fun
have lccomp2:
"V.module.lincomb a' A' ⊕⇘V⇙ ⊖⇘K⇙𝟭⇘K⇙⊙⇘V⇙ V.module.lincomb d D =
𝟬⇘V⇙"
by (simp add: a'_lc
V.module.smult_minus_1 V.module.M.r_neg)
from lccomp1 lccomp2 have lc0: "V.module.lincomb (λv. if v∈A' then a' v else ⊖⇘K⇙𝟭⇘K⇙⊗⇘K⇙ d v) (A'∪D)
=𝟬⇘V⇙" by auto
from disj a' v D have v_nin: "v∉A'" by auto
from A'fin Dfin
A'inC DinC
e_fun d
A'sub D disj
v dvnz
lc0
have AC_ld: "V.module.lin_dep (A∪C)"
apply (intro V.module.lin_dep_crit[where ?A="A'∪D" and
?S="A∪C" and ?a="λv. if v∈A' then a' v else ⊖⇘K⇙𝟭⇘K⇙⊗⇘K⇙ d v" and ?v="v"])
by (auto dest: integral)
from AC_ld ACbasis show False by (unfold V.basis_def, auto)
qed
have C'_card: "inj_on T C" "card C = card ?C'"
proof -
show "inj_on T C"
proof (rule ccontr)
assume "¬inj_on T C"
then obtain v w where "v∈C" "w∈C" "v≠w" "T v = T w" by (unfold inj_on_def, auto)
from this CinC show False
apply (intro lc_in_ker[where ?D1="{v,w}" and ?d1="λx. if x=v then 𝟭⇘K⇙ else ⊖⇘K⇙𝟭⇘K⇙"
and ?v1="v"])
by (auto simp add: V.module.lincomb_def hom_sum ring_subset_carrier
W.module.smult_minus_1 r_neg T_im)
qed
from this Cfin show "card C = card ?C'"
by (metis card_image)
qed
let ?f="the_inv_into C T"
have f: "⋀x. x∈C ⟹ ?f (T x) = x" "⋀y. y∈?C' ⟹ T (?f y) = y"
apply (insert C'_card(1))
apply (metis the_inv_into_f_f)
by (metis f_the_inv_into_f)
have C'_li: "im.lin_indpt ?C'"
proof (rule ccontr)
assume Cld: "¬im.lin_indpt ?C'"
from Cld cim subs_im have CldW: "W.module.lin_dep ?C'"
apply (subst sym[OF W.module.span_li_not_depend(2)[where ?S="T`C" and ?N="imT"]])
by auto
from C CldW have "∃c' v'. (c'∈ (?C'→carrier K)) ∧ (W.module.lincomb c' ?C' = 𝟬⇘W⇙)
∧ (v'∈?C') ∧ (c' v'≠ 𝟬⇘K⇙)" by (intro W.module.finite_lin_dep, auto)
then obtain c' v' where c': "(c'∈ (?C'→carrier K)) ∧ (W.module.lincomb c' ?C' = 𝟬⇘W⇙)
∧ (v'∈?C') ∧ (c' v'≠ 𝟬⇘K⇙)" by auto
hence c'fun: "(c'∈ (?C'→carrier K))" and c'lc: "(W.module.lincomb c' ?C' = 𝟬⇘W⇙)" and
v':"(v'∈?C')" and cvnz: "(c' v'≠ 𝟬⇘K⇙)" by auto
txt ‹We take the inverse image of $C'$ under $T$ to get a linear combination of $C$ that is
in the kernel and hence a linear combination of $A$. This contradicts $A\cup C$ being linearly
independent.›
let ?c="λv. c' (T v)"
from c'fun have c_fun: "?c∈ C→carrier K" by auto
from Cfin
c_fun c'fun
C'_card
CinC
f
c'lc
have "T (V.module.lincomb ?c C) = 𝟬⇘W⇙"
apply (unfold V.module.lincomb_def W.module.lincomb_def)
apply (subst hom_sum, auto)
apply (simp cong: finsum_cong add: ring_subset_carrier coeff_in_ring)
apply (subst finsum_reindex[where ?f="λw. c' w ⊙⇘W⇙ w" and ?h="T" and ?A="C", THEN sym])
by auto
with f c'fun cvnz v' show False
by (intro lc_in_ker[where ?D1="C" and ?d1="?c" and ?v1="?f v'"], auto)
qed
have C'_gen: "im.gen_set ?C'"
proof -
have C'_span: "span ?C' = imT"
proof (rule equalityI)
from cim subs_im show "W.module.span ?C' ⊆ imT"
by (intro span_is_subset, unfold subspace_def, auto)
next
show "imT⊆W.module.span ?C'"
proof (auto)
fix w
assume w: "w∈imT"
from this finA Cfin AinC CinC obtain v where v_inC: "v∈carrier V" and w_eq_T_v: "w= T v"
by (unfold im_def image_def, auto)
from finA Cfin AinC CinC v_inC ACgen have "∃a. a ∈ A∪C → carrier K∧ V.module.lincomb a (A∪C) = v"
by (intro V.module.finite_in_span, auto)
then obtain a where
a_fun: "a ∈ A∪C → carrier K" and
lc_a_v: "v= V.module.lincomb a (A∪C)"
by auto
let ?a'="λv. a (?f v)"
from finA Cfin AinC CinC a_fun disj Ainker f C'_card have Tv: "T v = W.module.lincomb ?a' ?C'"
apply (subst lc_a_v)
apply (subst V.module.lincomb_union, simp_all)
apply (unfold lincomb_def V.module.lincomb_def)
apply (subst hom_sum, auto)
apply (simp add: subsetD coeff_in_ring
hom_sum
T_ker
)
apply (subst finsum_reindex[where ?h="T" and ?f="λv. ?a' v⊙⇘W⇙ v"], auto)
by (auto cong: finsum_cong simp add: coeff_in_ring ring_subset_carrier)
from a_fun f have a'_fun: "?a'∈?C' → carrier K" by auto
from C'fin CinC this w_eq_T_v a'_fun Tv show "w ∈ LinearCombinations.module.span K W (T ` C)"
by (subst finite_span, auto)
qed
qed
from this subs_im CinC show ?thesis
apply (subst span_li_not_depend(1))
by (unfold im_def subspace_def, auto)
qed
from C'_li C'_gen C cim have C'_basis: "im.basis (T`C)"
by (unfold im.basis_def, auto)
have C_card_im: "card C = (vectorspace.dim K (W.vs imT))"
using C'_basis C'_card(2) C'fin im.dim_basis by auto
from finA Abasis have "ker.dim = card A" by (rule ker.dim_basis)
note * = this C_card_im cardEq
show "(vectorspace.dim K (W.vs imT)) + (vectorspace.dim K (V.vs kerT)) = V.dim" using * by auto
assume "T` (carrier V) = carrier W"
from * surj_imp_imT_carrier[OF this]
show "W.fin_dim" using C'_basis C'fin unfolding W.fin_dim_def im.basis_def by auto
qed
theorem (in linear_map) rank_nullity:
assumes fd: "V.fin_dim"
shows "(vectorspace.dim K (W.vs imT)) + (vectorspace.dim K (V.vs kerT)) = V.dim"
by (rule rank_nullity_main[OF fd])
end