Theory VectorSpace.LinearCombinations
section ‹Linear Combinations›
theory LinearCombinations
imports Main
"HOL-Algebra.Module"
"HOL-Algebra.Coset"
RingModuleFacts
MonoidSums
FunctionLemmas
begin
subsection ‹Lemmas for simplification›
text ‹The following are helpful in certain simplifications (esp. congruence rules). Warning: arbitrary
use leads to looping.›
lemma (in ring) coeff_in_ring:
"⟦a∈A→carrier R; x∈A⟧ ⟹ a x ∈carrier R"
by (rule Pi_mem)
lemma (in ring) coeff_in_ring2:
"⟦ x∈A;a∈A→carrier R⟧ ⟹ a x ∈carrier R"
by (metis Pi_mem)
lemma ring_subset_carrier:
"⟦x ∈A; A⊆carrier R⟧ ⟹ x ∈carrier R"
by auto
lemma disj_if:
"⟦A∩B={}; x∈ B⟧ ⟹ (if x∈A then f x else g x) = g x"
by auto
lemmas (in module) sum_simp = ring_subset_carrier
subsection ‹Linear combinations›
text ‹A linear combination is $\sum_{v\in A} a_v v$. $(a_v)_{v\in S}$ is a function
$A\to K$, where $A\subseteq K$.›
definition (in module) lincomb::"['c ⇒ 'a, 'c set]⇒ 'c"
where "lincomb a A = (⨁⇘M⇙ v∈A. (a v ⊙⇘M⇙ v))"
lemma (in module) summands_valid:
fixes A a
assumes h2: "A⊆ carrier M" and h3: "a∈(A→carrier R)"
shows "∀ v∈ A. (((a v) ⊙⇘M⇙ v)∈ carrier M)"
proof -
from assms show ?thesis by auto
qed
lemma (in module) lincomb_closed [simp, intro]:
fixes S a
assumes h2: "S⊆ carrier M" and h3: "a∈(S→carrier R)"
shows "lincomb a S ∈ carrier M"
proof -
from h2 h3 show ?thesis by (unfold lincomb_def, auto intro:finsum_closed)
qed
lemma (in comm_monoid) finprod_cong2:
"[| A = B;
!!i. i ∈ B ==> f i = g i; f ∈ B → carrier G|] ==>
finprod G f A = finprod G g B"
by (intro finprod_cong, auto)
lemmas (in abelian_monoid) finsum_cong2 = add.finprod_cong2
lemma (in module) lincomb_cong:
assumes h2: "A=B" and h3: "A ⊆ carrier M"
and h4: "⋀v. v∈A ⟹ a v = b v" and h5: "b∈ B→carrier R"
shows "lincomb a A = lincomb b B"
using assms
by (simp cong: finsum_cong2 add: lincomb_def summands_valid ring_subset_carrier)
lemma (in module) lincomb_union:
fixes a A B
assumes h1: "finite (A∪ B)" and h3: "A∪B ⊆ carrier M"
and h4: "A∩B={}" and h5: "a∈(A∪B→carrier R)"
shows "lincomb a (A∪B) = lincomb a A ⊕⇘M⇙ lincomb a B"
using assms
by (auto cong: finsum_cong2 simp add: lincomb_def finsum_Un_disjoint summands_valid ring_subset_carrier)
text ‹This is useful as a simp rule sometimes, for combining linear combinations.›
lemma (in module) lincomb_union2:
fixes a b A B
assumes h1: "finite (A∪ B)" and h3: "A∪B ⊆ carrier M"
and h4: "A∩B={}" and h5: "a∈A→carrier R" and h6: "b∈B→carrier R"
shows "lincomb a A ⊕⇘M⇙ lincomb b B = lincomb (λv. if (v∈A) then a v else b v) (A∪B)"
(is "lincomb a A ⊕⇘M⇙ lincomb b B = lincomb ?c (A∪B)")
using assms
by (auto cong: finsum_cong2
simp add: lincomb_def finsum_Un_disjoint summands_valid ring_subset_carrier disj_if)
lemma (in module) lincomb_del2:
fixes S a v
assumes h1: "finite S" and h2: "S⊆ carrier M" and h3: "a∈(S→carrier R)" and h4:"v∈S"
shows "lincomb a S = ((a v) ⊙⇘M⇙ v) ⊕⇘M⇙ lincomb a (S-{v})"
proof -
from h4 have 1: "S={v}∪(S-{v})" by (metis insert_Diff insert_is_Un)
from assms show ?thesis
apply (subst 1)
apply (subst lincomb_union, auto)
by (unfold lincomb_def, auto simp add: coeff_in_ring)
qed
lemma (in module) lincomb_insert:
fixes S a v
assumes h1: "finite S" and h2: "S⊆ carrier M" and h3: "a∈(S∪{v}→carrier R)" and h4:"v∉S" and
h5:"v∈ carrier M"
shows "lincomb a (S∪{v}) = ((a v) ⊙⇘M⇙ v) ⊕⇘M⇙ lincomb a S"
using assms
by (auto cong: finsum_cong2
simp add: lincomb_def finsum_Un_disjoint summands_valid ring_subset_carrier disj_if)
lemma (in module) lincomb_elim_if [simp]:
fixes b c S
assumes h1: "S ⊆ carrier M" and h2: "⋀v. v∈S⟹ ¬P v" and h3: "c∈S→carrier R"
shows "lincomb (λw. if P w then b w else c w) S = lincomb c S"
using assms
by (auto cong: finsum_cong2
simp add: lincomb_def finsum_Un_disjoint summands_valid ring_subset_carrier disj_if)
lemma (in module) lincomb_smult:
fixes A c
assumes h2: "A⊆carrier M" and h3: "a∈A→carrier R" and h4: "c∈carrier R"
shows "lincomb (λw. c⊗⇘R⇙ a w) A = c⊙⇘M⇙ (lincomb a A)"
using assms
by (auto cong: finsum_cong2
simp add: lincomb_def finsum_Un_disjoint finsum_smult ring_subset_carrier disj_if smult_assoc1 coeff_in_ring)
subsection ‹Linear dependence and independence.›
text ‹A set $S$ in a module/vectorspace is linearly dependent if there is a finite set $A \subseteq S$
and coefficients $(a_v)_{v\in A}$ such that $sum_{v\in A} a_vv=0$ and for some $v$, $a_v\neq 0$.›
definition (in module) lin_dep where
"lin_dep S = (∃A a v. (finite A ∧ A⊆S ∧ (a∈ (A→carrier R)) ∧ (lincomb a A = 𝟬⇘M⇙) ∧ (v∈A) ∧ (a v≠ 𝟬⇘R⇙)))"
abbreviation (in module) lin_indpt::"'c set ⇒ bool"
where "lin_indpt S ≡ ¬lin_dep S"
text ‹In the finite case, we can take $A=S$. This may be more convenient (e.g., when adding two
linear combinations.›
lemma (in module) finite_lin_dep:
fixes S
assumes finS:"finite S" and ld: "lin_dep S" and inC: "S⊆carrier M"
shows "∃a v. (a∈ (S→carrier R)) ∧ (lincomb a S = 𝟬⇘M⇙) ∧ (v∈S) ∧ (a v≠ 𝟬⇘R⇙)"
proof -
from ld obtain A a v where A: "(A⊆S ∧ (a∈ (A→carrier R)) ∧ (lincomb a A = 𝟬⇘M⇙) ∧ (v∈A) ∧ (a v≠ 𝟬⇘R⇙))"
by (unfold lin_dep_def, auto)
let ?b="λw. if w∈A then a w else 𝟬⇘R⇙"
from finS inC A have if_in: "(⨁⇘M⇙v∈S. (if v ∈ A then a v else 𝟬) ⊙⇘M⇙ v) = (⨁⇘M⇙v∈S. (if v ∈ A then a v ⊙⇘M⇙ v else 𝟬⇘M⇙))"
apply auto
apply (intro finsum_cong')
by (auto simp add: coeff_in_ring)
from finS inC A have b: "lincomb ?b S = 𝟬⇘M⇙"
apply (unfold lincomb_def)
apply (subst if_in)
by (subst extend_sum, auto)
from A b show ?thesis
apply (rule_tac x="?b" in exI)
apply (rule_tac x="v" in exI)
by auto
qed
text ‹Criteria of linear dependency in a easy format to apply: apply (rule lin-dep-crit)›
lemma (in module) lin_dep_crit:
fixes A S a v
assumes fin: "finite A" and subset: "A⊆S" and h1: "(a∈ (A→carrier R))" and h2: "v∈ A"
and h3:"a v≠ 𝟬⇘R⇙" and h4: "(lincomb a A = 𝟬⇘M⇙)"
shows "lin_dep S"
proof -
from assms show ?thesis
by (unfold lin_dep_def, auto)
qed
text ‹If $\sum_{v\in A} a_vv=0$ implies $a_v=0$ for all $v\in S$, then $A$ is linearly independent.›
lemma (in module) finite_lin_indpt2:
fixes A
assumes A_fin: "finite A" and AinC: "A⊆carrier M" and
lc0: "⋀a. a∈ (A→carrier R) ⟹ (lincomb a A = 𝟬⇘M⇙) ⟹ (∀ v∈A. a v= 𝟬⇘R⇙)"
shows "lin_indpt A"
proof (rule ccontr)
assume "¬lin_indpt A"
from A_fin AinC this obtain a v where av:
"(a∈ (A→carrier R)) ∧ (lincomb a A = 𝟬⇘M⇙) ∧ (v∈A) ∧ (a v≠ 𝟬⇘R⇙)"
by (metis finite_lin_dep)
from av lc0 show False by auto
qed
text ‹Any set containing 0 is linearly dependent.›
lemma (in module) zero_lin_dep:
assumes 0: "𝟬⇘M⇙ ∈ S" and nonzero: "carrier R ≠ {𝟬⇘R⇙}"
shows "lin_dep S"
proof -
from nonzero have zero_not_one: "𝟬⇘R⇙ ≠ 𝟭⇘R⇙" by (rule nontrivial_ring)
from 0 zero_not_one show ?thesis
apply (unfold lin_dep_def)
apply (rule_tac x="{𝟬⇘M⇙}" in exI)
apply (rule_tac x="(λv. 𝟭⇘R⇙)" in exI)
apply (rule_tac x="𝟬⇘M⇙" in exI)
by (unfold lincomb_def, auto)
qed
lemma (in module) zero_nin_lin_indpt:
assumes h2: "S⊆carrier M" and li: "¬(lin_dep S)" and nonzero: "carrier R ≠ {𝟬⇘R⇙}"
shows "𝟬⇘M⇙ ∉ S"
proof (rule ccontr)
assume a1: "¬(𝟬⇘M⇙ ∉ S)"
from a1 have a2: "𝟬⇘M⇙ ∈ S" by auto
from a2 nonzero have ld: "lin_dep S" by (rule zero_lin_dep)
from li ld show False by auto
qed
text ‹The ‹span› of $S$ is the set of linear combinations with $A \subseteq S$.›
definition (in module) span::"'c set ⇒'c set"
where "span S = {lincomb a A | a A. finite A ∧ A⊆S ∧ a∈ (A→carrier R)}"
text ‹The ‹span› interpreted as a module or vectorspace.›
abbreviation (in module) span_vs::"'c set ⇒ ('a,'c,'d) module_scheme"
where "span_vs S ≡ M ⦇carrier := span S⦈"
text ‹In the finite case, we can take $A=S$ without loss of generality.›
lemma (in module) finite_span:
assumes fin: "finite S" and inC: "S⊆carrier M"
shows "span S = {lincomb a S | a. a∈ (S→carrier R)}"
proof (rule equalityI)
{
fix A a
assume subset: "A ⊆ S" and a: "a ∈ A → carrier R"
let ?b="(λv. if v ∈ A then a v else 𝟬)"
from fin inC subset a have if_in: "(⨁⇘M⇙v∈S. ?b v ⊙⇘M⇙ v) = (⨁⇘M⇙v∈S. (if v ∈ A then a v ⊙⇘M⇙ v else 𝟬⇘M⇙))"
apply (intro finsum_cong')
by (auto simp add: coeff_in_ring)
from fin inC subset a have "∃b. lincomb a A = lincomb b S ∧ b ∈ S → carrier R"
apply (rule_tac x="?b" in exI)
apply (unfold lincomb_def, auto)
apply (subst if_in)
by (subst extend_sum, auto)
}
from this show "span S ⊆ {lincomb a S |a. a ∈ S → carrier R}"
by (unfold span_def, auto)
next
from fin show "{lincomb a S |a. a ∈ S → carrier R} ⊆ span S"
by (unfold span_def, auto)
qed
text ‹If $v\in \text{span S}$, then we can find a linear combination. This is in an easy to apply
format (e.g. obtain a A where\ldots)›
lemma (in module) in_span:
fixes S v
assumes h2: "S⊆carrier V" and h3: "v∈span S"
shows "∃a A. (A⊆S ∧ (a∈A→carrier R) ∧ (lincomb a A=v))"
proof -
from h2 h3 show ?thesis
apply (unfold span_def)
by auto
qed
text ‹In the finite case, we can take $A=S$.›
lemma (in module) finite_in_span:
fixes S v
assumes fin: "finite S" and h2: "S⊆carrier M" and h3: "v∈span S"
shows "∃a. (a∈S→carrier R) ∧ (lincomb a S=v)"
proof -
from fin h2 have fin_span: "span S = {lincomb a S |a. a ∈ S → carrier R}" by (rule finite_span)
from h3 fin_span show ?thesis by auto
qed
text ‹If a subset is linearly independent, then any linear combination that is 0 must have a
nonzero coefficient outside that set.›
lemma (in module) lincomb_must_include:
fixes A S T b v
assumes inC: "T⊆carrier M" and li: "lin_indpt S" and Ssub: "S⊆T" and Ssub: "A⊆T"
and fin: "finite A"
and b: "b∈A→carrier R" and lc: "lincomb b A=𝟬⇘M⇙" and v_in: "v∈A"
and nz_coeff: "b v≠𝟬⇘R⇙"
shows "∃w∈A-S. b w≠𝟬⇘R⇙"
proof (rule ccontr)
assume 0: "¬(∃ w∈A-S. b w≠𝟬⇘R⇙)"
from 0 have 1: "⋀w. w∈A-S⟹ b w=𝟬⇘R⇙" by auto
have Auni: "A=(S∩A) ∪(A-S)" by auto
from fin b Ssub inC 1 have 2: "lincomb b A = lincomb b (S∩A)"
apply (subst Auni)
apply (subst lincomb_union, auto)
apply (unfold lincomb_def)
apply (subst (2) finsum_all0, auto)
by (subst show_r_zero, auto intro!: finsum_closed)
from 1 2 assms have ld: "lin_dep S"
apply (intro lin_dep_crit[where ?A="S∩A" and ?a="b" and ?v="v"])
by auto
from ld li show False by auto
qed
text ‹A generating set is a set such that the span of $S$ is all of $M$.›
abbreviation (in module) gen_set::"'c set ⇒ bool"
where "gen_set S ≡ (span S = carrier M)"
subsection ‹Submodules›
lemma module_criteria:
fixes R and M
assumes cring: "cring R"
and zero: "𝟬⇘M⇙∈ carrier M"
and add: "∀v w. v∈carrier M ∧ w∈carrier M⟶ v⊕⇘M⇙ w∈ carrier M"
and neg: "∀v∈carrier M. (∃neg_v∈carrier M. v⊕⇘M⇙neg_v=𝟬⇘M⇙)"
and smult: "∀c v. c∈ carrier R ∧ v∈carrier M⟶ c⊙⇘M⇙ v ∈ carrier M"
and comm: "∀v w. v∈carrier M ∧ w∈carrier M⟶ v⊕⇘M⇙ w=w⊕⇘M⇙ v"
and assoc: "∀v w x. v∈carrier M ∧ w∈carrier M ∧ x∈carrier M⟶ (v⊕⇘M⇙ w)⊕⇘M⇙ x= v⊕⇘M⇙ (w⊕⇘M⇙ x)"
and add_id: "∀v∈carrier M. (v⊕⇘M⇙ 𝟬⇘M⇙ =v)"
and compat: "∀a b v. a∈ carrier R ∧ b∈ carrier R ∧ v∈carrier M⟶ (a⊗⇘R⇙ b)⊙⇘M⇙ v =a⊙⇘M⇙ (b⊙⇘M⇙ v)"
and smult_id: "∀v∈carrier M. (𝟭⇘R⇙ ⊙⇘M⇙ v =v)"
and dist_f: "∀a b v. a∈ carrier R ∧ b∈ carrier R ∧ v∈carrier M⟶ (a⊕⇘R⇙ b)⊙⇘M⇙ v =(a⊙⇘M⇙ v) ⊕⇘M⇙ (b⊙⇘M⇙ v)"
and dist_add: "∀a v w. a∈ carrier R ∧ v∈carrier M ∧ w∈carrier M⟶ a⊙⇘M⇙ (v⊕⇘M⇙ w) =(a⊙⇘M⇙ v) ⊕⇘M⇙ (a⊙⇘M⇙ w)"
shows "module R M"
proof -
from assms have 2: "abelian_group M"
by (intro abelian_groupI, auto)
from assms have 3: "module_axioms R M"
by (unfold module_axioms_def, auto)
from 2 3 cring show ?thesis
by (unfold module_def module_def, auto)
qed
text ‹A submodule is $N\subseteq M$ that is closed under addition and scalar multiplication, and
contains 0 (so is not empty).›
locale submodule =
fixes R and N and M (structure)
assumes module: "module R M"
and subset: "N ⊆ carrier M"
and m_closed [intro, simp]: "⟦v ∈ N; w ∈ N⟧ ⟹ v ⊕ w ∈ N"
and zero_closed [simp]: "𝟬 ∈ N"
and smult_closed [intro, simp]: "⟦c ∈ carrier R; v ∈ N⟧ ⟹ c⊙v ∈ N"
abbreviation (in module) md::"'c set ⇒ ('a, 'c, 'd) module_scheme"
where "md N ≡ M⦇carrier :=N⦈"
lemma (in module) carrier_vs_is_self [simp]:
"carrier (md N) = N"
by auto
lemma (in module) submodule_is_module:
fixes N::"'c set"
assumes 0: "submodule R N M"
shows "module R (md N)"
proof (unfold module_def, auto)
show 1: "cring R"..
next
from assms show 2: "abelian_group (md N)"
apply (unfold submodule_def)
apply (intro abelian_groupI, auto)
apply (metis (no_types, opaque_lifting) M.add.m_assoc contra_subsetD)
apply (metis (no_types, opaque_lifting) M.add.m_comm contra_subsetD)
apply (rename_tac v)
txt ‹The inverse of $v$ under addition is $-v$›
apply (rule_tac x="⊖⇘M⇙v" in bexI)
apply (metis M.l_neg contra_subsetD)
by (metis R.add.inv_closed one_closed smult_minus_1 subset_iff)
next
from assms show 3: "module_axioms R (md N)"
apply (unfold module_axioms_def submodule_def, auto)
apply (metis (no_types, opaque_lifting) smult_l_distr contra_subsetD)
apply (metis (no_types, opaque_lifting) smult_r_distr contra_subsetD)
by (metis (no_types, opaque_lifting) smult_assoc1 contra_subsetD)
qed
text ‹$N_1+N_2=\{x+y | x\in N_1,y\in N_2\}$›
definition (in module) submodule_sum:: "['c set, 'c set] ⇒ 'c set"
where "submodule_sum N1 N2 = (λ (x,y). x ⊕⇘M⇙ y) `{(x,y). x∈ N1 ∧ y∈ N2}"
text ‹A module homomorphism $M\to N$ preserves addition and scalar multiplication.›
definition module_hom:: "[('a, 'c0) ring_scheme,
('a,'b1,'c1) module_scheme, ('a,'b2,'c2) module_scheme] ⇒('b1⇒'b2) set"
where "module_hom R M N = {f.
((f∈ carrier M → carrier N)
∧ (∀m1 m2. m1∈carrier M∧ m2∈carrier M ⟶ f (m1 ⊕⇘M⇙ m2) = (f m1) ⊕⇘N⇙ (f m2))
∧ (∀r m. r∈carrier R∧ m∈carrier M ⟶f (r ⊙⇘M⇙ m) = r ⊙⇘N⇙ (f m)))}"
lemma module_hom_closed: "f∈ module_hom R M N ⟹ f∈ carrier M → carrier N"
by (unfold module_hom_def, auto)
lemma module_hom_add: "⟦f∈ module_hom R M N; m1∈carrier M; m2∈carrier M ⟧ ⟹ f (m1 ⊕⇘M⇙ m2) = (f m1) ⊕⇘N⇙ (f m2)"
by (unfold module_hom_def, auto)
lemma module_hom_smult: "⟦f∈ module_hom R M N; r∈carrier R; m∈carrier M ⟧ ⟹ f (r ⊙⇘M⇙ m) = r ⊙⇘N⇙ (f m)"
by (unfold module_hom_def, auto)
locale mod_hom =
M?: module R M + N?: module R N
for R and M and N +
fixes f
assumes f_hom: "f ∈ module_hom R M N"
notes f_add [simp] = module_hom_add [OF f_hom]
and f_smult [simp] = module_hom_smult [OF f_hom]
text ‹Some basic simplification rules for module homomorphisms.›
context mod_hom
begin
lemma f_im [simp, intro]:
assumes "v ∈ carrier M"
shows "f v ∈ carrier N"
proof -
have 0: "mod_hom R M N f"..
from 0 assms show ?thesis
apply (unfold mod_hom_def module_hom_def mod_hom_axioms_def Pi_def)
by auto
qed
definition im:: "'e set"
where "im = f`(carrier M)"
definition ker:: "'c set"
where "ker = {v. v ∈ carrier M & f v = 𝟬⇘N⇙}"
lemma f0_is_0[simp]: "f 𝟬⇘M⇙=𝟬⇘N⇙"
proof -
have 1: "f 𝟬⇘M⇙ = f (𝟬⇘R⇙ ⊙⇘M⇙ 𝟬⇘M⇙)" by simp
have 2: "f (𝟬⇘R⇙ ⊙⇘M⇙ 𝟬⇘M⇙) = 𝟬⇘N⇙"
using M.M.zero_closed N.lmult_0 R.zero_closed f_im f_smult by presburger
from 1 2 show ?thesis by auto
qed
lemma f_neg [simp]: "v ∈ carrier M⟹f (⊖⇘M⇙ v) = ⊖⇘N⇙ f v"
by (simp flip: M.smult_minus_1 N.smult_minus_1)
lemma f_minus [simp]: "⟦v∈carrier M; w∈carrier M⟧⟹f (v⊖⇘M⇙w) = f v ⊖⇘N⇙ f w"
by (simp add: a_minus_def)
lemma ker_is_submodule: "submodule R ker M"
proof -
have 0: "mod_hom R M N f"..
from 0 have 1: "module R M" by (unfold mod_hom_def, auto)
show ?thesis
by (rule submodule.intro, auto simp add: ker_def, rule 1)
qed
lemma im_is_submodule: "submodule R im N"
proof -
have 1: "im ⊆ carrier N" by (auto simp add: im_def image_def mod_hom_def module_hom_def f_im)
have 2: "⋀w1 w2.⟦w1 ∈ im; w2 ∈ im⟧ ⟹ w1 ⊕⇘N⇙ w2 ∈ im"
proof -
fix w1 w2
assume w1: "w1 ∈ im" and w2: "w2∈ im"
from w1 obtain v1 where 3: "v1∈ carrier M ∧ f v1 = w1" by (unfold im_def, auto)
from w2 obtain v2 where 4: "v2∈ carrier M ∧ f v2 = w2" by (unfold im_def, auto)
from 3 4 have 5: "f (v1⊕⇘M⇙v2) = w1 ⊕⇘N⇙ w2" by simp
from 3 4 have 6: "v1⊕⇘M⇙v2∈ carrier M" by simp
from 5 6 have 7: "∃x∈carrier M. w1 ⊕⇘N⇙ w2 = f x" by metis
from 7 show "?thesis w1 w2" by (unfold im_def image_def, auto)
qed
have 3: " 𝟬⇘N⇙ ∈ im"
proof -
have 8: "f 𝟬⇘M⇙ = 𝟬⇘N⇙ ∧ 𝟬⇘M⇙∈carrier M" by auto
from 8 have 9: "∃x∈carrier M. 𝟬⇘N⇙ = f x" by metis
from 9 show ?thesis by (unfold im_def image_def, auto)
qed
have 4: "⋀c w. ⟦c ∈ carrier R; w ∈ im⟧ ⟹ c⊙⇘N⇙ w ∈ im"
proof -
fix c w
assume c: "c ∈ carrier R" and w: "w ∈ im"
from w obtain v where 10: "v∈ carrier M ∧ f v = w" by (unfold im_def, auto)
from c 10 have 11: "f (c⊙⇘M⇙ v) = c⊙⇘N⇙ w∧ (c ⊙⇘M⇙ v∈carrier M)" by auto
from 11 have 12: "∃v1∈carrier M. c⊙⇘N⇙ w=f v1" by metis
from 12 show "?thesis c w" by (unfold im_def image_def, auto)
qed
from 1 2 3 4 show ?thesis by (unfold_locales, auto)
qed
lemma (in mod_hom) f_ker:
"v∈ker ⟹ f v=𝟬⇘N⇙"
by (unfold ker_def, auto)
end
text ‹We will show that for any set $S$, the space of functions $S\to K$ forms a vector space.›
definition (in ring) func_space:: "'z set⇒('a,('z ⇒ 'a)) module"
where "func_space S = ⦇carrier = S→⇩Ecarrier R,
mult = (λ f g. restrict (λv. 𝟬⇘R⇙) S),
one = restrict (λv. 𝟬⇘R⇙) S,
zero = restrict (λv. 𝟬⇘R⇙) S,
add = (λ f g. restrict (λv. f v ⊕⇘R⇙ g v) S),
smult = (λ c f. restrict (λv. c ⊗⇘R⇙ f v) S)⦈"
lemma (in cring) func_space_is_module:
fixes S
shows "module R (func_space S)"
proof -
have 0: "cring R"..
from 0 show ?thesis
apply (auto intro!: module_criteria simp add: func_space_def)
apply (auto simp add: module_def)
apply (rename_tac f)
apply (rule_tac x="restrict (λv'. ⊖⇘R⇙ (f v')) S" in bexI)
apply (auto simp add:restrict_def cong: if_cong split: if_split_asm, auto)
apply (auto simp add: a_ac PiE_mem2 r_neg)
apply (unfold PiE_def extensional_def Pi_def)
by (auto simp add: m_assoc l_distr r_distr)
qed
text ‹Note: one can define $M^n$ from this.›
text ‹A linear combination is a module homomorphism from the space of coefficients to the module,
$(a_v)\mapsto \sum_{v\in S} a_vv$.›
lemma (in module) lincomb_is_mod_hom:
fixes S
assumes h: "finite S" and h2: "S⊆carrier M"
shows "mod_hom R (func_space S) M (λa. lincomb a S)"
proof -
have 0: "module R M"..
{
fix m1 m2
assume m1: "m1 ∈ S →⇩E carrier R" and m2: "m2 ∈ S →⇩E carrier R"
from h h2 m1 m2 have a1: "(⨁⇘M⇙v∈S. (λv∈S. m1 v ⊕⇘R⇙ m2 v) v ⊙⇘M⇙ v) =
(⨁⇘M⇙v∈S. m1 v ⊙⇘M⇙ v ⊕⇘M⇙ m2 v ⊙⇘M⇙ v)"
by (intro finsum_cong', auto simp add: smult_l_distr PiE_mem2)
from h h2 m1 m2 have a2: "(⨁⇘M⇙v∈S. m1 v ⊙⇘M⇙ v ⊕⇘M⇙ m2 v ⊙⇘M⇙ v) =
(⨁⇘M⇙v∈S. m1 v ⊙⇘M⇙ v) ⊕⇘M⇙ (⨁⇘M⇙v∈S. m2 v ⊙⇘M⇙ v)"
by (intro finsum_addf, auto)
from a1 a2 have "(⨁⇘M⇙v∈S. (λv∈S. m1 v ⊕ m2 v) v ⊙⇘M⇙ v) =
(⨁⇘M⇙v∈S. m1 v ⊙⇘M⇙ v) ⊕⇘M⇙ (⨁⇘M⇙v∈S. m2 v ⊙⇘M⇙ v)" by auto
}
hence 1: "⋀m1 m2.
m1 ∈ S →⇩E carrier R ⟹
m2 ∈ S →⇩E carrier R ⟹ (⨁⇘M⇙v∈S. (λv∈S. m1 v ⊕ m2 v) v ⊙⇘M⇙ v) =
(⨁⇘M⇙v∈S. m1 v ⊙⇘M⇙ v) ⊕⇘M⇙ (⨁⇘M⇙v∈S. m2 v ⊙⇘M⇙ v)" by auto
{
fix r m
assume r: "r ∈ carrier R" and m: "m ∈ S →⇩E carrier R"
from h h2 r m have b1: "r ⊙⇘M⇙ (⨁⇘M⇙v∈S. m v ⊙⇘M⇙ v) = (⨁⇘M⇙v∈S. r ⊙⇘M⇙(m v ⊙⇘M⇙ v))"
by (intro finsum_smult, auto)
from h h2 r m have b2: "(⨁⇘M⇙v∈S. (λv∈S. r ⊗ m v) v ⊙⇘M⇙ v) = r ⊙⇘M⇙ (⨁⇘M⇙v∈S. m v ⊙⇘M⇙ v)"
apply (subst b1)
apply (intro finsum_cong', auto)
by (subst smult_assoc1, auto)
}
hence 2: "⋀r m. r ∈ carrier R ⟹
m ∈ S →⇩E carrier R ⟹ (⨁⇘M⇙v∈S. (λv∈S. r ⊗ m v) v ⊙⇘M⇙ v) = r ⊙⇘M⇙ (⨁⇘M⇙v∈S. m v ⊙⇘M⇙ v)"
by auto
from h h2 0 1 2 show ?thesis
apply (unfold mod_hom_def, auto)
apply (rule func_space_is_module)
apply (unfold mod_hom_axioms_def module_hom_def, auto)
apply (rule lincomb_closed, unfold func_space_def, auto)
apply (unfold lincomb_def)
by auto
qed
lemma (in module) lincomb_sum:
assumes A_fin: "finite A" and AinC: "A⊆carrier M" and a_fun: "a∈A→carrier R" and
b_fun: "b∈A→carrier R"
shows "lincomb (λv. a v ⊕⇘R⇙ b v) A = lincomb a A ⊕⇘M⇙ lincomb b A"
proof -
from A_fin AinC interpret mh: mod_hom R "func_space A" M "(λa. lincomb a A)" by (rule
lincomb_is_mod_hom)
let ?a="restrict a A"
let ?b="restrict b A"
from a_fun b_fun A_fin AinC
have 1: "LinearCombinations.module.lincomb M (?a⊕⇘(LinearCombinations.ring.func_space R A)⇙ ?b) A
= LinearCombinations.module.lincomb M (λx. a x ⊕⇘R⇙ b x) A"
by (auto simp add: func_space_def Pi_iff restrict_apply' cong: lincomb_cong)
from a_fun b_fun A_fin AinC
have 2: "LinearCombinations.module.lincomb M ?a A ⊕⇘M⇙
LinearCombinations.module.lincomb M ?b A = LinearCombinations.module.lincomb M a A ⊕⇘M⇙
LinearCombinations.module.lincomb M b A"
by (simp_all add: sum_simp cong: lincomb_cong)
from a_fun b_fun have ainC: "?a∈carrier (LinearCombinations.ring.func_space R A)"
and binC: "?b∈carrier (LinearCombinations.ring.func_space R A)" by (unfold func_space_def, auto)
from ainC binC have "LinearCombinations.module.lincomb M (?a⊕⇘(LinearCombinations.ring.func_space R A)⇙ ?b) A
= LinearCombinations.module.lincomb M ?a A ⊕⇘M⇙
LinearCombinations.module.lincomb M ?b A"
by (simp cong: lincomb_cong)
with 1 2 show ?thesis by auto
qed
text ‹The negative of a function is just pointwise negation.›
lemma (in cring) func_space_neg:
fixes f
assumes "f∈ carrier (func_space S)"
shows "⊖⇘func_space S⇙ f = (λ v. if (v∈S) then ⊖⇘R⇙ f v else undefined)"
proof -
interpret fs: module R "func_space S" by (rule func_space_is_module)
from assms show ?thesis
apply (intro fs.minus_equality)
apply (unfold func_space_def PiE_def extensional_def)
apply auto
apply (intro restrict_ext, auto)
by (simp add: l_neg coeff_in_ring)
qed
text ‹Ditto for subtraction. Note the above is really a special case, when a is the 0 function.›
lemma (in module) lincomb_diff:
assumes A_fin: "finite A" and AinC: "A⊆carrier M" and a_fun: "a∈A→carrier R" and
b_fun: "b∈A→carrier R"
shows "lincomb (λv. a v ⊖⇘R⇙ b v) A = lincomb a A ⊖⇘M⇙ lincomb b A"
proof -
from A_fin AinC interpret mh: mod_hom R "func_space A" M "(λa. lincomb a A)" by (rule
lincomb_is_mod_hom)
let ?a="restrict a A"
let ?b="restrict b A"
from a_fun b_fun have ainC: "?a∈carrier (LinearCombinations.ring.func_space R A)"
and binC: "?b∈carrier (LinearCombinations.ring.func_space R A)" by (unfold func_space_def, auto)
from a_fun b_fun ainC binC A_fin AinC
have 1: "LinearCombinations.module.lincomb M (?a⊖⇘(func_space A)⇙ ?b) A
= LinearCombinations.module.lincomb M (λx. a x ⊖⇘R⇙ b x) A"
apply (subst mh.M.M.minus_eq)
apply (intro lincomb_cong, auto)
apply (subst func_space_neg, auto)
apply (simp add: restrict_def func_space_def)
by (subst R.minus_eq, auto)
from a_fun b_fun A_fin AinC
have 2: "LinearCombinations.module.lincomb M ?a A ⊖⇘M⇙
LinearCombinations.module.lincomb M ?b A = LinearCombinations.module.lincomb M a A ⊖⇘M⇙
LinearCombinations.module.lincomb M b A"
by (simp cong: lincomb_cong)
from ainC binC have "LinearCombinations.module.lincomb M (?a⊖⇘(LinearCombinations.ring.func_space R A)⇙ ?b) A
= LinearCombinations.module.lincomb M ?a A ⊖⇘M⇙
LinearCombinations.module.lincomb M ?b A"
by (simp cong: lincomb_cong)
with 1 2 show ?thesis by auto
qed
text ‹The union of nested submodules is a submodule. We will use this to show that span of any
set is a submodule.›
lemma (in module) nested_union_vs:
fixes I N N'
assumes subm: "⋀i. i∈I⟹ submodule R (N i) M"
and max_exists: "⋀i j. i∈I⟹j∈I⟹ (∃k. k∈I ∧ N i⊆N k ∧ N j ⊆N k)"
and uni: "N'=(⋃ i∈I. N i)"
and ne: "I≠{}"
shows "submodule R N' M"
proof -
have 1: "module R M"..
from subm have all_in: "⋀i. i∈I ⟹ N i ⊆ carrier M"
by (unfold submodule_def, auto)
from uni all_in have 2: "⋀x. x ∈ N' ⟹ x ∈ carrier M"
by auto
from uni have 3: "⋀v w. v ∈ N' ⟹ w ∈ N' ⟹ v ⊕⇘M⇙ w ∈ N'"
proof -
fix v w
assume v: "v ∈ N'" and w: "w ∈ N'"
from uni v w obtain i j where i: "i∈I∧ v∈ N i" and j: "j∈I∧ w∈ N j" by auto
from max_exists i j obtain k where k: "k∈I ∧ N i ⊆ N k ∧ N j ⊆ N k" by presburger
from v w i j k have v2: "v∈N k" and w2: "w∈ N k" by auto
from v2 w2 k subm[of k] have vw: "v ⊕⇘M⇙ w ∈ N k" apply (unfold submodule_def) by auto
from k vw uni show "?thesis v w" by auto
qed
have 4: "𝟬⇘M⇙ ∈ N'"
proof -
from ne obtain i where i: "i∈I" by auto
from i subm have zi: "𝟬⇘M⇙∈N i" by (unfold submodule_def, auto)
from i zi uni show ?thesis by auto
qed
from uni subm have 5: "⋀c v. c ∈ carrier R ⟹ v ∈ N' ⟹ c ⊙⇘M⇙ v ∈ N'"
by (unfold submodule_def, auto)
from 1 2 3 4 5 show ?thesis by (unfold submodule_def, auto)
qed
lemma (in module) span_is_monotone:
fixes S T
assumes subs: "S⊆T"
shows "span S ⊆ span T"
proof -
from subs show ?thesis
by (unfold span_def, auto)
qed
lemma (in module) span_is_submodule:
fixes S
assumes h2: "S⊆carrier M"
shows "submodule R (span S) M"
proof (cases "S={}")
case True
moreover have "module R M"..
ultimately show ?thesis apply (unfold submodule_def span_def lincomb_def, auto) done
next
case False
show ?thesis
proof (rule nested_union_vs[where ?I="{F. F⊆S ∧ finite F}" and ?N="λF. span F" and ?N'="span S"])
show " ⋀F. F ∈ {F. F ⊆ S ∧ finite F} ⟹ submodule R (span F) M"
proof -
fix F
assume F: "F ∈ {F. F ⊆ S ∧ finite F}"
from F have h1: "finite F" by auto
from F h2 have inC: "F⊆carrier M" by auto
from h1 inC interpret mh: mod_hom R "(func_space F)" M "(λa. lincomb a F)"
by (rule lincomb_is_mod_hom)
from h1 inC have 1: "mh.im = span F"
apply (unfold mh.im_def)
apply (unfold func_space_def, simp)
apply (subst finite_span, auto)
apply (unfold image_def, auto)
apply (rule_tac x="restrict a F" in bexI)
by (auto intro!: lincomb_cong)
from 1 show "submodule R (span F) M" by (metis mh.im_is_submodule)
qed
next
show "⋀i j. i ∈ {F. F ⊆ S ∧ finite F} ⟹
j ∈ {F. F ⊆ S ∧ finite F} ⟹
∃k. k ∈ {F. F ⊆ S ∧ finite F} ∧ span i ⊆ span k ∧ span j ⊆ span k"
proof -
fix i j
assume i: "i ∈ {F. F ⊆ S ∧ finite F}" and j: "j ∈ {F. F ⊆ S ∧ finite F}"
from i j show "?thesis i j"
apply (rule_tac x="i∪j" in exI)
apply (auto del: subsetI)
by (intro span_is_monotone, auto del: subsetI)+
qed
next
show "span S=(⋃ i∈{F. F ⊆ S ∧ finite F}. span i)"
by (unfold span_def,auto)
next
have ne: "S≠{}" by fact
from ne show "{F. F ⊆ S ∧ finite F} ≠ {}" by auto
qed
qed
text ‹A finite sum does not depend on the ambient module. This can be done for monoid, but
"submonoid" isn't currently defined. (It can be copied, however, for groups\ldots)
This lemma requires a somewhat annoying lemma foldD-not-depend. Then we show that linear combinations,
linear independence, span do not depend on the ambient module.›
lemma (in module) finsum_not_depend:
fixes a A N
assumes h1: "finite A" and h2: "A⊆N" and h3: "submodule R N M" and h4: "f:A→N"
shows "(⨁⇘(md N)⇙ v∈A. f v) = (⨁⇘M⇙ v∈A. f v)"
proof -
from h1 h2 h3 h4 show ?thesis
apply (unfold finsum_def finprod_def)
apply simp
apply (intro foldD_not_depend[where ?B="A"])
apply (unfold submodule_def LCD_def, auto)
apply (meson M.add.m_lcomm PiE subsetCE)+
done
qed
lemma (in module) lincomb_not_depend:
fixes a A N
assumes h1: "finite A" and h2: "A⊆N" and h3: "submodule R N M" and h4: "a:A→carrier R"
shows "lincomb a A = module.lincomb (md N) a A"
proof -
from h3 interpret N: module R "(md N)" by (rule submodule_is_module)
have 3: "N=carrier (md N)" by auto
have 4: "(smult M ) = (smult (md N))" by auto
from h1 h2 h3 h4 have "(⨁⇘(md N)⇙v∈A. a v ⊙⇘M⇙ v) = (⨁⇘M⇙v∈A. a v ⊙⇘M⇙ v)"
apply (intro finsum_not_depend)
using N.summands_valid by auto
from this show ?thesis by (unfold lincomb_def N.lincomb_def, simp)
qed
lemma (in module) span_li_not_depend:
fixes S N
assumes h2: "S⊆N" and h3: "submodule R N M"
shows "module.span R (md N) S = module.span R M S"
and "module.lin_dep R (md N) S = module.lin_dep R M S"
proof -
from h3 interpret w: module R "(md N)" by (rule submodule_is_module)
from h2 have 1:"submodule R (module.span R (md N) S) (md N)"
by (intro w.span_is_submodule, simp)
have 3: "⋀a A. (finite A ∧ A⊆S ∧ a ∈ A → carrier R ⟹
module.lincomb M a A = module.lincomb (md N) a A)"
proof -
fix a A
assume 31: "finite A ∧ A⊆S ∧ a ∈ A → carrier R"
from assms 31 show "?thesis a A"
by (intro lincomb_not_depend, auto)
qed
from 3 show 4: "module.span R (md N) S = module.span R M S"
apply (unfold span_def w.span_def)
apply auto
by (metis)
have zeros: "𝟬⇘md N⇙=𝟬⇘M⇙" by auto
from assms 3 show 5: "module.lin_dep R (md N) S = module.lin_dep R M S"
apply (unfold lin_dep_def w.lin_dep_def)
apply (subst zeros)
by metis
qed
lemma (in module) span_is_subset:
fixes S N
assumes h2: "S⊆N" and h3: "submodule R N M"
shows "span S ⊆ N"
proof -
from h3 interpret w: module R "(md N)" by (rule submodule_is_module)
from h2 have 1:"submodule R (module.span R (md N) S) (md N)"
by (intro w.span_is_submodule, simp)
from assms have 4: "module.span R (md N) S = module.span R M S"
by (rule span_li_not_depend)
from 1 4 have 5: "submodule R (module.span R M S) (md N)" by auto
from 5 show ?thesis by (unfold submodule_def, simp)
qed
lemma (in module) span_is_subset2:
fixes S
assumes h2: "S⊆carrier M"
shows "span S ⊆ carrier M"
proof -
have 0: "module R M"..
from 0 have h3: "submodule R (carrier M) M" by (unfold submodule_def, auto)
from h2 h3 show ?thesis by (rule span_is_subset)
qed
lemma (in module) in_own_span:
fixes S
assumes inC:"S⊆carrier M"
shows "S ⊆ span S"
proof -
from inC show ?thesis
apply (unfold span_def, auto)
apply (rename_tac v)
apply (rule_tac x="(λ w. if (w=v) then 𝟭⇘R⇙ else 𝟬⇘R⇙)" in exI)
apply (rule_tac x="{v}" in exI)
apply (unfold lincomb_def)
by auto
qed
lemma (in module) supset_ld_is_ld:
fixes A B
assumes ld: "lin_dep A" and sub: "A ⊆ B"
shows "lin_dep B"
proof -
from ld obtain A' a v where 1: "(finite A' ∧ A'⊆A ∧ (a∈ (A'→carrier R)) ∧ (lincomb a A' = 𝟬⇘M⇙) ∧ (v∈A') ∧ (a v≠ 𝟬⇘R⇙))"
by (unfold lin_dep_def, auto)
from 1 sub show ?thesis
apply (unfold lin_dep_def)
apply (rule_tac x="A'" in exI)
apply (rule_tac x="a" in exI)
apply (rule_tac x="v" in exI)
by auto
qed
lemma (in module) subset_li_is_li:
fixes A B
assumes li: "lin_indpt A" and sub: "B ⊆ A"
shows "lin_indpt B"
proof (rule ccontr)
assume ld: "¬lin_indpt B"
from ld sub have ldA: "lin_dep A" by (metis supset_ld_is_ld)
from li ldA show False by auto
qed
lemma (in mod_hom) hom_sum:
fixes A B g
assumes h2: "A⊆carrier M" and h3: "g:A→carrier M"
shows "f (⨁⇘M⇙ a∈A. g a) = (⨁⇘N⇙ a∈A. f (g a))"
proof -
from h2 h3 show ?thesis
proof (induct A rule: infinite_finite_induct)
case (insert a A)
then have "(⨁⇘N⇙a∈insert a A. f (g a)) = f (g a) ⊕⇘N⇙ (⨁⇘N⇙a∈A. f (g a))"
by (intro finsum_insert, auto)
with insert.prems insert.hyps show ?case
by simp
qed auto
qed
end