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:
  "aAcarrier R; xA  a x carrier R"
by (rule Pi_mem)

lemma (in ring) coeff_in_ring2:
  " xA;aAcarrier R  a x carrier R"
by (metis Pi_mem)

lemma ring_subset_carrier:
  "x A; Acarrier R  x carrier R"
by auto

lemma disj_if:
  "AB={}; x B  (if xA 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 = (MvA. (a v Mv))"

lemma (in module) summands_valid:
  fixes A a
  assumes h2: "A carrier M" and h3: "a(Acarrier R)"
  shows " v A. (((a v) Mv) 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(Scarrier R)"
  shows "lincomb a S  carrier M"
proof -
  from h2 h3 show ?thesis by (unfold lincomb_def, auto intro:finsum_closed)
(*doesn't work with simp*)
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. vA  a v = b v" and h5: "b Bcarrier 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: "AB  carrier M" 
    and h4: "AB={}" and h5: "a(ABcarrier R)"
  shows "lincomb a (AB) = lincomb a A Mlincomb 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: "AB  carrier M" 
    and h4: "AB={}" and h5: "aAcarrier R" and h6: "bBcarrier R"
  shows "lincomb a A Mlincomb b B = lincomb (λv. if (vA) then a v else b v) (AB)"
    (is "lincomb a A Mlincomb b B = lincomb ?c (AB)")
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(Scarrier R)" and h4:"vS"
  shows "lincomb a S = ((a v) Mv) Mlincomb 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

(*alternate form of the above*)
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:"vS" and 
h5:"v carrier M"
  shows "lincomb a (S{v}) = ((a v) Mv) Mlincomb 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. vS ¬P v" and h3: "cScarrier 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: "Acarrier M"  and h3: "aAcarrier R" and h4: "ccarrier R"
  shows "lincomb (λw. cRa w) A = cM(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  AS  (a (Acarrier R))  (lincomb a A = 𝟬M)  (vA)  (a v 𝟬R)))"
  (*shows "∃a. (a∈ (S→carrier K)) ∧ (lincomb a S = 𝟬V) ∧ (∃v∈S. a v≠ 𝟬K)"*)

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: "Scarrier M"
  shows "a v. (a (Scarrier R))  (lincomb a S = 𝟬M)  (vS)  (a v 𝟬R)"
proof - 
  from ld obtain A a v where A: "(AS  (a (Acarrier R))  (lincomb a A = 𝟬M)  (vA)  (a v 𝟬R))" 
    by (unfold lin_dep_def, auto)
  let ?b="λw. if wA then a w else 𝟬R⇙" (*extend the coefficients to be 0 outside of A*)
  from finS inC A have if_in: "(MvS. (if v  A then a v else 𝟬) Mv) = (MvS. (if v  A then a v Mv else 𝟬M))"
    apply auto
      apply (intro finsum_cong') 
    by (auto simp add: coeff_in_ring)  (*massage the sum*)
  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: "AS" and h1: "(a (Acarrier 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: "Acarrier M" and
    lc0: "a. a (Acarrier R)  (lincomb a A = 𝟬M)  ( vA. 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 (Acarrier R))  (lincomb a A = 𝟬M)  (vA)  (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: "Scarrier 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  AS  a (Acarrier 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: "Scarrier M"
  shows "span S = {lincomb a S | a. a (Scarrier 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: "(MvS. ?b v Mv) = (MvS. (if v  A then a v Mv else 𝟬M))"
      apply (intro finsum_cong') 
        by (auto simp add: coeff_in_ring)  (*massage the sum*)
    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: "Scarrier V" and h3: "vspan S"
  shows "a A. (AS  (aAcarrier 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: "Scarrier M" and h3: "vspan S"
  shows "a. (aScarrier 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: "Tcarrier M" and li: "lin_indpt S" and Ssub: "ST" and Ssub: "AT"
    and fin: "finite A"
    and b: "bAcarrier R" and lc: "lincomb b A=𝟬M⇙" and v_in: "vA"
    and nz_coeff: "b v𝟬R⇙"
  shows "wA-S. b w𝟬R⇙"
proof (rule ccontr) 
  (*we may assume B doesn't intersect A.*)
  assume 0: "¬( wA-S. b w𝟬R)"
  from 0 have 1: "w. wA-S b w=𝟬R⇙" by auto
  have Auni: "A=(SA) (A-S)" by auto
  from fin b Ssub inC 1 have 2: "lincomb b A = lincomb b (SA)"(* ⊕M lincomb b ((-S)∩A)*)
    apply (subst Auni) 
    apply (subst lincomb_union, auto)
    (*apply (intro r_zero)*)
    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="SA" 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. vcarrier M  wcarrier M vMw carrier M"
      and neg: "vcarrier M. (neg_vcarrier M. vMneg_v=𝟬M)"
      and smult: "c v. c carrier R  vcarrier M cMv  carrier M"
      and comm: "v w. vcarrier M  wcarrier M vMw=wMv"
      and assoc: "v w x. vcarrier M  wcarrier M  xcarrier M (vMw)Mx= vM(wMx)"
      and add_id: "vcarrier M. (vM𝟬M=v)"
      and compat: "a b v. a carrier R  b carrier R  vcarrier M (aRb)Mv =aM(bMv)"
      and smult_id: "vcarrier M. (𝟭RMv =v)"
      and dist_f: "a b v. a carrier R  b carrier R  vcarrier M (aRb)Mv =(aMv) M(bMv)"
      and dist_add: "a v w. a carrier R  vcarrier M  wcarrier M aM(vMw) =(aMv) M(aMw)"
  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" (*prevents N from being the empty set*)
    and smult_closed [intro, simp]: "c  carrier R; v  N  cv  N"

abbreviation (in module) md::"'c set  ('a, 'c, 'd) module_scheme"
  where "md N  Mcarrier :=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="Mv" 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 My) `{(x,y). x  N1  y N2}"
(*This only depends on the carriers, actually, so it could be defined on that level if desired.*)

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. m1carrier M m2carrier M  f (m1 Mm2) = (f m1) N(f m2))
     (r m. rcarrier R mcarrier M f (r Mm) = 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; m1carrier M; m2carrier M   f (m1 Mm2) = (f m1) N(f m2)"
by (unfold module_hom_def, auto)

lemma module_hom_smult: "f module_hom R M N; rcarrier R; mcarrier M    f (r Mm) = 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" (*doesn't work if ⟹*)
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 (𝟬RM𝟬M)" by simp
  have 2: "f (𝟬RM𝟬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 Mf (Mv) = Nf v"
  by (simp flip: M.smult_minus_1 N.smult_minus_1)

lemma f_minus [simp]: "vcarrier M; wcarrier Mf (vMw) = f v Nf 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) (*rmult_0*)
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 Nw2  im" (*it can't auto convert ⋀ and w/ o*)
  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 (v1Mv2) = w1 Nw2" by simp
    from 3 4 have 6: "v1Mv2 carrier M" by simp
    from 5 6 have 7: "xcarrier M. w1 Nw2 = 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 𝟬Mcarrier M" by auto
    from 8 have 9: "xcarrier 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  cNw  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 (cMv) = cNw (c Mvcarrier M)" by auto
    from 11 have 12: "v1carrier M.  cNw=f v1" by metis 
    from 12 show "?thesis c w" by (unfold im_def image_def, auto) (*sensitive to ordering*)
  qed
  from 1 2 3 4 show ?thesis by (unfold_locales, auto)
qed

lemma (in mod_hom) f_ker:
  "vker  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 = SEcarrier 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 Rg v) S),
                  smult = (λ c f. restrict (λv. c Rf 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) (*intro: ext*)
      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: "Scarrier 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: "(MvS. (λvS. m1 v Rm2 v) v Mv) = 
      (MvS. m1 v Mv Mm2 v Mv)"
      by (intro finsum_cong', auto simp add: smult_l_distr PiE_mem2)
    from h h2 m1 m2 have a2: "(MvS. m1 v Mv Mm2 v Mv) = 
      (MvS. m1 v Mv) M(MvS. m2 v Mv)"
      by (intro finsum_addf, auto)
    from a1 a2 have "(MvS. (λvS. m1 v  m2 v) v Mv) =
       (MvS. m1 v Mv) M(MvS. m2 v Mv)" by auto
  }
  hence 1: "m1 m2.
       m1  S E carrier R 
       m2  S E carrier R  (MvS. (λvS. m1 v  m2 v) v Mv) =
       (MvS. m1 v Mv) M(MvS. m2 v Mv)" 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(MvS. m v Mv) =  (MvS. r M(m v Mv))"
      by (intro finsum_smult, auto) 
    from h h2 r m have b2: "(MvS. (λvS. r  m v) v Mv) = r M(MvS. m v Mv)"
      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  (MvS. (λvS. r  m v) v Mv) = r M(MvS. m v Mv)" 
            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

(*These are not really used.*)
lemma (in module) lincomb_sum:
  assumes A_fin: "finite A" and AinC: "Acarrier M" and a_fun: "aAcarrier R" and 
    b_fun: "bAcarrier R" 
  shows "lincomb (λv. a v Rb v) A = lincomb a A Mlincomb 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 Rb 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 MLinearCombinations.module.lincomb M ?b A = LinearCombinations.module.lincomb M a A MLinearCombinations.module.lincomb M b A"
    by (simp_all add: sum_simp cong: lincomb_cong)
  from a_fun b_fun have ainC: "?acarrier (LinearCombinations.ring.func_space R A)" 
    and binC: "?bcarrier (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 MLinearCombinations.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 Sf = (λ v. if (vS) then Rf 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: "Acarrier M" and a_fun: "aAcarrier R" and 
    b_fun: "bAcarrier R" 
  shows "lincomb (λv. a v Rb v) A = lincomb a A Mlincomb 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: "?acarrier (LinearCombinations.ring.func_space R A)" 
    and binC: "?bcarrier (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 Rb 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 MLinearCombinations.module.lincomb M ?b A = LinearCombinations.module.lincomb M a A MLinearCombinations.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 MLinearCombinations.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. iI submodule R (N i) M"
    and max_exists: "i j. iIjI (k. kI  N iN k  N j N k)" 
    and uni: "N'=( iI. N i)"
    and ne: "I{}"
  shows "submodule R N' M"
proof -
  have 1: "module R M"..
  from subm have all_in: "i. iI  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 Mw  N'"
  proof - 
    fix v w
    assume v: "v  N'" and w: "w  N'"
    from uni v w obtain i j where i: "iI v N i" and j: "jI w N j" by auto
    from max_exists i j obtain k where k: "kI  N i  N k  N j  N k" by presburger
    from v w i j k have v2: "vN k" and w2: "w N k" by auto
    from v2 w2 k subm[of k] have vw: "v Mw  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: "iI" by auto
    from i subm have zi: "𝟬MN 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 Mv  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: "ST"
  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: "Scarrier 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. FS  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: "Fcarrier 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="ij" 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: "AN" and h3: "submodule R N M" and h4: "f:AN"
  shows "((md N)vA. f v) = (MvA. 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: "AN" and h3: "submodule R N M" and h4: "a:Acarrier 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)vA. a v Mv) = (MvA. a v Mv)"
    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: "SN" 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  AS  a  A  carrier R  
    module.lincomb M a A = module.lincomb (md N) a A)"
  proof - 
    fix a A
    assume 31: "finite A  AS  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: "SN" 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: "Scarrier 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:"Scarrier 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 𝟭Relse 𝟬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)  (vA')  (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: "Acarrier M" and h3: "g:Acarrier M"
  shows "f (MaA. g a) = (NaA. f (g a))"
proof -   
  from h2 h3 show ?thesis
  proof (induct A rule: infinite_finite_induct) (*doesn't work on outside?*)
    case (insert a A)
    then have "(Nainsert a A. f (g a)) = f (g a) N(NaA. f (g a))"  
      by (intro finsum_insert, auto)
    with insert.prems insert.hyps show ?case
      by simp
  qed auto
qed


end