# Theory VectorSpace.SumSpaces

section ‹The direct sum of modules.›

theory SumSpaces
imports Main
"HOL-Algebra.Module"
"HOL-Algebra.Coset"
RingModuleFacts
MonoidSums
FunctionLemmas
LinearCombinations
begin

text ‹We define the direct sum $M_1\oplus M_2$ of 2 vector spaces as the set $M_1\times M_2$ under
definition direct_sum:: "('a,'b, 'd) module_scheme ⇒ ('a, 'c, 'e) module_scheme ⇒('a, ('b×'c)) module" (*(infixl "(⊕)" 50)*)
where  "direct_sum M1 M2 = ⦇carrier = carrier M1 × carrier M2,
mult = (λ v w. (𝟬⇘M1⇙, 𝟬⇘M2⇙)),
one =  (𝟬⇘M1⇙, 𝟬⇘M2⇙),
zero = (𝟬⇘M1⇙, 𝟬⇘M2⇙),
add = (λ v w. (fst v ⊕⇘M1⇙ fst w, snd v ⊕⇘M2⇙ snd w)),
smult = (λ c v. (c ⊙⇘M1⇙ fst v, c ⊙⇘M2⇙ snd v))⦈"

lemma direct_sum_is_module:
fixes R M1 M2
assumes h1: "module R M1" and h2: "module R M2"
shows "module R (direct_sum M1 M2)"
proof -
from h1 have 1: "cring R" by (unfold module_def, auto)
from h1 interpret v1: module R M1 by auto
from h2 interpret v2: module R M2 by auto
from h1 h2 have 2: "abelian_group (direct_sum M1 M2)"
apply (intro abelian_groupI, auto)
apply (unfold direct_sum_def, auto)
by (auto simp add: v1.a_ac v2.a_ac)
from h1 h2 assms have 3: "module_axioms R (direct_sum M1 M2)"
apply (unfold module_axioms_def, auto)
apply (unfold direct_sum_def, auto)
by (auto simp add: v1.smult_l_distr v2.smult_l_distr v1.smult_r_distr v2.smult_r_distr
v1.smult_assoc1 v2.smult_assoc1)
from 1 2 3  show ?thesis by (unfold module_def, auto)
qed

definition inj1:: "('a,'b) module ⇒ ('a, 'c) module ⇒('b⇒('b×'c))"
where "inj1 M1 M2 = (λv. (v, 𝟬⇘M2⇙))"

definition inj2:: "('a,'b) module ⇒ ('a, 'c) module ⇒('c⇒('b×'c))"
where "inj2 M1 M2 = (λv. (𝟬⇘M1⇙, v))"

lemma inj1_hom:
fixes R M1 M2
assumes h1: "module R M1" and h2: "module R M2"
shows "mod_hom R M1 (direct_sum M1 M2) (inj1 M1 M2)"
proof -
from h1 interpret v1:module R M1 by auto
from h2 interpret v2:module R M2 by auto
from h1 h2 show ?thesis
apply (unfold mod_hom_def module_hom_def mod_hom_axioms_def inj1_def, auto)
apply (rule direct_sum_is_module, auto)
by (unfold direct_sum_def, auto)
qed

lemma inj2_hom:
fixes R M1 M2
assumes h1: "module R M1" and h2: "module R M2"
shows "mod_hom R M2 (direct_sum M1 M2) (inj2 M1 M2)"
proof -
from h1 interpret v1:module R M1 by auto
from h2 interpret v2:module R M2 by auto
from h1 h2 show ?thesis
apply (unfold mod_hom_def module_hom_def mod_hom_axioms_def inj2_def, auto)
apply (rule direct_sum_is_module, auto)
by (unfold direct_sum_def, auto)
qed

text ‹For submodules $M_1,M_2\subseteq M$, the map $M_1\oplus M_2\to M$ given by $(m_1,m_2)\mapsto m_1+m_2$ is linear.›
lemma (in module) sum_map_hom:
fixes M1 M2
assumes h1: "submodule R M1 M" and h2: "submodule R M2 M"
shows "mod_hom R (direct_sum (md M1) (md M2)) M (λ v. (fst v) ⊕⇘M⇙ (snd v))"
proof -
have 0: "module R M"..
from h1 have 1: "module R (md M1)" by (rule submodule_is_module)
from h2 have 2: "module R (md M2)" by (rule submodule_is_module)
from h1 interpret w1: module R "(md M1)" by (rule submodule_is_module)
from h2 interpret w2: module R "(md M2)" by (rule submodule_is_module)
from 0 h1 h2 1 2 show ?thesis
apply (unfold mod_hom_def mod_hom_axioms_def module_hom_def, auto)
apply (rule direct_sum_is_module, auto)
apply (unfold direct_sum_def, auto)
apply (unfold submodule_def, auto)
by (auto simp add: a_ac smult_r_distr ring_subset_carrier)
(*key is a_ac, permutative rewrite rule*)
qed

lemma (in module) sum_is_submodule:
fixes N1 N2
assumes h1: "submodule R N1 M" and h2: "submodule R N2 M"
shows "submodule R (submodule_sum N1 N2) M"
proof -
from h1 h2 interpret l: mod_hom R "(direct_sum (md N1) (md N2))" M "(λ v. (fst v) ⊕⇘M⇙ (snd v))"
by (rule sum_map_hom)
have 1: "l.im =submodule_sum N1 N2"
apply (unfold l.im_def submodule_sum_def)
apply (unfold direct_sum_def, auto)
by (unfold image_def, auto)
have 2: "submodule R (l.im) M" by (rule l.im_is_submodule)
from 1 2 show ?thesis by auto
qed

lemma (in module) in_sum:
fixes N1 N2
assumes h1: "submodule R N1 M" and h2: "submodule R N2 M"
shows "N1 ⊆ submodule_sum N1 N2"
proof -
from h1 h2 show ?thesis
apply auto
apply (unfold submodule_sum_def image_def, auto)
apply (rename_tac v)
apply (rule_tac x="v" in bexI)
apply (rule_tac x="𝟬⇘M⇙" in bexI)
by (unfold submodule_def, auto)
qed

lemma (in module) msum_comm:
fixes N1 N2
assumes h1: "submodule R N1 M" and h2: "submodule R N2 M"
shows "(submodule_sum N1 N2) = (submodule_sum N2 N1)"
proof -
(*have 0: "module R M"..*)
from h1 h2 show ?thesis
apply (unfold submodule_sum_def image_def, auto)
apply (unfold submodule_def)
apply (rename_tac v w)
(* Alternatively, apply (rule_tac x="w" in bexI, rule_tac x="v" in bexI,
auto simp add: ring_subset_carrier M.a_ac)+ *)
qed

text ‹If $M_1,M_2\subseteq M$ are submodules, then $M_1+M_2$ is the minimal subspace such that
both $M_1\subseteq M$ and $M_2\subseteq M$.›
lemma (in module) sum_is_minimal:
fixes N N1 N2
assumes h1: "submodule R N1 M" and h2: "submodule R N2 M" and h3: "submodule R N M"
shows "(submodule_sum N1 N2) ⊆ N ⟷ N1 ⊆ N ∧ N2 ⊆ N"
proof -
have 1: "(submodule_sum N1 N2) ⊆ N ⟹ N1 ⊆ N ∧ N2 ⊆ N"
proof -
assume 10: "(submodule_sum N1 N2) ⊆ N"
from h1 h2 have 11: "N1⊆submodule_sum N1 N2" by (rule in_sum)
from h2 h1 have 12: "N2⊆submodule_sum N2 N1" by (rule in_sum)
from 12 h1 h2 have 13: "N2⊆submodule_sum N1 N2" by (metis msum_comm)
from 10 11 13 show ?thesis by auto
qed
have 2: "N1 ⊆ N ∧ N2 ⊆ N ⟹ (submodule_sum N1 N2) ⊆ N"
proof -
assume 19: "N1 ⊆ N ∧ N2 ⊆ N"
{
fix v
assume 20: "v∈submodule_sum N1 N2"
from 20 obtain w1 w2 where 21: "w1∈N1" and 22: "w2∈N2" and 23: "v=w1⊕⇘M⇙ w2"
by (unfold submodule_sum_def image_def, auto)
from 19 21 22 23 h3 have "v ∈ N"
apply (unfold submodule_def, auto)
by (metis (poly_guards_query)  contra_subsetD)
(*how is an obtain goal rep'd?*)
}
thus ?thesis
by (metis subset_iff)
qed
from 1 2 show ?thesis by metis
qed

text ‹$\text{span} A\cup B = \text{span} A + \text{span} B$›
lemma (in module) span_union_is_sum:
fixes A B
assumes  h2: "A⊆carrier M" and h3: "B⊆carrier M"
shows "span (A∪ B) = submodule_sum (span A) (span B)"
proof-
let ?AplusB="submodule_sum (span A) (span B)"
from  h2 have s0: "submodule R (span A) M" by (rule span_is_submodule)
from  h3 have s1: "submodule R (span B) M" by (rule span_is_submodule)
from s0 have s0_1: "(span A)⊆carrier M" by (unfold submodule_def, auto)
from s1 have s1_1: "(span B)⊆carrier M" by (unfold submodule_def, auto)
from h2 h3 have 1: "A∪B⊆carrier M" by auto
from  1 have 2: "submodule R (span (A∪B)) M" by (rule span_is_submodule)
from s0 s1 have 3: "submodule R ?AplusB M" by (rule sum_is_submodule)
have c1: "span (A∪B) ⊆ ?AplusB"
(*span(A∪B) ⊆ span(A) + span(B) *)
proof -
from  h2 have a1: "A⊆span A" by (rule in_own_span)
from s0 s1 have a2: "span A ⊆ ?AplusB" by (rule in_sum) (*M⊆M+N*)
from a1 a2 have a3: "A⊆ ?AplusB" by auto
(*similarly*)
from  h3 have b1: "B⊆span B" by (rule in_own_span)
from s1 s0 have b2: "span B ⊆ ?AplusB" by (metis in_sum msum_comm) (*M⊆M+N*)
from b1 b2 have b3: "B⊆ ?AplusB" by auto
from a3 b3 have 5: "A∪B⊆ ?AplusB" by auto
(*by default simp *)
from 5 3 show ?thesis by (rule span_is_subset)
qed
have c2: "?AplusB ⊆ span (A∪B)"
proof -
have 11: "A⊆A∪B" by auto
have 12: "B⊆A∪B" by auto
from  11 have 21:"span A ⊆span (A∪B)" by (rule span_is_monotone)
from  12 have 22:"span B ⊆span (A∪B)" by (rule span_is_monotone)
from s0 s1 2 21 22 show ?thesis by (auto simp add: sum_is_minimal)
qed
from c1 c2 show ?thesis by auto
qed

end