(* Title: HOL/Algebra/Embedded_Algebras.thy Author: Paulo Emílio de Vilhena *) theory Embedded_Algebras imports Subrings Generated_Groups begin section ‹Definitions› locale embedded_algebra = K?: subfield K R + R?: ring R for K :: "'a set" and R :: "('a, 'b) ring_scheme" (structure) definition (in ring) line_extension :: "'a set ⇒ 'a ⇒ 'a set ⇒ 'a set" where "line_extension K a E = (K #> a) <+>⇘R⇙ E" fun (in ring) Span :: "'a set ⇒ 'a list ⇒ 'a set" where "Span K Us = foldr (line_extension K) Us { 𝟬 }" fun (in ring) combine :: "'a list ⇒ 'a list ⇒ 'a" where "combine (k # Ks) (u # Us) = (k ⊗ u) ⊕ (combine Ks Us)" | "combine Ks Us = 𝟬" inductive (in ring) independent :: "'a set ⇒ 'a list ⇒ bool" where li_Nil [simp, intro]: "independent K []" | li_Cons: "⟦ u ∈ carrier R; u ∉ Span K Us; independent K Us ⟧ ⟹ independent K (u # Us)" inductive (in ring) dimension :: "nat ⇒ 'a set ⇒ 'a set ⇒ bool" where zero_dim [simp, intro]: "dimension 0 K { 𝟬 }" | Suc_dim: "⟦ v ∈ carrier R; v ∉ E; dimension n K E ⟧ ⟹ dimension (Suc n) K (line_extension K v E)" subsubsection ‹Syntactic Definitions› abbreviation (in ring) dependent :: "'a set ⇒ 'a list ⇒ bool" where "dependent K U ≡ ¬ independent K U" definition over :: "('a ⇒ 'b) ⇒ 'a ⇒ 'b" (infixl "over" 65) where "f over a = f a" context ring begin subsection ‹Basic Properties - First Part› lemma line_extension_consistent: assumes "subring K R" shows "ring.line_extension (R ⦇ carrier := K ⦈) = line_extension" unfolding ring.line_extension_def[OF subring_is_ring[OF assms]] line_extension_def by (simp add: set_add_def set_mult_def) lemma Span_consistent: assumes "subring K R" shows "ring.Span (R ⦇ carrier := K ⦈) = Span" unfolding ring.Span.simps[OF subring_is_ring[OF assms]] Span.simps line_extension_consistent[OF assms] by simp lemma combine_in_carrier [simp, intro]: "⟦ set Ks ⊆ carrier R; set Us ⊆ carrier R ⟧ ⟹ combine Ks Us ∈ carrier R" by (induct Ks Us rule: combine.induct) (auto) lemma combine_r_distr: "⟦ set Ks ⊆ carrier R; set Us ⊆ carrier R ⟧ ⟹ k ∈ carrier R ⟹ k ⊗ (combine Ks Us) = combine (map ((⊗) k) Ks) Us" by (induct Ks Us rule: combine.induct) (auto simp add: m_assoc r_distr) lemma combine_l_distr: "⟦ set Ks ⊆ carrier R; set Us ⊆ carrier R ⟧ ⟹ u ∈ carrier R ⟹ (combine Ks Us) ⊗ u = combine Ks (map (λu'. u' ⊗ u) Us)" by (induct Ks Us rule: combine.induct) (auto simp add: m_assoc l_distr) lemma combine_eq_foldr: "combine Ks Us = foldr (λ(k, u). λl. (k ⊗ u) ⊕ l) (zip Ks Us) 𝟬" by (induct Ks Us rule: combine.induct) (auto) lemma combine_replicate: "set Us ⊆ carrier R ⟹ combine (replicate (length Us) 𝟬) Us = 𝟬" by (induct Us) (auto) lemma combine_take: "combine (take (length Us) Ks) Us = combine Ks Us" by (induct Us arbitrary: Ks) (auto, metis combine.simps(1) list.exhaust take.simps(1) take_Suc_Cons) lemma combine_append_zero: "set Us ⊆ carrier R ⟹ combine (Ks @ [ 𝟬 ]) Us = combine Ks Us" proof (induct Ks arbitrary: Us) case Nil thus ?case by (induct Us) (auto) next case Cons thus ?case by (cases Us) (auto) qed lemma combine_prepend_replicate: "⟦ set Ks ⊆ carrier R; set Us ⊆ carrier R ⟧ ⟹ combine ((replicate n 𝟬) @ Ks) Us = combine Ks (drop n Us)" proof (induct n arbitrary: Us, simp) case (Suc n) thus ?case by (cases Us) (auto, meson combine_in_carrier ring_simprules(8) set_drop_subset subset_trans) qed lemma combine_append_replicate: "set Us ⊆ carrier R ⟹ combine (Ks @ (replicate n 𝟬)) Us = combine Ks Us" by (induct n) (auto, metis append.assoc combine_append_zero replicate_append_same) lemma combine_append: assumes "length Ks = length Us" and "set Ks ⊆ carrier R" "set Us ⊆ carrier R" and "set Ks' ⊆ carrier R" "set Vs ⊆ carrier R" shows "(combine Ks Us) ⊕ (combine Ks' Vs) = combine (Ks @ Ks') (Us @ Vs)" using assms proof (induct Ks arbitrary: Us) case Nil thus ?case by auto next case (Cons k Ks) then obtain u Us' where Us: "Us = u # Us'" by (metis length_Suc_conv) hence u: "u ∈ carrier R" and Us': "set Us' ⊆ carrier R" using Cons(4) by auto then show ?case using combine_in_carrier[OF _ Us', of Ks] Cons combine_in_carrier[OF Cons(5-6)] unfolding Us by (auto, simp add: add.m_assoc) qed lemma combine_add: assumes "length Ks = length Us" and "length Ks' = length Us" and "set Ks ⊆ carrier R" "set Ks' ⊆ carrier R" "set Us ⊆ carrier R" shows "(combine Ks Us) ⊕ (combine Ks' Us) = combine (map2 (⊕) Ks Ks') Us" using assms proof (induct Us arbitrary: Ks Ks') case Nil thus ?case by simp next case (Cons u Us) then obtain c c' Cs Cs' where Ks: "Ks = c # Cs" and Ks': "Ks' = c' # Cs'" by (metis length_Suc_conv) hence in_carrier: "c ∈ carrier R" "set Cs ⊆ carrier R" "c' ∈ carrier R" "set Cs' ⊆ carrier R" "u ∈ carrier R" "set Us ⊆ carrier R" using Cons(4-6) by auto hence lc_in_carrier: "combine Cs Us ∈ carrier R" "combine Cs' Us ∈ carrier R" using combine_in_carrier by auto have "combine Ks (u # Us) ⊕ combine Ks' (u # Us) = ((c ⊗ u) ⊕ combine Cs Us) ⊕ ((c' ⊗ u) ⊕ combine Cs' Us)" unfolding Ks Ks' by auto also have " ... = ((c ⊕ c') ⊗ u ⊕ (combine Cs Us ⊕ combine Cs' Us))" using lc_in_carrier in_carrier(1,3,5) by (simp add: l_distr ring_simprules(7,22)) also have " ... = combine (map2 (⊕) Ks Ks') (u # Us)" using Cons unfolding Ks Ks' by auto finally show ?case . qed lemma combine_normalize: assumes "set Ks ⊆ carrier R" "set Us ⊆ carrier R" "combine Ks Us = a" obtains Ks' where "set (take (length Us) Ks) ⊆ set Ks'" "set Ks' ⊆ set (take (length Us) Ks) ∪ { 𝟬 }" and "length Ks' = length Us" "combine Ks' Us = a" proof - define Ks' where "Ks' = (if length Ks ≤ length Us then Ks @ (replicate (length Us - length Ks) 𝟬) else take (length Us) Ks)" hence "set (take (length Us) Ks) ⊆ set Ks'" "set Ks' ⊆ set (take (length Us) Ks) ∪ { 𝟬 }" "length Ks' = length Us" "a = combine Ks' Us" using combine_append_replicate[OF assms(2)] combine_take assms(3) by auto thus thesis using that by blast qed lemma line_extension_mem_iff: "u ∈ line_extension K a E ⟷ (∃k ∈ K. ∃v ∈ E. u = k ⊗ a ⊕ v)" unfolding line_extension_def set_add_def'[of R "K #> a" E] unfolding r_coset_def by blast lemma line_extension_in_carrier: assumes "K ⊆ carrier R" "a ∈ carrier R" "E ⊆ carrier R" shows "line_extension K a E ⊆ carrier R" using set_add_closed[OF r_coset_subset_G[OF assms(1-2)] assms(3)] by (simp add: line_extension_def) lemma Span_in_carrier: assumes "K ⊆ carrier R" "set Us ⊆ carrier R" shows "Span K Us ⊆ carrier R" using assms by (induct Us) (auto simp add: line_extension_in_carrier) subsection ‹Some Basic Properties of Linear Independence› lemma independent_in_carrier: "independent K Us ⟹ set Us ⊆ carrier R" by (induct Us rule: independent.induct) (simp_all) lemma independent_backwards: "independent K (u # Us) ⟹ u ∉ Span K Us" "independent K (u # Us) ⟹ independent K Us" "independent K (u # Us) ⟹ u ∈ carrier R" by (cases rule: independent.cases, auto)+ lemma dimension_independent [intro]: "independent K Us ⟹ dimension (length Us) K (Span K Us)" proof (induct Us) case Nil thus ?case by simp next case Cons thus ?case using Suc_dim independent_backwards[OF Cons(2)] by auto qed text ‹Now, we fix K, a subfield of the ring. Many lemmas would also be true for weaker structures, but our interest is to work with subfields, so generalization could be the subject of a future work.› context fixes K :: "'a set" assumes K: "subfield K R" begin subsection ‹Basic Properties - Second Part› lemmas subring_props [simp] = subringE[OF subfieldE(1)[OF K]] lemma line_extension_is_subgroup: assumes "subgroup E (add_monoid R)" "a ∈ carrier R" shows "subgroup (line_extension K a E) (add_monoid R)" proof (rule add.subgroupI) show "line_extension K a E ⊆ carrier R" by (simp add: assms add.subgroupE(1) line_extension_def r_coset_subset_G set_add_closed) next have "𝟬 = 𝟬 ⊗ a ⊕ 𝟬" using assms(2) by simp hence "𝟬 ∈ line_extension K a E" using line_extension_mem_iff subgroup.one_closed[OF assms(1)] by auto thus "line_extension K a E ≠ {}" by auto next fix u1 u2 assume "u1 ∈ line_extension K a E" and "u2 ∈ line_extension K a E" then obtain k1 k2 v1 v2 where u1: "k1 ∈ K" "v1 ∈ E" "u1 = (k1 ⊗ a) ⊕ v1" and u2: "k2 ∈ K" "v2 ∈ E" "u2 = (k2 ⊗ a) ⊕ v2" and in_carr: "k1 ∈ carrier R" "v1 ∈ carrier R" "k2 ∈ carrier R" "v2 ∈ carrier R" using line_extension_mem_iff by (meson add.subgroupE(1)[OF assms(1)] subring_props(1) subsetCE) hence "u1 ⊕ u2 = ((k1 ⊕ k2) ⊗ a) ⊕ (v1 ⊕ v2)" using assms(2) by algebra moreover have "k1 ⊕ k2 ∈ K" and "v1 ⊕ v2 ∈ E" using add.subgroupE(4)[OF assms(1)] u1 u2 by auto ultimately show "u1 ⊕ u2 ∈ line_extension K a E" using line_extension_mem_iff by auto have "⊖ u1 = ((⊖ k1) ⊗ a) ⊕ (⊖ v1)" using in_carr(1-2) u1(3) assms(2) by algebra moreover have "⊖ k1 ∈ K" and "⊖ v1 ∈ E" using add.subgroupE(3)[OF assms(1)] u1 by auto ultimately show "(⊖ u1) ∈ line_extension K a E" using line_extension_mem_iff by auto qed corollary Span_is_add_subgroup: "set Us ⊆ carrier R ⟹ subgroup (Span K Us) (add_monoid R)" using line_extension_is_subgroup normal_imp_subgroup[OF add.one_is_normal] by (induct Us) (auto) lemma line_extension_smult_closed: assumes "⋀k v. ⟦ k ∈ K; v ∈ E ⟧ ⟹ k ⊗ v ∈ E" and "E ⊆ carrier R" "a ∈ carrier R" shows "⋀k u. ⟦ k ∈ K; u ∈ line_extension K a E ⟧ ⟹ k ⊗ u ∈ line_extension K a E" proof - fix k u assume A: "k ∈ K" "u ∈ line_extension K a E" then obtain k' v' where u: "k' ∈ K" "v' ∈ E" "u = k' ⊗ a ⊕ v'" and in_carr: "k ∈ carrier R" "k' ∈ carrier R" "v' ∈ carrier R" using line_extension_mem_iff assms(2) by (meson subring_props(1) subsetCE) hence "k ⊗ u = (k ⊗ k') ⊗ a ⊕ (k ⊗ v')" using assms(3) by algebra thus "k ⊗ u ∈ line_extension K a E" using assms(1)[OF A(1) u(2)] line_extension_mem_iff u(1) A(1) by auto qed lemma Span_subgroup_props [simp]: assumes "set Us ⊆ carrier R" shows "Span K Us ⊆ carrier R" and "𝟬 ∈ Span K Us" and "⋀v1 v2. ⟦ v1 ∈ Span K Us; v2 ∈ Span K Us ⟧ ⟹ (v1 ⊕ v2) ∈ Span K Us" and "⋀v. v ∈ Span K Us ⟹ (⊖ v) ∈ Span K Us" using add.subgroupE subgroup.one_closed[of _ "add_monoid R"] Span_is_add_subgroup[OF assms(1)] by auto lemma Span_smult_closed [simp]: assumes "set Us ⊆ carrier R" shows "⋀k v. ⟦ k ∈ K; v ∈ Span K Us ⟧ ⟹ k ⊗ v ∈ Span K Us" using assms proof (induct Us) case Nil thus ?case using r_null subring_props(1) by (auto, blast) next case Cons thus ?case using Span_subgroup_props(1) line_extension_smult_closed by auto qed lemma Span_m_inv_simprule [simp]: assumes "set Us ⊆ carrier R" shows "⟦ k ∈ K - { 𝟬 }; a ∈ carrier R ⟧ ⟹ k ⊗ a ∈ Span K Us ⟹ a ∈ Span K Us" proof - assume k: "k ∈ K - { 𝟬 }" and a: "a ∈ carrier R" and ka: "k ⊗ a ∈ Span K Us" have inv_k: "inv k ∈ K" "inv k ⊗ k = 𝟭" using subfield_m_inv[OF K k] by simp+ hence "inv k ⊗ (k ⊗ a) ∈ Span K Us" using Span_smult_closed[OF assms _ ka] by simp thus ?thesis using inv_k subring_props(1)a k by (metis (no_types, lifting) DiffE l_one m_assoc subset_iff) qed subsection ‹Span as Linear Combinations› text ‹We show that Span is the set of linear combinations› lemma line_extension_of_combine_set: assumes "u ∈ carrier R" shows "line_extension K u { combine Ks Us | Ks. set Ks ⊆ K } = { combine Ks (u # Us) | Ks. set Ks ⊆ K }" (is "?line_extension = ?combinations") proof show "?line_extension ⊆ ?combinations" proof fix v assume "v ∈ ?line_extension" then obtain k Ks where "k ∈ K" "set Ks ⊆ K" and "v = combine (k # Ks) (u # Us)" using line_extension_mem_iff by auto thus "v ∈ ?combinations" by (metis (mono_tags, lifting) insert_subset list.simps(15) mem_Collect_eq) qed next show "?combinations ⊆ ?line_extension" proof fix v assume "v ∈ ?combinations" then obtain Ks where v: "set Ks ⊆ K" "v = combine Ks (u # Us)" by auto thus "v ∈ ?line_extension" proof (cases Ks) case Cons thus ?thesis using v line_extension_mem_iff by auto next case Nil hence "v = 𝟬" using v by simp moreover have "combine [] Us = 𝟬" by simp hence "𝟬 ∈ { combine Ks Us | Ks. set Ks ⊆ K }" by (metis (mono_tags, lifting) local.Nil mem_Collect_eq v(1)) hence "(𝟬 ⊗ u) ⊕ 𝟬 ∈ ?line_extension" using line_extension_mem_iff subring_props(2) by blast hence "𝟬 ∈ ?line_extension" using assms by auto ultimately show ?thesis by auto qed qed qed lemma Span_eq_combine_set: assumes "set Us ⊆ carrier R" shows "Span K Us = { combine Ks Us | Ks. set Ks ⊆ K }" using assms line_extension_of_combine_set by (induct Us) (auto, metis empty_set empty_subsetI) lemma line_extension_of_combine_set_length_version: assumes "u ∈ carrier R" shows "line_extension K u { combine Ks Us | Ks. length Ks = length Us ∧ set Ks ⊆ K } = { combine Ks (u # Us) | Ks. length Ks = length (u # Us) ∧ set Ks ⊆ K }" (is "?line_extension = ?combinations") proof show "?line_extension ⊆ ?combinations" proof fix v assume "v ∈ ?line_extension" then obtain k Ks where "v = combine (k # Ks) (u # Us)" "length (k # Ks) = length (u # Us)" "set (k # Ks) ⊆ K" using line_extension_mem_iff by auto thus "v ∈ ?combinations" by blast qed next show "?combinations ⊆ ?line_extension" proof fix c assume "c ∈ ?combinations" then obtain Ks where c: "c = combine Ks (u # Us)" "length Ks = length (u # Us)" "set Ks ⊆ K" by blast then obtain k Ks' where k: "Ks = k # Ks'" by (metis length_Suc_conv) thus "c ∈ ?line_extension" using c line_extension_mem_iff unfolding k by auto qed qed lemma Span_eq_combine_set_length_version: assumes "set Us ⊆ carrier R" shows "Span K Us = { combine Ks Us | Ks. length Ks = length Us ∧ set Ks ⊆ K }" using assms line_extension_of_combine_set_length_version by (induct Us) (auto) subsubsection ‹Corollaries› corollary Span_mem_iff_length_version: assumes "set Us ⊆ carrier R" shows "a ∈ Span K Us ⟷ (∃Ks. set Ks ⊆ K ∧ length Ks = length Us ∧ a = combine Ks Us)" using Span_eq_combine_set_length_version[OF assms] by blast corollary Span_mem_imp_non_trivial_combine: assumes "set Us ⊆ carrier R" and "a ∈ Span K Us" obtains k Ks where "k ∈ K - { 𝟬 }" "set Ks ⊆ K" "length Ks = length Us" "combine (k # Ks) (a # Us) = 𝟬" proof - obtain Ks where Ks: "set Ks ⊆ K" "length Ks = length Us" "a = combine Ks Us" using Span_mem_iff_length_version[OF assms(1)] assms(2) by auto hence "((⊖ 𝟭) ⊗ a) ⊕ a = combine ((⊖ 𝟭) # Ks) (a # Us)" by auto moreover have "((⊖ 𝟭) ⊗ a) ⊕ a = 𝟬" using assms(2) Span_subgroup_props(1)[OF assms(1)] l_minus l_neg by auto moreover have "⊖ 𝟭 ≠ 𝟬" using subfieldE(6)[OF K] l_neg by force ultimately show ?thesis using that subring_props(3,5) Ks(1-2) by (force simp del: combine.simps) qed corollary Span_mem_iff: assumes "set Us ⊆ carrier R" and "a ∈ carrier R" shows "a ∈ Span K Us ⟷ (∃k ∈ K - { 𝟬 }. ∃Ks. set Ks ⊆ K ∧ combine (k # Ks) (a # Us) = 𝟬)" (is "?in_Span ⟷ ?exists_combine") proof assume "?in_Span" then obtain Ks where Ks: "set Ks ⊆ K" "a = combine Ks Us" using Span_eq_combine_set[OF assms(1)] by auto hence "((⊖ 𝟭) ⊗ a) ⊕ a = combine ((⊖ 𝟭) # Ks) (a # Us)" by auto moreover have "((⊖ 𝟭) ⊗ a) ⊕ a = 𝟬" using assms(2) l_minus l_neg by auto moreover have "⊖ 𝟭 ≠ 𝟬" using subfieldE(6)[OF K] l_neg by force ultimately show "?exists_combine" using subring_props(3,5) Ks(1) by (force simp del: combine.simps) next assume "?exists_combine" then obtain k Ks where k: "k ∈ K" "k ≠ 𝟬" and Ks: "set Ks ⊆ K" and a: "(k ⊗ a) ⊕ combine Ks Us = 𝟬" by auto hence "combine Ks Us ∈ Span K Us" using Span_eq_combine_set[OF assms(1)] by auto hence "k ⊗ a ∈ Span K Us" using Span_subgroup_props[OF assms(1)] k Ks a by (metis (no_types, lifting) assms(2) contra_subsetD m_closed minus_equality subring_props(1)) thus "?in_Span" using Span_m_inv_simprule[OF assms(1) _ assms(2), of k] k by auto qed subsection ‹Span as the minimal subgroup that contains \<^term>‹K <#> (set Us)›› text ‹Now we show the link between Span and Group.generate› lemma mono_Span: assumes "set Us ⊆ carrier R" and "u ∈ carrier R" shows "Span K Us ⊆ Span K (u # Us)" proof fix v assume v: "v ∈ Span K Us" hence "(𝟬 ⊗ u) ⊕ v ∈ Span K (u # Us)" using line_extension_mem_iff by auto thus "v ∈ Span K (u # Us)" using Span_subgroup_props(1)[OF assms(1)] assms(2) v by (auto simp del: Span.simps) qed lemma Span_min: assumes "set Us ⊆ carrier R" and "subgroup E (add_monoid R)" shows "K <#> (set Us) ⊆ E ⟹ Span K Us ⊆ E" proof - assume "K <#> (set Us) ⊆ E" show "Span K Us ⊆ E" proof fix v assume "v ∈ Span K Us" then obtain Ks where v: "set Ks ⊆ K" "v = combine Ks Us" using Span_eq_combine_set[OF assms(1)] by auto from ‹set Ks ⊆ K› ‹set Us ⊆ carrier R› and ‹K <#> (set Us) ⊆ E› show "v ∈ E" unfolding v(2) proof (induct Ks Us rule: combine.induct) case (1 k Ks u Us) hence "k ∈ K" and "u ∈ set (u # Us)" by auto hence "k ⊗ u ∈ E" using 1(4) unfolding set_mult_def by auto moreover have "K <#> set Us ⊆ E" using 1(4) unfolding set_mult_def by auto hence "combine Ks Us ∈ E" using 1 by auto ultimately show ?case using add.subgroupE(4)[OF assms(2)] by auto next case "2_1" thus ?case using subgroup.one_closed[OF assms(2)] by auto next case "2_2" thus ?case using subgroup.one_closed[OF assms(2)] by auto qed qed qed lemma Span_eq_generate: assumes "set Us ⊆ carrier R" shows "Span K Us = generate (add_monoid R) (K <#> (set Us))" proof (rule add.generateI) show "subgroup (Span K Us) (add_monoid R)" using Span_is_add_subgroup[OF assms] . next show "⋀E. ⟦ subgroup E (add_monoid R); K <#> set Us ⊆ E ⟧ ⟹ Span K Us ⊆ E" using Span_min assms by blast next show "K <#> set Us ⊆ Span K Us" using assms proof (induct Us) case Nil thus ?case unfolding set_mult_def by auto next case (Cons u Us) have "K <#> set (u # Us) = (K <#> { u }) ∪ (K <#> set Us)" unfolding set_mult_def by auto moreover have "⋀k. k ∈ K ⟹ k ⊗ u ∈ Span K (u # Us)" proof - fix k assume k: "k ∈ K" hence "combine [ k ] (u # Us) ∈ Span K (u # Us)" using Span_eq_combine_set[OF Cons(2)] by (auto simp del: combine.simps) moreover have "k ∈ carrier R" and "u ∈ carrier R" using Cons(2) k subring_props(1) by (blast, auto) ultimately show "k ⊗ u ∈ Span K (u # Us)" by (auto simp del: Span.simps) qed hence "K <#> { u } ⊆ Span K (u # Us)" unfolding set_mult_def by auto moreover have "K <#> set Us ⊆ Span K (u # Us)" using mono_Span[of Us u] Cons by (auto simp del: Span.simps) ultimately show ?case using Cons by (auto simp del: Span.simps) qed qed subsubsection ‹Corollaries› corollary Span_same_set: assumes "set Us ⊆ carrier R" shows "set Us = set Vs ⟹ Span K Us = Span K Vs" using Span_eq_generate assms by auto corollary Span_incl: "set Us ⊆ carrier R ⟹ K <#> (set Us) ⊆ Span K Us" using Span_eq_generate generate.incl[of _ _ "add_monoid R"] by auto corollary Span_base_incl: "set Us ⊆ carrier R ⟹ set Us ⊆ Span K Us" proof - assume A: "set Us ⊆ carrier R" hence "{ 𝟭 } <#> set Us = set Us" unfolding set_mult_def by force moreover have "{ 𝟭 } <#> set Us ⊆ K <#> set Us" using subring_props(3) unfolding set_mult_def by blast ultimately show ?thesis using Span_incl[OF A] by auto qed corollary mono_Span_sublist: assumes "set Us ⊆ set Vs" "set Vs ⊆ carrier R" shows "Span K Us ⊆ Span K Vs" using add.mono_generate[OF mono_set_mult[OF _ assms(1), of K K R]] Span_eq_generate[OF assms(2)] Span_eq_generate[of Us] assms by auto corollary mono_Span_append: assumes "set Us ⊆ carrier R" "set Vs ⊆ carrier R" shows "Span K Us ⊆ Span K (Us @ Vs)" and "Span K Us ⊆ Span K (Vs @ Us)" using mono_Span_sublist[of Us "Us @ Vs"] assms Span_same_set[of "Us @ Vs" "Vs @ Us"] by auto corollary mono_Span_subset: assumes "set Us ⊆ Span K Vs" "set Vs ⊆ carrier R" shows "Span K Us ⊆ Span K Vs" proof (rule Span_min[OF _ Span_is_add_subgroup[OF assms(2)]]) show "set Us ⊆ carrier R" using Span_subgroup_props(1)[OF assms(2)] assms by auto show "K <#> set Us ⊆ Span K Vs" using Span_smult_closed[OF assms(2)] assms(1) unfolding set_mult_def by blast qed lemma Span_strict_incl: assumes "set Us ⊆ carrier R" "set Vs ⊆ carrier R" shows "Span K Us ⊂ Span K Vs ⟹ (∃v ∈ set Vs. v ∉ Span K Us)" proof - assume "Span K Us ⊂ Span K Vs" show "∃v ∈ set Vs. v ∉ Span K Us" proof (rule ccontr) assume "¬ (∃v ∈ set Vs. v ∉ Span K Us)" hence "Span K Vs ⊆ Span K Us" using mono_Span_subset[OF _ assms(1), of Vs] by auto from ‹Span K Us ⊂ Span K Vs› and ‹Span K Vs ⊆ Span K Us› show False by simp qed qed lemma Span_append_eq_set_add: assumes "set Us ⊆ carrier R" and "set Vs ⊆ carrier R" shows "Span K (Us @ Vs) = (Span K Us <+>⇘R⇙ Span K Vs)" using assms proof (induct Us) case Nil thus ?case using Span_subgroup_props(1)[OF Nil(2)] unfolding set_add_def' by force next case (Cons u Us) hence in_carrier: "u ∈ carrier R" "set Us ⊆ carrier R" "set Vs ⊆ carrier R" by auto have "line_extension K u (Span K Us <+>⇘R⇙ Span K Vs) = (Span K (u # Us) <+>⇘R⇙ Span K Vs)" proof show "line_extension K u (Span K Us <+>⇘R⇙ Span K Vs) ⊆ (Span K (u # Us) <+>⇘R⇙ Span K Vs)" proof fix v assume "v ∈ line_extension K u (Span K Us <+>⇘R⇙ Span K Vs)" then obtain k u' v' where v: "k ∈ K" "u' ∈ Span K Us" "v' ∈ Span K Vs" "v = k ⊗ u ⊕ (u' ⊕ v')" using line_extension_mem_iff[of v _ u "Span K Us <+>⇘R⇙ Span K Vs"] unfolding set_add_def' by blast hence "v = (k ⊗ u ⊕ u') ⊕ v'" using in_carrier(2-3)[THEN Span_subgroup_props(1)] in_carrier(1) subring_props(1) by (metis (no_types, lifting) rev_subsetD ring_simprules(7) semiring_simprules(3)) moreover have "k ⊗ u ⊕ u' ∈ Span K (u # Us)" using line_extension_mem_iff v(1-2) by auto ultimately show "v ∈ Span K (u # Us) <+>⇘R⇙ Span K Vs" unfolding set_add_def' using v(3) by auto qed next show "Span K (u # Us) <+>⇘R⇙ Span K Vs ⊆ line_extension K u (Span K Us <+>⇘R⇙ Span K Vs)" proof fix v assume "v ∈ Span K (u # Us) <+>⇘R⇙ Span K Vs" then obtain k u' v' where v: "k ∈ K" "u' ∈ Span K Us" "v' ∈ Span K Vs" "v = (k ⊗ u ⊕ u') ⊕ v'" using line_extension_mem_iff[of _ _ u "Span K Us"] unfolding set_add_def' by auto hence "v = (k ⊗ u) ⊕ (u' ⊕ v')" using in_carrier(2-3)[THEN Span_subgroup_props(1)] in_carrier(1) subring_props(1) by (metis (no_types, lifting) rev_subsetD ring_simprules(5,7)) thus "v ∈ line_extension K u (Span K Us <+>⇘R⇙ Span K Vs)" using line_extension_mem_iff[of "(k ⊗ u) ⊕ (u' ⊕ v')" K u "Span K Us <+>⇘R⇙ Span K Vs"] unfolding set_add_def' using v by auto qed qed thus ?case using Cons by auto qed subsection ‹Characterisation of Linearly Independent "Sets"› declare independent_backwards [intro] declare independent_in_carrier [intro] lemma independent_distinct: "independent K Us ⟹ distinct Us" proof (induct Us rule: list.induct) case Nil thus ?case by simp next case Cons thus ?case using independent_backwards[OF Cons(2)] independent_in_carrier[OF Cons(2)] Span_base_incl by auto qed lemma independent_strict_incl: assumes "independent K (u # Us)" shows "Span K Us ⊂ Span K (u # Us)" proof - have "u ∈ Span K (u # Us)" using Span_base_incl[OF independent_in_carrier[OF assms]] by auto moreover have "Span K Us ⊆ Span K (u # Us)" using mono_Span independent_in_carrier[OF assms] by auto ultimately show ?thesis using independent_backwards(1)[OF assms] by auto qed corollary independent_replacement: assumes "independent K (u # Us)" and "independent K Vs" shows "Span K (u # Us) ⊆ Span K Vs ⟹ (∃v ∈ set Vs. independent K (v # Us))" proof - assume "Span K (u # Us) ⊆ Span K Vs" hence "Span K Us ⊂ Span K Vs" using independent_strict_incl[OF assms(1)] by auto then obtain v where v: "v ∈ set Vs" "v ∉ Span K Us" using Span_strict_incl[of Us Vs] assms[THEN independent_in_carrier] by auto thus ?thesis using li_Cons[of v K Us] assms independent_in_carrier[OF assms(2)] by auto qed lemma independent_split: assumes "independent K (Us @ Vs)" shows "independent K Vs" and "independent K Us" and "Span K Us ∩ Span K Vs = { 𝟬 }" proof - from assms show "independent K Vs" by (induct Us) (auto) next from assms show "independent K Us" proof (induct Us) case Nil thus ?case by simp next case (Cons u Us') hence u: "u ∈ carrier R" and "set Us' ⊆ carrier R" "set Vs ⊆ carrier R" using independent_in_carrier[of K "(u # Us') @ Vs"] by auto hence "Span K Us' ⊆ Span K (Us' @ Vs)" using mono_Span_append(1) by simp thus ?case using independent_backwards[of K u "Us' @ Vs"] Cons li_Cons[OF u] by auto qed next from assms show "Span K Us ∩ Span K Vs = { 𝟬 }" proof (induct Us rule: list.induct) case Nil thus ?case using Span_subgroup_props(2)[OF independent_in_carrier[of K Vs]] by simp next case (Cons u Us) hence IH: "Span K Us ∩ Span K Vs = {𝟬}" by auto have in_carrier: "u ∈ carrier R" "set Us ⊆ carrier R" "set Vs ⊆ carrier R" "set (u # Us) ⊆ carrier R" using Cons(2)[THEN independent_in_carrier] by auto hence "{ 𝟬 } ⊆ Span K (u # Us) ∩ Span K Vs" using in_carrier(3-4)[THEN Span_subgroup_props(2)] by auto moreover have "Span K (u # Us) ∩ Span K Vs ⊆ { 𝟬 }" proof (rule ccontr) assume "¬ Span K (u # Us) ∩ Span K Vs ⊆ {𝟬}" hence "∃a. a ≠ 𝟬 ∧ a ∈ Span K (u # Us) ∧ a ∈ Span K Vs" by auto then obtain k u' v' where u': "u' ∈ Span K Us" "u' ∈ carrier R" and v': "v' ∈ Span K Vs" "v' ∈ carrier R" "v' ≠ 𝟬" and k: "k ∈ K" "(k ⊗ u ⊕ u') = v'" using line_extension_mem_iff[of _ _ u "Span K Us"] in_carrier(2-3)[THEN Span_subgroup_props(1)] subring_props(1) by force hence "v' = 𝟬" if "k = 𝟬" using in_carrier(1) that IH by auto hence diff_zero: "k ≠ 𝟬" using v'(3) by auto have "k ∈ carrier R" using subring_props(1) k(1) by blast hence "k ⊗ u = (⊖ u') ⊕ v'" using in_carrier(1) k(2) u'(2) v'(2) add.m_comm r_neg1 by auto hence "k ⊗ u ∈ Span K (Us @ Vs)" using Span_subgroup_props(4)[OF in_carrier(2) u'(1)] v'(1) Span_append_eq_set_add[OF in_carrier(2-3)] unfolding set_add_def' by blast hence "u ∈ Span K (Us @ Vs)" using Cons(2) Span_m_inv_simprule[OF _ _ in_carrier(1), of "Us @ Vs" k] diff_zero k(1) in_carrier(2-3) by auto moreover have "u ∉ Span K (Us @ Vs)" using independent_backwards(1)[of K u "Us @ Vs"] Cons(2) by auto ultimately show False by simp qed ultimately show ?case by auto qed qed lemma independent_append: assumes "independent K Us" and "independent K Vs" and "Span K Us ∩ Span K Vs = { 𝟬 }" shows "independent K (Us @ Vs)" using assms proof (induct Us rule: list.induct) case Nil thus ?case by simp next case (Cons u Us) hence in_carrier: "u ∈ carrier R" "set Us ⊆ carrier R" "set Vs ⊆ carrier R" "set (u # Us) ⊆ carrier R" using Cons(2-3)[THEN independent_in_carrier] by auto hence "Span K Us ⊆ Span K (u # Us)" using mono_Span by auto hence "Span K Us ∩ Span K Vs = { 𝟬 }" using Cons(4) Span_subgroup_props(2)[OF in_carrier(2)] by auto hence "independent K (Us @ Vs)" using Cons by auto moreover have "u ∉ Span K (Us @ Vs)" proof (rule ccontr) assume "¬ u ∉ Span K (Us @ Vs)" then obtain u' v' where u': "u' ∈ Span K Us" "u' ∈ carrier R" and v': "v' ∈ Span K Vs" "v' ∈ carrier R" and u:"u = u' ⊕ v'" using Span_append_eq_set_add[OF in_carrier(2-3)] in_carrier(2-3)[THEN Span_subgroup_props(1)] unfolding set_add_def' by blast hence "u ⊕ (⊖ u') = v'" using in_carrier(1) by algebra moreover have "u ∈ Span K (u # Us)" and "u' ∈ Span K (u # Us)" using Span_base_incl[OF in_carrier(4)] mono_Span[OF in_carrier(2,1)] u'(1) by (auto simp del: Span.simps) hence "u ⊕ (⊖ u') ∈ Span K (u # Us)" using Span_subgroup_props(3-4)[OF in_carrier(4)] by (auto simp del: Span.simps) ultimately have "u ⊕ (⊖ u') = 𝟬" using Cons(4) v'(1) by auto hence "u = u'" using Cons(4) v'(1) in_carrier(1) u'(2) ‹u ⊕ ⊖ u' = v'› u by auto thus False using u'(1) independent_backwards(1)[OF Cons(2)] by simp qed ultimately show ?case using in_carrier(1) li_Cons by simp qed lemma independent_imp_trivial_combine: assumes "independent K Us" shows "⋀Ks. ⟦ set Ks ⊆ K; combine Ks Us = 𝟬 ⟧ ⟹ set (take (length Us) Ks) ⊆ { 𝟬 }" using assms proof (induct Us rule: list.induct) case Nil thus ?case by simp next case (Cons u Us) thus ?case proof (cases "Ks = []") assume "Ks = []" thus ?thesis by auto next assume "Ks ≠ []" then obtain k Ks' where k: "k ∈ K" and Ks': "set Ks' ⊆ K" and Ks: "Ks = k # Ks'" using Cons(2) by (metis insert_subset list.exhaust_sel list.simps(15)) hence Us: "set Us ⊆ carrier R" and u: "u ∈ carrier R" using independent_in_carrier[OF Cons(4)] by auto have "u ∈ Span K Us" if "k ≠ 𝟬" using that Span_mem_iff[OF Us u] Cons(3-4) Ks' k unfolding Ks by blast hence k_zero: "k = 𝟬" using independent_backwards[OF Cons(4)] by blast hence "combine Ks' Us = 𝟬" using combine_in_carrier[OF _ Us, of Ks'] Ks' u Cons(3) subring_props(1) unfolding Ks by auto hence "set (take (length Us) Ks') ⊆ { 𝟬 }" using Cons(1)[OF Ks' _ independent_backwards(2)[OF Cons(4)]] by simp thus ?thesis using k_zero unfolding Ks by auto qed qed lemma non_trivial_combine_imp_dependent: assumes "set Ks ⊆ K" and "combine Ks Us = 𝟬" and "¬ set (take (length Us) Ks) ⊆ { 𝟬 }" shows "dependent K Us" using independent_imp_trivial_combine[OF _ assms(1-2)] assms(3) by blast lemma trivial_combine_imp_independent: assumes "set Us ⊆ carrier R" and "⋀Ks. ⟦ set Ks ⊆ K; combine Ks Us = 𝟬 ⟧ ⟹ set (take (length Us) Ks) ⊆ { 𝟬 }" shows "independent K Us" using assms proof (induct Us) case Nil thus ?case by simp next case (Cons u Us) hence Us: "set Us ⊆ carrier R" and u: "u ∈ carrier R" by auto have "⋀Ks. ⟦ set Ks ⊆ K; combine Ks Us = 𝟬 ⟧ ⟹ set (take (length Us) Ks) ⊆ { 𝟬 }" proof - fix Ks assume Ks: "set Ks ⊆ K" and lin_c: "combine Ks Us = 𝟬" hence "combine (𝟬 # Ks) (u # Us) = 𝟬" using u subring_props(1) combine_in_carrier[OF _ Us] by auto hence "set (take (length (u # Us)) (𝟬 # Ks)) ⊆ { 𝟬 }" using Cons(3)[of "𝟬 # Ks"] subring_props(2) Ks by auto thus "set (take (length Us) Ks) ⊆ { 𝟬 }" by auto qed hence "independent K Us" using Cons(1)[OF Us] by simp moreover have "u ∉ Span K Us" proof (rule ccontr) assume "¬ u ∉ Span K Us" then obtain k Ks where k: "k ∈ K" "k ≠ 𝟬" and Ks: "set Ks ⊆ K" and u: "combine (k # Ks) (u # Us) = 𝟬" using Span_mem_iff[OF Us u] by auto have "set (take (length (u # Us)) (k # Ks)) ⊆ { 𝟬 }" using Cons(3)[OF _ u] k(1) Ks by auto hence "k = 𝟬" by auto from ‹k = 𝟬› and ‹k ≠ 𝟬› show False by simp qed ultimately show ?case using li_Cons[OF u] by simp qed corollary dependent_imp_non_trivial_combine: assumes "set Us ⊆ carrier R" and "dependent K Us" obtains Ks where "length Ks = length Us" "combine Ks Us = 𝟬" "set Ks ⊆ K" "set Ks ≠ { 𝟬 }" proof - obtain Ks where Ks: "set Ks ⊆ carrier R" "set Ks ⊆ K" "combine Ks Us = 𝟬" "¬ set (take (length Us) Ks) ⊆ { 𝟬 }" using trivial_combine_imp_independent[OF assms(1)] assms(2) subring_props(1) by blast obtain Ks' where Ks': "set (take (length Us) Ks) ⊆ set Ks'" "set Ks' ⊆ set (take (length Us) Ks) ∪ { 𝟬 }" "length Ks' = length Us" "combine Ks' Us = 𝟬" using combine_normalize[OF Ks(1) assms(1) Ks(3)] by metis have "set (take (length Us) Ks) ⊆ set Ks" by (simp add: set_take_subset) hence "set Ks' ⊆ K" using Ks(2) Ks'(2) subring_props(2) Un_commute by blast moreover have "set Ks' ≠ { 𝟬 }" using Ks'(1) Ks(4) by auto ultimately show thesis using that Ks' by blast qed corollary unique_decomposition: assumes "independent K Us" shows "a ∈ Span K Us ⟹ ∃!Ks. set Ks ⊆ K ∧ length Ks = length Us ∧ a = combine Ks Us" proof - note in_carrier = independent_in_carrier[OF assms] assume "a ∈ Span K Us" then obtain Ks where Ks: "set Ks ⊆ K" "length Ks = length Us" "a = combine Ks Us" using Span_mem_iff_length_version[OF in_carrier] by blast moreover have "⋀Ks'. ⟦ set Ks' ⊆ K; length Ks' = length Us; a = combine Ks' Us ⟧ ⟹ Ks = Ks'" proof - fix Ks' assume Ks': "set Ks' ⊆ K" "length Ks' = length Us" "a = combine Ks' Us" hence set_Ks: "set Ks ⊆ carrier R" and set_Ks': "set Ks' ⊆ carrier R" using subring_props(1) Ks(1) by blast+ have same_length: "length Ks = length Ks'" using Ks Ks' by simp have "(combine Ks Us) ⊕ ((⊖ 𝟭) ⊗ (combine Ks' Us)) = 𝟬" using combine_in_carrier[OF set_Ks in_carrier] combine_in_carrier[OF set_Ks' in_carrier] Ks(3) Ks'(3) by algebra hence "(combine Ks Us) ⊕ (combine (map ((⊗) (⊖ 𝟭)) Ks') Us) = 𝟬" using combine_r_distr[OF set_Ks' in_carrier, of "⊖ 𝟭"] subring_props by auto moreover have set_map: "set (map ((⊗) (⊖ 𝟭)) Ks') ⊆ K" using Ks'(1) subring_props by (induct Ks') (auto) hence "set (map ((⊗) (⊖ 𝟭)) Ks') ⊆ carrier R" using subring_props(1) by blast ultimately have "combine (map2 (⊕) Ks (map ((⊗) (⊖ 𝟭)) Ks')) Us = 𝟬" using combine_add[OF Ks(2) _ set_Ks _ in_carrier, of "map ((⊗) (⊖ 𝟭)) Ks'"] Ks'(2) by auto moreover have "set (map2 (⊕) Ks (map ((⊗) (⊖ 𝟭)) Ks')) ⊆ K" using Ks(1) set_map subring_props(7) by (induct Ks) (auto, metis contra_subsetD in_set_zipE local.set_map set_ConsD subring_props(7)) ultimately have "set (take (length Us) (map2 (⊕) Ks (map ((⊗) (⊖ 𝟭)) Ks'))) ⊆ { 𝟬 }" using independent_imp_trivial_combine[OF assms] by auto hence "set (map2 (⊕) Ks (map ((⊗) (⊖ 𝟭)) Ks')) ⊆ { 𝟬 }" using Ks(2) Ks'(2) by auto thus "Ks = Ks'" using set_Ks set_Ks' same_length proof (induct Ks arbitrary: Ks') case Nil thus?case by simp next case (Cons k Ks) then obtain k' Ks'' where k': "Ks' = k' # Ks''" by (metis Suc_length_conv) have "Ks = Ks''" using Cons unfolding k' by auto moreover have "k = k'" using Cons(2-4) l_minus minus_equality unfolding k' by (auto, fastforce) ultimately show ?case unfolding k' by simp qed qed ultimately show ?thesis by blast qed subsection ‹Replacement Theorem› lemma independent_rotate1_aux: "independent K (u # Us @ Vs) ⟹ independent K ((Us @ [u]) @ Vs)" proof - assume "independent K (u # Us @ Vs)" hence li: "independent K [u]" "independent K Us" "independent K Vs" and inter: "Span K [u] ∩ Span K Us = { 𝟬 }" "Span K (u # Us) ∩ Span K Vs = { 𝟬 }" using independent_split[of "u # Us" Vs] independent_split[of "[u]" Us] by auto hence "independent K (Us @ [u])" using independent_append[OF li(2,1)] by auto moreover have "Span K (Us @ [u]) ∩ Span K Vs = { 𝟬 }" using Span_same_set[of "u # Us" "Us @ [u]"] li(1-2)[THEN independent_in_carrier] inter(2) by auto ultimately show "independent K ((Us @ [u]) @ Vs)" using independent_append[OF _ li(3), of "Us @ [u]"] by simp qed corollary independent_rotate1: "independent K (Us @ Vs) ⟹ independent K ((rotate1 Us) @ Vs)" using independent_rotate1_aux by (cases Us) (auto) (* corollary independent_rotate: "independent K (Us @ Vs) ⟹ independent K ((rotate n Us) @ Vs)" using independent_rotate1 by (induct n) auto lemma rotate_append: "rotate (length l) (l @ q) = q @ l" by (induct l arbitrary: q) (auto simp add: rotate1_rotate_swap) *) corollary independent_same_set: assumes "set Us = set Vs" and "length Us = length Vs" shows "independent K Us ⟹ independent K Vs" proof - assume "independent K Us" thus ?thesis using assms proof (induct Us arbitrary: Vs rule: list.induct) case Nil thus ?case by simp next case (Cons u Us) then obtain Vs' Vs'' where Vs: "Vs = Vs' @ (u # Vs'')" by (metis list.set_intros(1) split_list) have in_carrier: "u ∈ carrier R" "set Us ⊆ carrier R" using independent_in_carrier[OF Cons(2)] by auto have "distinct Vs" using Cons(3-4) independent_distinct[OF Cons(2)] by (metis card_distinct distinct_card) hence "u ∉ set (Vs' @ Vs'')" and "u ∉ set Us" using independent_distinct[OF Cons(2)] unfolding Vs by auto hence set_eq: "set Us = set (Vs' @ Vs'')" and "length (Vs' @ Vs'') = length Us" using Cons(3-4) unfolding Vs by auto hence "independent K (Vs' @ Vs'')" using Cons(1)[OF independent_backwards(2)[OF Cons(2)]] unfolding Vs by simp hence "independent K (u # (Vs' @ Vs''))" using li_Cons Span_same_set[OF _ set_eq] independent_backwards(1)[OF Cons(2)] in_carrier by auto hence "independent K (Vs' @ (u # Vs''))" using independent_rotate1[of "u # Vs'" Vs''] by auto thus ?case unfolding Vs . qed qed lemma replacement_theorem: assumes "independent K (Us' @ Us)" and "independent K Vs" and "Span K (Us' @ Us) ⊆ Span K Vs" shows "∃Vs'. set Vs' ⊆ set Vs ∧ length Vs' = length Us' ∧ independent K (Vs' @ Us)" using assms proof (induct "length Us'" arbitrary: Us' Us) case 0 thus ?case by auto next case (Suc n) then obtain u Us'' where Us'': "Us' = Us'' @ [u]" by (metis list.size(3) nat.simps(3) rev_exhaust) then obtain Vs' where Vs': "set Vs' ⊆ set Vs" "length Vs' = n" "independent K (Vs' @ (u # Us))" using Suc(1)[of Us'' "u # Us"] Suc(2-5) by auto hence li: "independent K ((u # Vs') @ Us)" using independent_same_set[OF _ _ Vs'(3), of "(u # Vs') @ Us"] by auto moreover have in_carrier: "u ∈ carrier R" "set Us ⊆ carrier R" "set Us' ⊆ carrier R" "set Vs ⊆ carrier R" using Suc(3-4)[THEN independent_in_carrier] Us'' by auto moreover have "Span K ((u # Vs') @ Us) ⊆ Span K Vs" proof - have "set Us ⊆ Span K Vs" "u ∈ Span K Vs" using Suc(5) Span_base_incl[of "Us' @ Us"] Us'' in_carrier(2-3) by auto moreover have "set Vs' ⊆ Span K Vs" using Span_base_incl[OF in_carrier(4)] Vs'(1) by auto ultimately have "set ((u # Vs') @ Us) ⊆ Span K Vs" by auto thus ?thesis using mono_Span_subset[OF _ in_carrier(4)] by (simp del: Span.simps) qed ultimately obtain v where "v ∈ set Vs" "independent K ((v # Vs') @ Us)" using independent_replacement[OF _ Suc(4), of u "Vs' @ Us"] by auto thus ?case using Vs'(1-2) Suc(2) by (metis (mono_tags, lifting) insert_subset length_Cons list.simps(15)) qed corollary independent_length_le: assumes "independent K Us" and "independent K Vs" shows "set Us ⊆ Span K Vs ⟹ length Us ≤ length Vs" proof - assume "set Us ⊆ Span K Vs" hence "Span K Us ⊆ Span K Vs" using mono_Span_subset[OF _ independent_in_carrier[OF assms(2)]] by simp then obtain Vs' where Vs': "set Vs' ⊆ set Vs" "length Vs' = length Us" "independent K Vs'" using replacement_theorem[OF _ assms(2), of Us "[]"] assms(1) by auto hence "card (set Vs') ≤ card (set Vs)" by (simp add: card_mono) thus "length Us ≤ length Vs" using independent_distinct assms(2) Vs'(2-3) by (simp add: distinct_card) qed subsection ‹Dimension› lemma exists_base: assumes "dimension n K E" shows "∃Vs. set Vs ⊆ carrier R ∧ independent K Vs ∧ length Vs = n ∧ Span K Vs = E" (is "∃Vs. ?base K Vs E n") using assms proof (induct E rule: dimension.induct) case zero_dim thus ?case by auto next case (Suc_dim v E n K) then obtain Vs where Vs: "set Vs ⊆ carrier R" "independent K Vs" "length Vs = n" "Span K Vs = E" by auto hence "?base K (v # Vs) (line_extension K v E) (Suc n)" using Suc_dim li_Cons by auto thus ?case by blast qed lemma dimension_zero: "dimension 0 K E ⟹ E = { 𝟬 }" proof - assume "dimension 0 K E" then obtain Vs where "length Vs = 0" "Span K Vs = E" using exists_base by blast thus ?thesis by auto qed lemma dimension_one [iff]: "dimension 1 K K" proof - have "K = Span K [ 𝟭 ]" using line_extension_mem_iff[of _ K 𝟭 "{ 𝟬 }"] subfieldE(3)[OF K] by (auto simp add: rev_subsetD) thus ?thesis using dimension.Suc_dim[OF one_closed _ dimension.zero_dim, of K] subfieldE(6)[OF K] by auto qed lemma dimensionI: assumes "independent K Us" "Span K Us = E" shows "dimension (length Us) K E" using dimension_independent[OF assms(1)] assms(2) by simp lemma space_subgroup_props: assumes "dimension n K E" shows "E ⊆ carrier R" and "𝟬 ∈ E" and "⋀v1 v2. ⟦ v1 ∈ E; v2 ∈ E ⟧ ⟹ (v1 ⊕ v2) ∈ E" and "⋀v. v ∈ E ⟹ (⊖ v) ∈ E" and "⋀k v. ⟦ k ∈ K; v ∈ E ⟧ ⟹ k ⊗ v ∈ E" and "⟦ k ∈ K - { 𝟬 }; a ∈ carrier R ⟧ ⟹ k ⊗ a ∈ E ⟹ a ∈ E" using exists_base[OF assms] Span_subgroup_props Span_smult_closed Span_m_inv_simprule by auto lemma independent_length_le_dimension: assumes "dimension n K E" and "independent K Us" "set Us ⊆ E" shows "length Us ≤ n" proof - obtain Vs where Vs: "set Vs ⊆ carrier R" "independent K Vs" "length Vs = n" "Span K Vs = E" using exists_base[OF assms(1)] by auto thus ?thesis using independent_length_le assms(2-3) by auto qed lemma dimension_is_inj: assumes "dimension n K E" and "dimension m K E" shows "n = m" proof - { fix n m assume n: "dimension n K E" and m: "dimension m K E" then obtain Vs where Vs: "set Vs ⊆ carrier R" "independent K Vs" "length Vs = n" "Span K Vs = E" using exists_base by meson hence "n ≤ m" using independent_length_le_dimension[OF m Vs(2)] Span_base_incl[OF Vs(1)] by auto } note aux_lemma = this show ?thesis using aux_lemma[OF assms] aux_lemma[OF assms(2,1)] by simp qed corollary independent_length_eq_dimension: assumes "dimension n K E" and "independent K Us" "set Us ⊆ E" shows "length Us = n ⟷ Span K Us = E" proof assume len: "length Us = n" show "Span K Us = E" proof (rule ccontr) assume "Span K Us ≠ E" hence "Span K Us ⊂ E" using mono_Span_subset[of Us] exists_base[OF assms(1)] assms(3) by blast then obtain v where v: "v ∈ E" "v ∉ Span K Us" using Span_strict_incl exists_base[OF assms(1)] space_subgroup_props(1)[OF assms(1)] assms by blast hence "independent K (v # Us)" using li_Cons[OF _ _ assms(2)] space_subgroup_props(1)[OF assms(1)] by auto hence "length (v # Us) ≤ n" using independent_length_le_dimension[OF assms(1)] v(1) assms(2-3) by fastforce moreover have "length (v # Us) = Suc n" using len by simp ultimately show False by simp qed next assume "Span K Us = E" hence "dimension (length Us) K E" using dimensionI assms by auto thus "length Us = n" using dimension_is_inj[OF assms(1)] by auto qed lemma complete_base: assumes "dimension n K E" and "independent K Us" "set Us ⊆ E" shows "∃Vs. length (Vs @ Us) = n ∧ independent K (Vs @ Us) ∧ Span K (Vs @ Us) = E" proof - { fix Us k assume "k ≤ n" "independent K Us" "set Us ⊆ E" "length Us = k" hence "∃Vs. length (Vs @ Us) = n ∧ independent K (Vs @ Us) ∧ Span K (Vs @ Us) = E" proof (induct arbitrary: Us rule: inc_induct) case base thus ?case using independent_length_eq_dimension[OF assms(1) base(1-2)] by auto next case (step m) have "Span K Us ⊆ E" using mono_Span_subset step(4-6) exists_base[OF assms(1)] by blast hence "Span K Us ⊂ E" using independent_length_eq_dimension[OF assms(1) step(4-5)] step(2,6) assms(1) by blast then obtain v where v: "v ∈ E" "v ∉ Span K Us" using Span_strict_incl exists_base[OF assms(1)] by blast hence "independent K (v # Us)" using space_subgroup_props(1)[OF assms(1)] li_Cons[OF _ v(2) step(4)] by auto then obtain Vs where "length (Vs @ (v # Us)) = n" "independent K (Vs @ (v # Us))" "Span K (Vs @ (v # Us)) = E" using step(3)[of "v # Us"] step(1-2,4-6) v by auto thus ?case by (metis append.assoc append_Cons append_Nil) qed } note aux_lemma = this have "length Us ≤ n" using independent_length_le_dimension[OF assms] . thus ?thesis using aux_lemma[OF _ assms(2-3)] by auto qed lemma filter_base: assumes "set Us ⊆ carrier R" obtains Vs where "set Vs ⊆ carrier R" and "independent K Vs" and "Span K Vs = Span K Us" proof - from ‹set Us ⊆ carrier R› have "∃Vs. independent K Vs ∧ Span K Vs = Span K Us" proof (induction Us) case Nil thus ?case by auto next case (Cons u Us) then obtain Vs where Vs: "independent K Vs" "Span K Vs = Span K Us" by auto show ?case proof (cases "u ∈ Span K Us") case True hence "Span K (u # Us) = Span K Us" using Span_base_incl mono_Span_subset by (metis Cons.prems insert_subset list.simps(15) subset_antisym) thus ?thesis using Vs by blast next case False hence "Span K (u # Vs) = Span K (u # Us)" and "independent K (u # Vs)" using li_Cons[of u K Vs] Cons(2) Vs by auto thus ?thesis by blast qed qed thus ?thesis using independent_in_carrier that by auto qed lemma dimension_backwards: "dimension (Suc n) K E ⟹ ∃v ∈ carrier R. ∃E'. dimension n K E' ∧ v ∉ E' ∧ E = line_extension K v E'" by (cases rule: dimension.cases) (auto) lemma dimension_direct_sum_space: assumes "dimension n K E" and "dimension m K F" and "E ∩ F = { 𝟬 }" shows "dimension (n + m) K (E <+>⇘R⇙ F)" proof - obtain Us Vs where Vs: "set Vs ⊆ carrier R" "independent K Vs" "length Vs = n" "Span K Vs = E" and Us: "set Us ⊆ carrier R" "independent K Us" "length Us = m" "Span K Us = F" using assms(1-2)[THEN exists_base] by auto hence "Span K (Vs @ Us) = E <+>⇘R⇙ F" using Span_append_eq_set_add by auto moreover have "independent K (Vs @ Us)" using assms(3) independent_append[OF Vs(2) Us(2)] unfolding Vs(4) Us(4) by simp ultimately show "dimension (n + m) K (E <+>⇘R⇙ F)" using dimensionI[of "Vs @ Us"] Vs(3) Us(3) by auto qed lemma dimension_sum_space: assumes "dimension n K E" and "dimension m K F" and "dimension k K (E ∩ F)" shows "dimension (n + m - k) K (E <+>⇘R⇙ F)" proof - obtain Bs where Bs: "set Bs ⊆ carrier R" "length Bs = k" "independent K Bs" "Span K Bs = E ∩ F" using exists_base[OF assms(3)] by blast then obtain Us Vs where Us: "length (Us @ Bs) = n" "independent K (Us @ Bs)" "Span K (Us @ Bs) = E" and Vs: "length (Vs @ Bs) = m" "independent K (Vs @ Bs)" "Span K (Vs @ Bs) = F" using Span_base_incl[OF Bs(1)] assms(1-2)[THEN complete_base] by (metis le_infE) hence in_carrier: "set Us ⊆ carrier R" "set (Vs @ Bs) ⊆ carrier R" using independent_in_carrier[OF Us(2)] independent_in_carrier[OF Vs(2)] by auto hence "Span K Us ∩ (Span K (Vs @ Bs)) ⊆ Span K Bs" using Bs(4) Us(3) Vs(3) mono_Span_append(1)[OF _ Bs(1), of Us] by auto hence "Span K Us ∩ (Span K (Vs @ Bs)) ⊆ { 𝟬 }" using independent_split(3)[OF Us(2)] by blast hence "Span K Us ∩ (Span K (Vs @ Bs)) = { 𝟬 }" using in_carrier[THEN Span_subgroup_props(2)] by auto hence dim: "dimension (n + m - k) K (Span K (Us @ (Vs @ Bs)))" using independent_append[OF independent_split(2)[OF Us(2)] Vs(2)] Us(1) Vs(1) Bs(2) dimension_independent[of K "Us @ (Vs @ Bs)"] by auto have "(Span K Us) <+>⇘R⇙ F ⊆ E <+>⇘R⇙ F" using mono_Span_append(1)[OF in_carrier(1) Bs(1)] Us(3) unfolding set_add_def' by auto moreover have "E <+>⇘R⇙ F ⊆ (Span K Us) <+>⇘R⇙ F" proof fix v assume "v ∈ E <+>⇘R⇙ F" then obtain u' v' where v: "u' ∈ E" "v' ∈ F" "v = u' ⊕ v'" unfolding set_add_def' by auto then obtain u1' u2' where u1': "u1' ∈ Span K Us" and u2': "u2' ∈ Span K Bs" and u': "u' = u1' ⊕ u2'" using Span_append_eq_set_add[OF in_carrier(1) Bs(1)] Us(3) unfolding set_add_def' by blast have "v = u1' ⊕ (u2' ⊕ v')" using Span_subgroup_props(1)[OF Bs(1)] Span_subgroup_props(1)[OF in_carrier(1)] space_subgroup_props(1)[OF assms(2)] u' v u1' u2' a_assoc[of u1' u2' v'] by auto moreover have "u2' ⊕ v' ∈ F" using space_subgroup_props(3)[OF assms(2) _ v(2)] u2' Bs(4) by auto ultimately show "v ∈ (Span K Us) <+>⇘R⇙ F" using u1' unfolding set_add_def' by auto qed ultimately have "Span K (Us @ (Vs @ Bs)) = E <+>⇘R⇙ F" using Span_append_eq_set_add[OF in_carrier] Vs(3) by auto thus ?thesis using dim by simp qed end (* of fixed K context. *) end (* of ring context. *) lemma (in ring) telescopic_base_aux: assumes "subfield K R" "subfield F R" and "dimension n K F" and "dimension 1 F E" shows "dimension n K E" proof - obtain Us u where Us: "set Us ⊆ carrier R" "length Us = n" "independent K Us" "Span K Us = F" and u: "u ∈ carrier R" "independent F [u]" "Span F [u] = E" using exists_base[OF assms(2,4)] exists_base[OF assms(1,3)] independent_backwards(3) assms(2) by (metis One_nat_def length_0_conv length_Suc_conv) have in_carrier: "set (map (λu'. u' ⊗ u) Us) ⊆ carrier R" using Us(1) u(1) by (induct Us) (auto) have li: "independent K (map (λu'. u' ⊗ u) Us)" proof (rule trivial_combine_imp_independent[OF assms(1) in_carrier]) fix Ks assume Ks: "set Ks ⊆ K" and "combine Ks (map (λu'. u' ⊗ u) Us) = 𝟬" hence "(combine Ks Us) ⊗ u = 𝟬" using combine_l_distr[OF _ Us(1) u(1)] subring_props(1)[OF assms(1)] by auto hence "combine [ combine Ks Us ] [ u ] = 𝟬" by simp moreover have "combine Ks Us ∈ F" using Us(4) Ks(1) Span_eq_combine_set[OF assms(1) Us(1)] by auto ultimately have "combine Ks Us = 𝟬" using independent_imp_trivial_combine[OF assms(2) u(2), of "[ combine Ks Us ]"] by auto hence "set (take (length Us) Ks) ⊆ { 𝟬 }" using independent_imp_trivial_combine[OF assms(1) Us(3) Ks(1)] by simp thus "set (take (length (map (λu'. u' ⊗ u) Us)) Ks) ⊆ { 𝟬 }" by simp qed have "E ⊆ Span K (map (λu'. u' ⊗ u) Us)" proof fix v assume "v ∈ E" then obtain f where f: "f ∈ F" "v = f ⊗ u ⊕ 𝟬" using u(1,3) line_extension_mem_iff by auto then obtain Ks where Ks: "set Ks ⊆ K" "f = combine Ks Us" using Span_eq_combine_set[OF assms(1) Us