Theory Free_Module
section ‹Generators, independence, bases and free modules›
theory Free_Module
imports Module_Basics
begin
text ‹Over a ring the two halves of ``basis'' come apart. A spanning set need not be linearly
independent, a linearly independent set need not span, and --- unlike the vector-space case --- a
linearly independent spanning set is genuinely stronger than either. So ‹spanning› and
‹lin_indep› are defined separately, and a module is ∗‹free› when it has a basis, meaning a
set that is both.
∗‹These definitions are stated for arbitrary --- possibly infinite --- subsets.› Finiteness is
not part of either concept; it enters only through the finite index sets inside ‹lincomb› and
‹span›. This matters because ‹madd.fincomp› returns the unit on an infinite index set
(‹fincomp_infinite›), so a definition that applied ‹lincomb› directly to an
infinite set would silently be talking about the zero of the module rather than about an
infinite sum.
Quantifying over finite subsets, as ‹lin_indep› does, avoids that trap; guarding the
definition with ‹finite› would merely hide it.
‹Vector_Space› defines its own finite-dimensional ‹basis› as bijectivity of the coordinate map,
which is the right packaging for the cardinality count there but presumes finiteness. The
bridging lemmas relating the two live in that theory, with ‹finite› as an explicit hypothesis
where it does real work rather than baked into the concept.
The uniqueness-of-coordinates theorem ‹lin_indep_lincomb_unique› below is the reason linear
independence is worth isolating: it is what makes a free module the right domain for defining a
homomorphism by prescribing values on a basis.›
context Module
begin
subsection ‹Coefficient functions›
text ‹A ∗‹coefficient function on ‹B›› assigns a ring element to each element of @{term B}. We do
not require extensionality: the linear combination @{term "lincomb c B"} only ever inspects
@{term c} on @{term B}, so two coefficient functions agreeing on @{term B} give the same
combination (‹lincomb_cong› below).›
definition coeffs_on :: "('b ⇒ 'a) ⇒ 'b set ⇒ bool"
where "coeffs_on c B ⟷ (∀v ∈ B. c v ∈ R)"
lemma coeffs_onI: "(⋀v. v ∈ B ⟹ c v ∈ R) ⟹ coeffs_on c B"
by (simp add: coeffs_on_def)
lemma coeffs_onD: "⟦ coeffs_on c B; v ∈ B ⟧ ⟹ c v ∈ R"
by (simp add: coeffs_on_def)
lemma coeffs_on_subset: "⟦ coeffs_on c B; A ⊆ B ⟧ ⟹ coeffs_on c A"
by (auto simp: coeffs_on_def)
text ‹The zero coefficient function.›
abbreviation zero_coeffs :: "'b ⇒ 'a"
where "zero_coeffs ≡ (λ_. 𝟬)"
lemma coeffs_on_zero [simp, intro]: "coeffs_on zero_coeffs B"
by (simp add: coeffs_on_def)
text ‹A linear combination depends on the coefficients only through their values on the index set.›
lemma lincomb_cong:
assumes B: "B ⊆ M" and eq: "⋀v. v ∈ B ⟹ c v = d v" and d: "coeffs_on d B"
shows "lincomb c B = lincomb d B"
unfolding lincomb_def
proof (rule madd.fincomp_cong')
show "B = B" ..
show "(λv. d v ⊙ v) ∈ B → M" using B d by (auto intro: scale_closed coeffs_onD)
show "⋀v. v ∈ B ⟹ c v ⊙ v = d v ⊙ v" using eq by simp
qed
text ‹The zero combination. Every term is @{term "𝟬 ⊙ v = 𝟬⇩M"}.›
lemma lincomb_zero_coeffs [simp]:
assumes B: "B ⊆ M" shows "lincomb zero_coeffs B = 𝟬⇩M"
unfolding lincomb_def
using B by (auto intro!: madd.fincomp_unit_eqI scale_zero_scalar)
text ‹Scaling distributes over a finite module sum. Proved by induction on the index set; kept as
a named lemma because inline it is slow enough to hit the proof timeout.›
lemma scale_fincomp:
assumes a: "a ∈ R" and f: "f ∈ A → M"
shows "a ⊙ madd.fincomp f A = madd.fincomp (λv. a ⊙ f v) A"
using f
proof (induct A rule: infinite_finite_induct)
case (infinite A) then show ?case using a by (simp add: scale_zero_elem)
next
case empty then show ?case using a by (simp add: scale_zero_elem)
next
case (insert v A)
then have fv: "f v ∈ M" and fA: "f ∈ A → M" by auto
have sc: "(λu. a ⊙ f u) ∈ A → M" using a fA by (auto intro: scale_closed)
have "a ⊙ madd.fincomp f (insert v A) = a ⊙ (f v ⊕ madd.fincomp f A)"
using insert fv fA by simp
also have "… = (a ⊙ f v) ⊕ (a ⊙ madd.fincomp f A)"
using a fv fA by (auto intro!: scale_distrib_madd madd.fincomp_closed)
also have "… = (a ⊙ f v) ⊕ madd.fincomp (λu. a ⊙ f u) A"
using insert fA by simp
also have "… = madd.fincomp (λu. a ⊙ f u) (insert v A)"
using insert a fv sc by (auto intro!: madd.fincomp_insert[symmetric] scale_closed)
finally show ?case .
qed
text ‹Enlarging the index set by elements whose coefficient is @{term 𝟬} does not change the
combination: the extra terms are all @{term "𝟬 ⊙ v = 𝟬⇩M"}. This is what lets two combinations
over different finite index sets be added on their union.›
lemma lincomb_mono_zero:
assumes B: "finite B" and AB: "A ⊆ B" and BM: "B ⊆ M"
and zero: "⋀v. v ∈ B - A ⟹ c v = 𝟬" and c: "coeffs_on c B"
shows "lincomb c A = lincomb c B"
unfolding lincomb_def
proof (rule madd.fincomp_mono_neutral_cong_left)
show "finite B" and "A ⊆ B" using B AB by simp_all
show "⋀v. v ∈ B - A ⟹ c v ⊙ v = 𝟬⇩M"
using zero BM by (auto simp: scale_zero_scalar)
show "⋀v. v ∈ A ⟹ c v ⊙ v = c v ⊙ v" by simp
show "(λv. c v ⊙ v) ∈ B → M"
using BM c by (auto intro!: scale_closed intro: coeffs_onD)
qed
subsection ‹Membership in the span›
text ‹Introduction and elimination for @{const span}, in the form the proofs below want.›
lemma spanI:
assumes "finite A" and "A ⊆ S" and "coeffs_on c A" and "x = lincomb c A"
shows "x ∈ span S"
using assms unfolding span_def coeffs_on_def by blast
lemma spanE:
assumes "x ∈ span S"
obtains c A where "finite A" "A ⊆ S" "coeffs_on c A" "x = lincomb c A"
using assms unfolding span_def coeffs_on_def by blast
text ‹A combination over a singleton is just the scaling. Kept separate: unfolding
@{const lincomb} to @{const madd.fincomp} inline makes the simplifier work far harder than it
needs to (it timed out at 12s in an earlier draft).›
lemma lincomb_singleton [simp]:
assumes v: "v ∈ M" and c: "c v ∈ R"
shows "lincomb c {v} = c v ⊙ v"
unfolding lincomb_def using v c by (simp add: scale_closed)
text ‹Each element of a set lies in its span: take the singleton combination with coefficient
@{term 𝟭}.›
lemma span_incl:
assumes S: "S ⊆ M" shows "S ⊆ span S"
proof
fix v assume v: "v ∈ S"
then have vM: "v ∈ M" using S by blast
have "lincomb (λ_. 𝟭) {v} = 𝟭 ⊙ v" using vM by simp
also have "… = v" using vM by (rule scale_one)
finally have "v = lincomb (λ_. 𝟭) {v}" ..
then show "v ∈ span S" using v by (auto intro!: spanI[where A = "{v}"] coeffs_onI)
qed
text ‹Adding coefficient functions pointwise adds the combinations. Both the span-closure proof
and the uniqueness proof need this; factored out so each does the @{const madd.fincomp}
manipulation once.›
lemma lincomb_add_coeffs:
assumes AM: "A ⊆ M" and c: "coeffs_on c A" and d: "coeffs_on d A"
shows "lincomb (λv. c v + d v) A = lincomb c A ⊕ lincomb d A"
unfolding lincomb_def
proof (rule trans)
show "madd.fincomp (λv. (c v + d v) ⊙ v) A
= madd.fincomp (λv. (c v ⊙ v) ⊕ (d v ⊙ v)) A"
using AM c d
by (intro madd.fincomp_cong')
(auto intro!: scale_distrib_add scale_closed madd_closed intro: coeffs_onD)
show "madd.fincomp (λv. (c v ⊙ v) ⊕ (d v ⊙ v)) A
= madd.fincomp (λv. c v ⊙ v) A ⊕ madd.fincomp (λv. d v ⊙ v) A"
using AM c d
by (intro madd.fincomp_comp) (auto intro!: scale_closed intro: coeffs_onD)
qed
text ‹The span is a submodule. Closure under addition merges two finite index sets; closure under
scaling multiplies through the coefficients.›
lemma span_zero [simp, intro]: "𝟬⇩M ∈ span S"
by (rule spanI[where A = "{}" and c = zero_coeffs]) auto
lemma span_madd_closed:
assumes S: "S ⊆ M" and x: "x ∈ span S" and y: "y ∈ span S"
shows "x ⊕ y ∈ span S"
proof -
from x obtain c A where A: "finite A" "A ⊆ S" "coeffs_on c A" "x = lincomb c A"
by (rule spanE)
from y obtain d B where B: "finite B" "B ⊆ S" "coeffs_on d B" "y = lincomb d B"
by (rule spanE)
define c' where "c' = (λv. if v ∈ A then c v else 𝟬)"
define d' where "d' = (λv. if v ∈ B then d v else 𝟬)"
have UM: "A ∪ B ⊆ M" using A(2) B(2) S by blast
have finU: "finite (A ∪ B)" using A(1) B(1) by simp
have c'R: "coeffs_on c' (A ∪ B)"
proof (rule coeffs_onI)
fix v assume "v ∈ A ∪ B"
show "c' v ∈ R" unfolding c'_def using coeffs_onD[OF A(3)] by simp
qed
have d'R: "coeffs_on d' (A ∪ B)"
proof (rule coeffs_onI)
fix v assume "v ∈ A ∪ B"
show "d' v ∈ R" unfolding d'_def using coeffs_onD[OF B(3)] by simp
qed
have cA: "lincomb c' (A ∪ B) = lincomb c A"
proof -
have "lincomb c' A = lincomb c' (A ∪ B)"
proof (rule lincomb_mono_zero[OF finU Un_upper1 UM])
show "⋀v. v ∈ A ∪ B - A ⟹ c' v = 𝟬" unfolding c'_def by simp
show "coeffs_on c' (A ∪ B)" by (rule c'R)
qed
moreover have "lincomb c' A = lincomb c A"
proof (rule lincomb_cong)
show "A ⊆ M" using A(2) S by blast
show "⋀v. v ∈ A ⟹ c' v = c v" unfolding c'_def by simp
show "coeffs_on c A" by (rule A(3))
qed
ultimately show ?thesis by simp
qed
have dB: "lincomb d' (A ∪ B) = lincomb d B"
proof -
have "lincomb d' B = lincomb d' (A ∪ B)"
proof (rule lincomb_mono_zero[OF finU Un_upper2 UM])
show "⋀v. v ∈ A ∪ B - B ⟹ d' v = 𝟬" unfolding d'_def by simp
show "coeffs_on d' (A ∪ B)" by (rule d'R)
qed
moreover have "lincomb d' B = lincomb d B"
proof (rule lincomb_cong)
show "B ⊆ M" using B(2) S by blast
show "⋀v. v ∈ B ⟹ d' v = d v" unfolding d'_def by simp
show "coeffs_on d B" by (rule B(3))
qed
ultimately show ?thesis by simp
qed
have sum: "lincomb (λv. c' v + d' v) (A ∪ B) = x ⊕ y"
using lincomb_add_coeffs[OF UM c'R d'R] cA dB A(4) B(4) by simp
have sumR: "coeffs_on (λv. c' v + d' v) (A ∪ B)"
by (rule coeffs_onI) (use coeffs_onD[OF c'R] coeffs_onD[OF d'R] in simp)
show ?thesis
by (rule spanI[OF finU _ sumR sum[symmetric]]) (use A(2) B(2) in blast)
qed
lemma span_scale_closed:
assumes S: "S ⊆ M" and a: "a ∈ R" and x: "x ∈ span S"
shows "a ⊙ x ∈ span S"
proof -
from x obtain c A where A: "finite A" "A ⊆ S" "coeffs_on c A" "x = lincomb c A"
by (rule spanE)
have AM: "A ⊆ M" using A(2) S by blast
have pi: "(λv. c v ⊙ v) ∈ A → M"
using AM A(3) by (auto intro!: scale_closed intro: coeffs_onD)
have "a ⊙ lincomb c A = lincomb (λv. a ⋅ c v) A"
unfolding lincomb_def
proof (rule trans)
show "a ⊙ madd.fincomp (λv. c v ⊙ v) A = madd.fincomp (λv. a ⊙ (c v ⊙ v)) A"
using a pi by (rule scale_fincomp)
show "madd.fincomp (λv. a ⊙ (c v ⊙ v)) A = madd.fincomp (λv. (a ⋅ c v) ⊙ v) A"
proof (rule madd.fincomp_cong')
show "A = A" ..
show "(λv. (a ⋅ c v) ⊙ v) ∈ A → M"
using AM a coeffs_onD[OF A(3)] by (auto intro!: scale_closed)
fix v assume v: "v ∈ A"
then have vM: "v ∈ M" and cv: "c v ∈ R" using AM coeffs_onD[OF A(3)] by auto
show "a ⊙ (c v ⊙ v) = (a ⋅ c v) ⊙ v" by (rule scale_scale[OF a cv vM, symmetric])
qed
qed
moreover have "coeffs_on (λv. a ⋅ c v) A"
by (rule coeffs_onI) (use a coeffs_onD[OF A(3)] in simp)
ultimately show ?thesis using A by (blast intro: spanI)
qed
theorem span_submodule:
assumes S: "S ⊆ M" shows "submodule (span S)"
proof (rule submoduleI)
show "span S ⊆ M" using S by (auto intro: span_closed)
show "𝟬⇩M ∈ span S" by simp
show "⋀u v. ⟦ u ∈ span S; v ∈ span S ⟧ ⟹ u ⊕ v ∈ span S"
using S by (rule span_madd_closed)
show "⋀a v. ⟦ a ∈ R; v ∈ span S ⟧ ⟹ a ⊙ v ∈ span S"
using S by (rule span_scale_closed)
qed
text ‹The span is the least submodule containing its generators. This elimination form
complements @{thm [source] span_submodule}: any submodule containing @{term S} contains every
finite linear combination of elements of @{term S}.›
theorem span_minimal:
assumes N: "submodule N" and SN: "S ⊆ N"
shows "span S ⊆ N"
proof
fix x assume "x ∈ span S"
then obtain c A where A: "finite A" "A ⊆ S" "coeffs_on c A" "x = lincomb c A"
by (rule spanE)
have lincomb_in_N: "lincomb c A ∈ N"
if "finite A" "A ⊆ N" "coeffs_on c A" for A c
using that
proof (induction A arbitrary: c rule: finite_induct)
case empty
then show ?case using submodule_zero[OF N] by simp
next
case (insert v A)
have vN: "v ∈ N" and AN: "A ⊆ N" using insert.prems by auto
have NM: "N ⊆ M" by (rule submodule_subset[OF N])
have vM: "v ∈ M" and AM: "A ⊆ M" using vN AN NM by auto
have cv: "c v ∈ R" by (rule coeffs_onD[OF insert.prems(2)]) simp
have cA: "coeffs_on c A" by (rule coeffs_on_subset[OF insert.prems(2)]) blast
have terms: "(λu. c u ⊙ u) ∈ A → M"
using AM cA by (auto intro!: scale_closed intro: coeffs_onD)
have eq: "lincomb c (insert v A) = (c v ⊙ v) ⊕ lincomb c A"
unfolding lincomb_def using insert.hyps terms cv vM by (simp add: scale_closed)
have term_N: "c v ⊙ v ∈ N" by (rule submodule_scale[OF N cv vN])
have rest_N: "lincomb c A ∈ N" by (rule insert.IH[OF AN cA])
have "(c v ⊙ v) ⊕ lincomb c A ∈ N"
by (rule submodule_add[OF N term_N rest_N])
then show ?case using eq by simp
qed
have "lincomb c A ∈ N"
by (rule lincomb_in_N[OF A(1) _ A(3)]) (use A(2) SN in blast)
then show "x ∈ N" using A(4) by simp
qed
subsection ‹Generating sets, independence, bases›
text ‹@{term S} ∗‹generates› the module when its span is everything.›
definition spanning :: "'b set ⇒ bool"
where "spanning S ⟷ S ⊆ M ∧ span S = M"
lemma spanningI: "⟦ S ⊆ M; ⋀v. v ∈ M ⟹ v ∈ span S ⟧ ⟹ spanning S"
unfolding spanning_def using span_closed by blast
lemma spanningD: "⟦ spanning S; v ∈ M ⟧ ⟹ v ∈ span S"
by (simp add: spanning_def)
text ‹The whole module generates itself.›
lemma spanning_whole: "spanning M"
by (rule spanningI) (auto intro: span_incl[THEN subsetD])
text ‹@{term S} is ∗‹linearly independent› when no non-trivial finite combination of ∗‹distinct› elements
vanishes: whenever a finite @{term "A ⊆ S"} has @{term "lincomb c A = 𝟬⇩M"}, all the coefficients
on @{term A} are @{term 𝟬}. Over a ring this is the right notion --- note it forbids torsion
among the generators, which is why not every module is free.›
definition lin_indep :: "'b set ⇒ bool"
where "lin_indep S ⟷ S ⊆ M ∧
(∀c A. finite A ⟶ A ⊆ S ⟶ coeffs_on c A ⟶ lincomb c A = 𝟬⇩M ⟶ (∀v ∈ A. c v = 𝟬))"
lemma lin_indepI:
"⟦ S ⊆ M;
⋀c A v. ⟦ finite A; A ⊆ S; coeffs_on c A; lincomb c A = 𝟬⇩M; v ∈ A ⟧ ⟹ c v = 𝟬 ⟧
⟹ lin_indep S"
unfolding lin_indep_def by blast
lemma lin_indepD:
"⟦ lin_indep S; finite A; A ⊆ S; coeffs_on c A; lincomb c A = 𝟬⇩M; v ∈ A ⟧ ⟹ c v = 𝟬"
unfolding lin_indep_def by blast
lemma lin_indep_subset: "⟦ lin_indep S; T ⊆ S ⟧ ⟹ lin_indep T"
unfolding lin_indep_def using subset_trans by blast
text ‹The empty set is linearly independent.›
lemma lin_indep_empty [simp, intro]: "lin_indep {}"
by (rule lin_indepI) auto
text ‹Independence rules out @{term "𝟬⇩M"} as a member --- the combination @{term "𝟭 ⊙ 𝟬⇩M"} vanishes
with coefficient @{term 𝟭} --- but ∗‹only over a non-trivial ring›. The hypothesis
@{term "𝟭 ≠ 𝟬"} is genuinely needed: @{locale Module} extends @{locale Ring}, which does not
assume it, and over the trivial ring @{term "𝟭 = 𝟬"} makes every coefficient zero, so
@{term "{𝟬⇩M}"} counts as ‹lin_indep›.›
lemma lin_indep_not_mzero:
assumes S: "lin_indep S" and nz: "𝟭 ≠ 𝟬" shows "𝟬⇩M ∉ S"
proof
assume z: "𝟬⇩M ∈ S"
have "lincomb (λ_. 𝟭) {𝟬⇩M} = 𝟭 ⊙ 𝟬⇩M" by simp
also have "… = 𝟬⇩M" by (rule scale_one) simp
finally have lc: "lincomb (λ_. 𝟭) {𝟬⇩M} = 𝟬⇩M" .
have "(λ_. 𝟭) 𝟬⇩M = 𝟬"
by (rule lin_indepD[OF S _ _ _ lc]) (use z in ‹auto intro!: coeffs_onI›)
then have "𝟭 = 𝟬" by simp
then show False using nz by simp
qed
text ‹A ∗‹basis› is a linearly independent spanning set; a module is ∗‹free› when it has one.›
definition module_basis :: "'b set ⇒ bool"
where "module_basis B ⟷ spanning B ∧ lin_indep B"
definition free :: bool
where "free ⟷ (∃B. module_basis B)"
lemma module_basisI: "⟦ spanning B; lin_indep B ⟧ ⟹ module_basis B"
by (simp add: module_basis_def)
lemma module_basis_spanning: "module_basis B ⟹ spanning B"
by (simp add: module_basis_def)
lemma module_basis_lin_indep: "module_basis B ⟹ lin_indep B"
by (simp add: module_basis_def)
lemma freeI: "module_basis B ⟹ free"
unfolding free_def by blast
text ‹The trivial module is free, on the empty basis: its only element @{term "𝟬⇩M"} is the empty
linear combination, which lies in @{term "span {}"}.›
lemma module_basis_empty_trivial:
assumes triv: "M = {𝟬⇩M}" shows "module_basis {}"
proof (rule module_basisI)
show "spanning {}"
proof (rule spanningI)
show "{} ⊆ M" by simp
fix v assume "v ∈ M"
then have "v = 𝟬⇩M" using triv by blast
then show "v ∈ span {}" by simp
qed
qed auto
lemma free_trivial:
assumes "M = {𝟬⇩M}" shows free
using module_basis_empty_trivial[OF assms] by (rule freeI)
subsection ‹Uniqueness of coordinates›
text ‹∗‹The point of independence.› Over a linearly independent set the coefficients of a linear
combination are determined by its value. Stated for a common finite index set @{term A}: if two
coefficient functions give the same combination, they agree on @{term A}.
The proof forms the difference of the two coefficient functions. Its combination is
@{term "𝟬⇩M"}, so independence forces every difference to vanish, hence
@{term "c v = d v"} by cancellation in the ring's additive group.›
theorem lin_indep_lincomb_unique:
assumes S: "lin_indep S" and A: "finite A" "A ⊆ S"
and c: "coeffs_on c A" and d: "coeffs_on d A"
and eq: "lincomb c A = lincomb d A"
and v: "v ∈ A"
shows "c v = d v"
proof -
have AM: "A ⊆ M" using A(2) S unfolding lin_indep_def by blast
define e where "e = (λu. c u + (- d u))"
have negd: "coeffs_on (λu. - d u) A"
by (rule coeffs_onI) (use coeffs_onD[OF d] in simp)
have eR: "coeffs_on e A"
unfolding e_def
by (rule coeffs_onI)
(use coeffs_onD[OF c] coeffs_onD[OF negd] in simp)
have "lincomb e A = lincomb c A ⊕ madd.inverse (lincomb d A)"
proof -
have "lincomb e A = lincomb c A ⊕ lincomb (λu. - d u) A"
unfolding e_def by (rule lincomb_add_coeffs[OF AM c negd])
also have "lincomb (λu. - d u) A = madd.inverse (lincomb d A)"
unfolding lincomb_def
proof (rule trans)
show "madd.fincomp (λu. (- d u) ⊙ u) A = madd.fincomp (λu. madd.inverse (d u ⊙ u)) A"
proof (rule madd.fincomp_cong')
show "A = A" ..
show "(λu. madd.inverse (d u ⊙ u)) ∈ A → M"
using AM coeffs_onD[OF d] by (auto intro!: scale_closed)
fix u assume u: "u ∈ A"
then have uM: "u ∈ M" and du: "d u ∈ R" using AM coeffs_onD[OF d] by auto
show "(- d u) ⊙ u = madd.inverse (d u ⊙ u)" by (rule scale_neg_scalar[OF du uM])
qed
show "madd.fincomp (λu. madd.inverse (d u ⊙ u)) A = madd.inverse (madd.fincomp (λu. d u ⊙ u) A)"
using AM d by (intro madd.fincomp_inverse) (auto intro!: scale_closed intro: coeffs_onD)
qed
finally show ?thesis .
qed
also have "… = 𝟬⇩M"
using eq lincomb_closed[OF AM] d c
by (simp add: madd.invertible_right_inverse coeffs_on_def)
finally have "lincomb e A = 𝟬⇩M" .
then have "e v = 𝟬" using S A eR v by (rule_tac lin_indepD) auto
then have cd: "c v + (- d v) = 𝟬" unfolding e_def .
have cvR: "c v ∈ R" and dvR: "d v ∈ R" using coeffs_onD[OF c v] coeffs_onD[OF d v] by simp_all
have ndvR: "- d v ∈ R" using dvR by simp
have "d v + (- d v) = 𝟬" using dvR by simp
with cd have eq2: "c v + (- d v) = d v + (- d v)" by simp
show "c v = d v"
by (rule additive.invertible_right_cancel
[OF additive.invertible[OF ndvR] ndvR cvR dvR, THEN iffD1, OF eq2])
qed
text ‹Consequently, for a basis every module element has ∗‹unique› coordinates on any finite
index set: existence from generation, uniqueness from independence.›
corollary module_basis_coords_unique:
assumes B: "module_basis B" and A: "finite A" "A ⊆ B"
and c: "coeffs_on c A" and d: "coeffs_on d A"
and eq: "lincomb c A = lincomb d A"
shows "∀v ∈ A. c v = d v"
using lin_indep_lincomb_unique[OF module_basis_lin_indep[OF B] A c d eq] by blast
subsection ‹Coordinates over a basis›
text ‹For the universal property below we need uniqueness across ∗‹different› index sets, not just a
common one: two representations of the same element, over possibly different finite subsets of an
independent set, must agree once each coefficient function is extended by @{term 𝟬} outside its own
index set. The proof pushes both representations onto the union of the two index sets --- which
changes neither combination, by @{thm [source] lincomb_mono_zero} --- and then applies
@{thm [source] lin_indep_lincomb_unique} there.›
theorem lin_indep_lincomb_unique_gen:
assumes S: "lin_indep S"
and A: "finite A" "A ⊆ S" and A': "finite A'" "A' ⊆ S"
and c: "coeffs_on c A" and d: "coeffs_on d A'"
and eq: "lincomb c A = lincomb d A'"
shows "(if v ∈ A then c v else 𝟬) = (if v ∈ A' then d v else 𝟬)"
proof -
have SM: "S ⊆ M" using S unfolding lin_indep_def by blast
have UM: "A ∪ A' ⊆ M" using A(2) A'(2) SM by blast
have finU: "finite (A ∪ A')" using A(1) A'(1) by simp
have US: "A ∪ A' ⊆ S" using A(2) A'(2) by blast
define c' where "c' = (λu. if u ∈ A then c u else 𝟬)"
define d' where "d' = (λu. if u ∈ A' then d u else 𝟬)"
have c'R: "coeffs_on c' (A ∪ A')"
by (rule coeffs_onI) (use coeffs_onD[OF c] in ‹simp add: c'_def›)
have d'R: "coeffs_on d' (A ∪ A')"
by (rule coeffs_onI) (use coeffs_onD[OF d] in ‹simp add: d'_def›)
have cU: "lincomb c' (A ∪ A') = lincomb c A"
proof -
have "lincomb c' A = lincomb c' (A ∪ A')"
proof (rule lincomb_mono_zero[OF finU Un_upper1 UM])
show "⋀u. u ∈ A ∪ A' - A ⟹ c' u = 𝟬" unfolding c'_def by simp
show "coeffs_on c' (A ∪ A')" by (rule c'R)
qed
moreover have "lincomb c' A = lincomb c A"
proof (rule lincomb_cong)
show "A ⊆ M" using A(2) SM by blast
show "⋀u. u ∈ A ⟹ c' u = c u" unfolding c'_def by simp
show "coeffs_on c A" by (rule c)
qed
ultimately show ?thesis by simp
qed
have dU: "lincomb d' (A ∪ A') = lincomb d A'"
proof -
have "lincomb d' A' = lincomb d' (A ∪ A')"
proof (rule lincomb_mono_zero[OF finU Un_upper2 UM])
show "⋀u. u ∈ A ∪ A' - A' ⟹ d' u = 𝟬" unfolding d'_def by simp
show "coeffs_on d' (A ∪ A')" by (rule d'R)
qed
moreover have "lincomb d' A' = lincomb d A'"
proof (rule lincomb_cong)
show "A' ⊆ M" using A'(2) SM by blast
show "⋀u. u ∈ A' ⟹ d' u = d u" unfolding d'_def by simp
show "coeffs_on d A'" by (rule d)
qed
ultimately show ?thesis by simp
qed
from eq cU dU have eqU: "lincomb c' (A ∪ A') = lincomb d' (A ∪ A')" by simp
show ?thesis
proof (cases "v ∈ A ∪ A'")
case True
then have "c' v = d' v"
by (rule lin_indep_lincomb_unique[OF S finU US c'R d'R eqU])
then show ?thesis unfolding c'_def d'_def .
next
case False
then show ?thesis by simp
qed
qed
text ‹Spans generated by disjoint parts of one independent set meet only at zero. The
generating sets themselves need not be finite: span membership supplies the two finite supports
on which uniqueness of coordinates is applied.›
theorem span_inter_eq_trivial:
assumes S: "lin_indep S" and AS: "A ⊆ S" and BS: "B ⊆ S"
and disjoint: "A ∩ B = {}"
shows "span A ∩ span B = {𝟬⇩M}"
proof
show "span A ∩ span B ⊆ {𝟬⇩M}"
proof
fix x assume x: "x ∈ span A ∩ span B"
have xA: "x ∈ span A" and xB: "x ∈ span B" using x by simp_all
from xA obtain c C where C: "finite C" "C ⊆ A" "coeffs_on c C"
"x = lincomb c C"
by (rule spanE)
from xB obtain d D where D: "finite D" "D ⊆ B" "coeffs_on d D"
"x = lincomb d D"
by (rule spanE)
have CS: "C ⊆ S" using C(2) AS by blast
have DS: "D ⊆ S" using D(2) BS by blast
have eq: "lincomb c C = lincomb d D" using C(4) D(4) by simp
have c_zero: "c v = 𝟬" if v: "v ∈ C" for v
proof -
have "v ∉ D" using v C(2) D(2) disjoint by blast
moreover have "(if v ∈ C then c v else 𝟬) =
(if v ∈ D then d v else 𝟬)"
by (rule lin_indep_lincomb_unique_gen[OF S C(1) CS D(1) DS C(3) D(3) eq])
ultimately show ?thesis using v by simp
qed
have CM: "C ⊆ M" using CS S unfolding lin_indep_def by blast
have "x = lincomb c C" by (rule C(4))
also have "… = lincomb zero_coeffs C"
by (rule lincomb_cong[OF CM c_zero coeffs_on_zero])
also have "… = 𝟬⇩M" using CM by simp
finally show "x ∈ {𝟬⇩M}" by simp
qed
show "{𝟬⇩M} ⊆ span A ∩ span B" by simp
qed
text ‹Every element of a module with a basis has a representation over some finite subset of it.›
lemma module_basis_repr_exists:
assumes B: "module_basis B" and x: "x ∈ M"
obtains A c where "finite A" "A ⊆ B" "coeffs_on c A" "x = lincomb c A"
proof -
have "x ∈ span B" by (rule spanningD[OF module_basis_spanning[OF B] x])
then show thesis using that by (rule spanE)
qed
text ‹And that representation is unique in the sense of
@{thm [source] lin_indep_lincomb_unique_gen}: the coefficients, extended by @{term 𝟬}, are
determined by the element.›
corollary module_basis_repr_unique:
assumes B: "module_basis B"
and A: "finite A" "A ⊆ B" and A': "finite A'" "A' ⊆ B"
and c: "coeffs_on c A" and d: "coeffs_on d A'"
and eq: "lincomb c A = lincomb d A'"
shows "(if v ∈ A then c v else 𝟬) = (if v ∈ A' then d v else 𝟬)"
by (rule lin_indep_lincomb_unique_gen
[OF module_basis_lin_indep[OF B] A A' c d eq])
end
end