Theory Embedded_Algebras
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_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 -
have aux_lemma: "n ≤ m" if n: "dimension n K E" and m: "dimension m K E" for n m
proof -
from that obtain Vs
where Vs: "set Vs ⊆ carrier R" "independent K Vs" "length Vs = n" "Span K Vs = E"
using exists_base by meson
then show ?thesis
using independent_length_le_dimension[OF m Vs(2)] Span_base_incl[OF Vs(1)] by auto
qed
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 -
have aux_lemma: "∃Vs. length (Vs @ Us) = n ∧ independent K (Vs @ Us) ∧ Span K (Vs @ Us) = E"
if "k ≤ n" "independent K Us" "set Us ⊆ E" "length Us = k" for Us k
using that
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
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
end
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(1)] Us(4) by auto
have "v = f ⊗ u"
using subring_props(1)[OF assms(2)] f u(1) by auto
hence "v = combine Ks (map (λu'. u' ⊗ u) Us)"
using combine_l_distr[OF _ Us(1) u(1), of Ks] Ks(1-2)
subring_props(1)[OF assms(1)] by blast
thus "v ∈ Span K (map (λu'. u' ⊗ u) Us)"
unfolding Span_eq_combine_set[OF assms(1) in_carrier] using Ks(1) by blast
qed
moreover have "Span K (map (λu'. u' ⊗ u) Us) ⊆ E"
proof
fix v assume "v ∈ Span K (map (λu'. u' ⊗ u) Us)"
then obtain Ks where Ks: "set Ks ⊆ K" "v = combine Ks (map (λu'. u' ⊗ u) Us)"
unfolding Span_eq_combine_set[OF assms(1) in_carrier] by blast
hence "v = (combine Ks Us) ⊗ u"
using combine_l_distr[OF _ Us(1) u(1), of Ks] subring_props(1)[OF assms(1)] by auto
moreover have "combine Ks Us ∈ F"
using Us(4) Span_eq_combine_set[OF assms(1) Us(1)] Ks(1) by blast
ultimately have "v = (combine Ks Us) ⊗ u ⊕ 𝟬" and "combine Ks Us ∈ F"
using subring_props(1)[OF assms(2)] u(1) by auto
thus "v ∈ E"
using u(3) line_extension_mem_iff by auto
qed
ultimately have "Span K (map (λu'. u' ⊗ u) Us) = E" by auto
thus ?thesis
using dimensionI[OF assms(1) li] Us(2) by simp
qed
lemma (in ring) telescopic_base:
assumes "subfield K R" "subfield F R"
and "dimension n K F" and "dimension m F E"
shows "dimension (n * m) K E"
using assms(4)
proof (induct m arbitrary: E)
case 0 thus ?case
using dimension_zero[OF assms(2)] zero_dim by auto
next
case (Suc m)
obtain Vs
where Vs: "set Vs ⊆ carrier R" "length Vs = Suc m" "independent F Vs" "Span F Vs = E"
using exists_base[OF assms(2) Suc(2)] by blast
then obtain v Vs' where v: "Vs = v # Vs'"
by (meson length_Suc_conv)
hence li: "independent F [ v ]" "independent F Vs'" and inter: "Span F [ v ] ∩ Span F Vs' = { 𝟬 }"
using Vs(3) independent_split[OF assms(2), of "[ v ]" Vs'] by auto
have "dimension n K (Span F [ v ])"
using dimension_independent[OF li(1)] telescopic_base_aux[OF assms(1-3)] by simp
moreover have "dimension (n * m) K (Span F Vs')"
using Suc(1) dimension_independent[OF li(2)] Vs(2) unfolding v by auto
ultimately have "dimension (n * Suc m) K (Span F [ v ] <+>⇘R⇙ Span F Vs')"
using dimension_direct_sum_space[OF assms(1) _ _ inter] by auto
thus "dimension (n * Suc m) K E"
using Span_append_eq_set_add[OF assms(2) li[THEN independent_in_carrier]] Vs(4) v by auto
qed
context ring_hom_ring
begin
lemma combine_hom:
"⟦ set Ks ⊆ carrier R; set Us ⊆ carrier R ⟧ ⟹ combine (map h Ks) (map h Us) = h (R.combine Ks Us)"
by (induct Ks Us rule: R.combine.induct) (auto)
lemma line_extension_hom:
assumes "K ⊆ carrier R" "a ∈ carrier R" "E ⊆ carrier R"
shows "line_extension (h ` K) (h a) (h ` E) = h ` R.line_extension K a E"
using set_add_hom[OF homh R.r_coset_subset_G[OF assms(1-2)] assms(3)]
coset_hom(2)[OF ring_hom_in_hom(1)[OF homh] assms(1-2)]
unfolding R.line_extension_def S.line_extension_def
by simp
lemma Span_hom:
assumes "K ⊆ carrier R" "set Us ⊆ carrier R"
shows "Span (h ` K) (map h Us) = h ` R.Span K Us"
using assms line_extension_hom R.Span_in_carrier by (induct Us) (auto)
lemma inj_on_subgroup_iff_trivial_ker:
assumes "subgroup H (add_monoid R)"
shows "inj_on h H ⟷ a_kernel (R ⦇ carrier := H ⦈) S h = { 𝟬 }"
using group_hom.inj_on_subgroup_iff_trivial_ker[OF a_group_hom assms]
unfolding a_kernel_def[of "R ⦇ carrier := H ⦈" S h] by simp
corollary inj_on_Span_iff_trivial_ker:
assumes "subfield K R" "set Us ⊆ carrier R"
shows "inj_on h (R.Span K Us) ⟷ a_kernel (R ⦇ carrier := R.Span K Us ⦈) S h = { 𝟬 }"
using inj_on_subgroup_iff_trivial_ker[OF R.Span_is_add_subgroup[OF assms]] .
context
fixes K :: "'a set" assumes K: "subfield K R" and one_zero: "𝟭⇘S⇙ ≠ 𝟬⇘S⇙"
begin
lemma inj_hom_preserves_independent:
assumes "inj_on h (R.Span K Us)"
and "R.independent K Us" shows "independent (h ` K) (map h Us)"
proof (rule ccontr)
have in_carrier: "set Us ⊆ carrier R" "set (map h Us) ⊆ carrier S"
using R.independent_in_carrier[OF assms(2)] by auto
assume ld: "dependent (h ` K) (map h Us)"
obtain Ks :: "'c list"
where Ks: "length Ks = length Us" "combine Ks (map h Us) = 𝟬⇘S⇙" "set Ks ⊆ h ` K" "set Ks ≠ { 𝟬⇘S⇙ }"
using dependent_imp_non_trivial_combine[OF img_is_subfield(2)[OF K one_zero] in_carrier(2) ld]
by (metis length_map)
obtain Ks' where Ks': "set Ks' ⊆ K" "Ks = map h Ks'"
using Ks(3) by (induct Ks) (auto, metis insert_subset list.simps(15,9))
hence "h (R.combine Ks' Us) = 𝟬⇘S⇙"
using combine_hom[OF _ in_carrier(1)] Ks(2) subfieldE(3)[OF K] by (metis subset_trans)
moreover have "R.combine Ks' Us ∈ R.Span K Us"
using R.Span_eq_combine_set[OF K in_carrier(1)] Ks'(1) by auto
ultimately have "R.combine Ks' Us = 𝟬"
using assms hom_zero R.Span_subgroup_props(2)[OF K in_carrier(1)] by (auto simp add: inj_on_def)
hence "set Ks' ⊆ { 𝟬 }"
using R.independent_imp_trivial_combine[OF K assms(2)] Ks' Ks(1)
by (metis length_map order_refl take_all)
hence "set Ks ⊆ { 𝟬⇘S⇙ }"
unfolding Ks' using hom_zero by (induct Ks') (auto)
hence "Ks = []"
using Ks(4) by (metis set_empty2 subset_singletonD)
hence "independent (h ` K) (map h Us)"
using independent.li_Nil Ks(1) by simp
from ‹dependent (h ` K) (map h Us)› and this show False by simp
qed
corollary inj_hom_dimension:
assumes "inj_on h E"
and "R.dimension n K E" shows "dimension n (h ` K) (h ` E)"
proof -
obtain Us
where Us: "set Us ⊆ carrier R" "R.independent K Us" "length Us = n" "R.Span K Us = E"
using R.exists_base[OF K assms(2)] by blast
hence "dimension n (h ` K) (Span (h ` K) (map h Us))"
using dimension_independent[OF inj_hom_preserves_independent[OF _ Us(2)]] assms(1) by auto
thus ?thesis
using Span_hom[OF subfieldE(3)[OF K] Us(1)] Us(4) by simp
qed
corollary rank_nullity_theorem:
assumes "R.dimension n K E" and "R.dimension m K (a_kernel (R ⦇ carrier := E ⦈) S h)"
shows "dimension (n - m) (h ` K) (h ` E)"
proof -
obtain Us
where Us: "set Us ⊆ carrier R" "R.independent K Us" "length Us = m"
"R.Span K Us = a_kernel (R ⦇ carrier := E ⦈) S h"
using R.exists_base[OF K assms(2)] by blast
obtain Vs
where Vs: "R.independent K (Vs @ Us)" "length (Vs @ Us) = n" "R.Span K (Vs @ Us) = E"
using R.complete_base[OF K assms(1) Us(2)] R.Span_base_incl[OF K Us(1)] Us(4)
unfolding a_kernel_def' by auto
have set_Vs: "set Vs ⊆ carrier R"
using R.independent_in_carrier[OF Vs(1)] by auto
have "R.Span K Vs ∩ a_kernel (R ⦇ carrier := E ⦈) S h = { 𝟬 }"
using R.independent_split[OF K Vs(1)] Us(4) by simp
moreover have "R.Span K Vs ⊆ E"
using R.mono_Span_append(1)[OF K set_Vs Us(1)] Vs(3) by auto
ultimately have "a_kernel (R ⦇ carrier := R.Span K Vs ⦈) S h ⊆ { 𝟬 }"
unfolding a_kernel_def' by (simp del: R.Span.simps, blast)
hence "a_kernel (R ⦇ carrier := R.Span K Vs ⦈) S h = { 𝟬 }"
using R.Span_subgroup_props(2)[OF K set_Vs]
unfolding a_kernel_def' by (auto simp del: R.Span.simps)
hence "inj_on h (R.Span K Vs)"
using inj_on_Span_iff_trivial_ker[OF K set_Vs] by simp
moreover have "R.dimension (n - m) K (R.Span K Vs)"
using R.dimension_independent[OF R.independent_split(2)[OF K Vs(1)]] Vs(2) Us(3) by auto
ultimately have "dimension (n - m) (h ` K) (h ` (R.Span K Vs))"
using assms(1) inj_hom_dimension by simp
have "h ` E = h ` (R.Span K Vs <+>⇘R⇙ R.Span K Us)"
using R.Span_append_eq_set_add[OF K set_Vs Us(1)] Vs(3) by simp
hence "h ` E = h ` (R.Span K Vs) <+>⇘S⇙ h ` (R.Span K Us)"
using R.Span_subgroup_props(1)[OF K] set_Vs Us(1) set_add_hom[OF homh] by auto
moreover have "h ` (R.Span K Us) = { 𝟬⇘S⇙ }"
using R.space_subgroup_props(2)[OF K assms(1)] unfolding Us(4) a_kernel_def' by force
ultimately have "h ` E = h ` (R.Span K Vs) <+>⇘S⇙ { 𝟬⇘S⇙ }"
by simp
hence "h ` E = h ` (R.Span K Vs)"
using R.Span_subgroup_props(1-2)[OF K set_Vs] unfolding set_add_def' by force
from ‹dimension (n - m) (h ` K) (h ` (R.Span K Vs))› and this show ?thesis by simp
qed
end
end
lemma (in ring_hom_ring)
assumes "subfield K R" and "set Us ⊆ carrier R" and "𝟭⇘S⇙ ≠ 𝟬⇘S⇙"
and "independent (h ` K) (map h Us)" shows "R.independent K Us"
proof (rule ccontr)
assume "R.dependent K Us"
then obtain Ks
where "length Ks = length Us" and "R.combine Ks Us = 𝟬" and "set Ks ⊆ K" and "set Ks ≠ { 𝟬 }"
using R.dependent_imp_non_trivial_combine[OF assms(1-2)] by metis
hence "combine (map h Ks) (map h Us) = 𝟬⇘S⇙"
using combine_hom[OF _ assms(2), of Ks] subfieldE(3)[OF assms(1)] by simp
moreover from ‹set Ks ⊆ K› have "set (map h Ks) ⊆ h ` K"
by (induction Ks) (auto)
moreover have "¬ set (map h Ks) ⊆ { h 𝟬 }"
proof (rule ccontr)
assume "¬ ¬ set (map h Ks) ⊆ { h 𝟬 }" then have "set (map h Ks) ⊆ { h 𝟬 }"
by simp
moreover from ‹R.dependent K Us› and ‹length Ks = length Us› have "Ks ≠ []"
by auto
ultimately have "set (map h Ks) = { h 𝟬 }"
using subset_singletonD by fastforce
with ‹set Ks ⊆ K› have "set Ks = { 𝟬 }"
using inj_onD[OF _ _ _ subringE(2)[OF subfieldE(1)[OF assms(1)]], of h]
img_is_subfield(1)[OF assms(1,3)] subset_singletonD
by (induction Ks) (auto simp add: subset_singletonD, fastforce)
with ‹set Ks ≠ { 𝟬 }› show False
by simp
qed
with ‹length Ks = length Us› have "¬ set (take (length (map h Us)) (map h Ks)) ⊆ { h 𝟬 }"
by auto
ultimately have "dependent (h ` K) (map h Us)"
using non_trivial_combine_imp_dependent[OF img_is_subfield(2)[OF assms(1,3)], of "map h Ks"] by simp
with ‹independent (h ` K) (map h Us)› show False
by simp
qed
subsection ‹Finite Dimension›
definition (in ring) finite_dimension :: "'a set ⇒ 'a set ⇒ bool"
where "finite_dimension K E ⟷ (∃n. dimension n K E)"
abbreviation (in ring) infinite_dimension :: "'a set ⇒ 'a set ⇒ bool"
where "infinite_dimension K E ≡ ¬ finite_dimension K E"
definition (in ring) dim :: "'a set ⇒ 'a set ⇒ nat"
where "dim K E = (THE n. dimension n K E)"
locale subalgebra = subgroup V "add_monoid R" for K and V and R (structure) +
assumes smult_closed: "⟦ k ∈ K; v ∈ V ⟧ ⟹ k ⊗ v ∈ V"
subsubsection ‹Basic Properties›
lemma (in ring) unique_dimension:
assumes "subfield K R" and "finite_dimension K E" shows "∃!n. dimension n K E"
using assms(2) dimension_is_inj[OF assms(1)] unfolding finite_dimension_def by auto
lemma (in ring) finite_dimensionI:
assumes "dimension n K E" shows "finite_dimension K E"
using assms unfolding finite_dimension_def by auto
lemma (in ring) finite_dimensionE:
assumes "subfield K R" and "finite_dimension K E" shows "dimension ((dim over K) E) K E"
using theI'[OF unique_dimension[OF assms]] unfolding over_def dim_def by simp
lemma (in ring) dimI:
assumes "subfield K R" and "dimension n K E" shows "(dim over K) E = n"
using finite_dimensionE[OF assms(1) finite_dimensionI] dimension_is_inj[OF assms(1)] assms(2)
unfolding over_def dim_def by auto
lemma (in ring) finite_dimensionE' [elim]:
assumes "finite_dimension K E" and "⋀n. dimension n K E ⟹ P" shows P
using assms unfolding finite_dimension_def by auto
lemma (in ring) Span_finite_dimension:
assumes "subfield K R" and "set Us ⊆ carrier R"
shows "finite_dimension K (Span K Us)"
using filter_base[OF assms] finite_dimensionI[OF dimension_independent[of K]] by metis
lemma (in ring) carrier_is_subalgebra:
assumes "K ⊆ carrier R" shows "subalgebra K (carrier R) R"
using assms subalgebra.intro[OF add.group_incl_imp_subgroup[of "carrier R"], of K] add.group_axioms
unfolding subalgebra_axioms_def by auto
lemma (in ring) subalgebra_in_carrier:
assumes "subalgebra K V R" shows "V ⊆ carrier R"
using subgroup.subset[OF subalgebra.axioms(1)[OF assms]] by simp
lemma (in ring) subalgebra_inter:
assumes "subalgebra K V R" and "subalgebra K V' R" shows "subalgebra K (V ∩ V') R"
using add.subgroups_Inter_pair assms unfolding subalgebra_def subalgebra_axioms_def by auto
lemma (in ring_hom_ring) img_is_subalgebra:
assumes "K ⊆ carrier R" and "subalgebra K V R" shows "subalgebra (h ` K) (h ` V) S"
proof (intro subalgebra.intro)
have "group_hom (add_monoid R) (add_monoid S) h"
using ring_hom_in_hom(2)[OF homh] R.add.group_axioms add.group_axioms
unfolding group_hom_def group_hom_axioms_def by auto
thus "subgroup (h ` V) (add_monoid S)"
using group_hom.subgroup_img_is_subgroup[OF _ subalgebra.axioms(1)[OF assms(2)]] by force
next
show "subalgebra_axioms (h ` K) (h ` V) S"
using R.subalgebra_in_carrier[OF assms(2)] subalgebra.axioms(2)[OF assms(2)] assms(1)
unfolding subalgebra_axioms_def
by (auto, metis hom_mult image_eqI subset_iff)
qed
lemma (in ring) ideal_is_subalgebra:
assumes "K ⊆ carrier R" "ideal I R" shows "subalgebra K I R"
using ideal.axioms(1)[OF assms(2)] ideal.I_l_closed[OF assms(2)] assms(1)
unfolding subalgebra_def subalgebra_axioms_def additive_subgroup_def by auto
lemma (in ring) Span_is_subalgebra:
assumes "subfield K R" "set Us ⊆ carrier R" shows "subalgebra K (Span K Us) R"
using Span_smult_closed[OF assms] Span_is_add_subgroup[OF assms]
unfolding subalgebra_def subalgebra_axioms_def by auto
lemma (in ring) finite_dimension_imp_subalgebra:
assumes "subfield K R" "finite_dimension K E" shows "subalgebra K E R"
using exists_base[OF assms(1) finite_dimensionE[OF assms]] Span_is_subalgebra[OF assms(1)] by auto
lemma (in ring) subalgebra_Span_incl:
assumes "subfield K R" and "subalgebra K V R" "set Us ⊆ V" shows "Span K Us ⊆ V"
proof -
have "K <#> (set Us) ⊆ V"
using subalgebra.smult_closed[OF assms(2)] assms(3) unfolding set_mult_def by blast
moreover have "set Us ⊆ carrier R"
using subalgebra_in_carrier[OF assms(2)] assms(3) by auto
ultimately show ?thesis
using subalgebra.axioms(1)[OF assms(2)] Span_min[OF assms(1)] by blast
qed
lemma (in ring) Span_subalgebra_minimal:
assumes "subfield K R" "set Us ⊆ carrier R"
shows "Span K Us = ⋂ { V. subalgebra K V R ∧ set Us ⊆ V }"
using Span_is_subalgebra[OF assms] Span_base_incl[OF assms] subalgebra_Span_incl[OF assms(1)]
by blast
lemma (in ring) Span_subalgebraI:
assumes "subfield K R"
and "subalgebra K E R" "set Us ⊆ E"
and "⋀V. ⟦ subalgebra K V R; set Us ⊆ V ⟧ ⟹ E ⊆ V"
shows "E = Span K Us"
proof -
have "⋂ { V. subalgebra K V R ∧ set Us ⊆ V } = E"
using assms(2-4) by auto
thus "E = Span K Us"
using Span_subalgebra_minimal subalgebra_in_carrier[of K E] assms by auto
qed
lemma (in ring) subalbegra_incl_imp_finite_dimension:
assumes "subfield K R" and "finite_dimension K E"
and "subalgebra K V R" "V ⊆ E" shows "finite_dimension K V"
proof -
obtain n where n: "dimension n K E"
using assms(2) by auto
define S where "S = { Us. set Us ⊆ V ∧ independent K Us }"
have "length ` S ⊆ {..n}"
unfolding S_def using independent_length_le_dimension[OF assms(1) n] assms(4) by auto
moreover have "[] ∈ S"
unfolding S_def by simp
hence "length ` S ≠ {}" by blast
ultimately obtain m where m: "m ∈ length ` S" and greatest: "⋀k. k ∈ length ` S ⟹ k ≤ m"
by (meson Max_ge Max_in finite_atMost rev_finite_subset)
then obtain Us where Us: "set Us ⊆ V" "independent K Us" "m = length Us"
unfolding S_def by auto
have "Span K Us = V"
proof (rule ccontr)
assume "¬ Span K Us = V" then have "Span K Us ⊂ V"
using subalgebra_Span_incl[OF assms(1,3) Us(1)] by blast
then obtain v where v:"v ∈ V" "v ∉ Span K Us"
by blast
hence "independent K (v # Us)"
using independent.li_Cons[OF _ _ Us(2)] subalgebra_in_carrier[OF assms(3)] by auto
hence "(v # Us) ∈ S"
unfolding S_def using Us(1) v(1) by auto
hence "length (v # Us) ≤ m"
using greatest by blast
moreover have "length (v # Us) = Suc m"
using Us(3) by auto
ultimately show False by simp
qed
thus ?thesis
using finite_dimensionI[OF dimension_independent[OF Us(2)]] by simp
qed
lemma (in ring_hom_ring) infinite_dimension_hom:
assumes "subfield K R" and "𝟭⇘S⇙ ≠ 𝟬⇘S⇙" and "inj_on h E" and "subalgebra K E R"
shows "R.infinite_dimension K E ⟹ infinite_dimension (h ` K) (h ` E)"
proof -
note subfield = img_is_subfield(2)[OF assms(1-2)]
assume "R.infinite_dimension K E"
show "infinite_dimension (h ` K) (h ` E)"
proof (rule ccontr)
assume "¬ infinite_dimension (h ` K) (h ` E)"
then obtain Vs where "set Vs ⊆ carrier S" and "Span (h ` K) Vs = h ` E"
using exists_base[OF subfield] by blast
hence "set Vs ⊆ h ` E"
using Span_base_incl[OF subfield] by blast
hence "∃Us. set Us ⊆ E ∧ Vs = map h Us"
by (induct Vs) (auto, metis insert_subset list.simps(9,15))
then obtain Us where "set Us ⊆ E" and "Vs = map h Us"
by blast
with ‹Span (h ` K) Vs = h ` E› have "h ` (R.Span K Us) = h ` E"
using R.subalgebra_in_carrier[OF assms(4)] Span_hom assms(1) by auto
moreover from ‹set Us ⊆ E› have "R.Span K Us ⊆ E"
using R.subalgebra_Span_incl assms(1-4) by blast
ultimately have "R.Span K Us = E"
proof (auto simp del: R.Span.simps)
fix a assume "a ∈ E"
with ‹h ` (R.Span K Us) = h ` E› obtain b where "b ∈ R.Span K Us" and "h a = h b"
by auto
with ‹R.Span K Us ⊆ E› and ‹a ∈ E› have "a = b"
using inj_onD[OF assms(3)] by auto
with ‹b ∈ R.Span K Us› show "a ∈ R.Span K Us"
by simp
qed
with ‹set Us ⊆ E› have "R.finite_dimension K E"
using R.Span_finite_dimension[OF assms(1)] R.subalgebra_in_carrier[OF assms(4)] by auto
with ‹R.infinite_dimension K E› show False
by simp
qed
qed
subsubsection ‹Reformulation of some lemmas in this new language.›
lemma (in ring) sum_space_dim:
assumes "subfield K R" "finite_dimension K E" "finite_dimension K F"
shows "finite_dimension K (E <+>⇘R⇙ F)"
and "((dim over K) (E <+>⇘R⇙ F)) = ((dim over K) E) + ((dim over K) F) - ((dim over K) (E ∩ F))"
proof -
obtain n m k where n: "dimension n K E" and m: "dimension m K F" and k: "dimension k K (E ∩ F)"
using assms(2-3) subalbegra_incl_imp_finite_dimension[OF assms(1-2)
subalgebra_inter[OF assms(2-3)[THEN finite_dimension_imp_subalgebra[OF assms(1)]]]]
by (meson inf_le1 finite_dimension_def)
hence "dimension (n + m - k) K (E <+>⇘R⇙ F)"
using dimension_sum_space[OF assms(1)] by simp
thus "finite_dimension K (E <+>⇘R⇙ F)"
and "((dim over K) (E <+>⇘R⇙ F)) = ((dim over K) E) + ((dim over K) F) - ((dim over K) (E ∩ F))"
using finite_dimensionI dimI[OF assms(1)] n m k by auto
qed
lemma (in ring) telescopic_base_dim:
assumes "subfield K R" "subfield F R" and "finite_dimension K F" and "finite_dimension F E"
shows "finite_dimension K E" and "(dim over K) E = ((dim over K) F) * ((dim over F) E)"
using telescopic_base[OF assms(1-2)
finite_dimensionE[OF assms(1,3)]
finite_dimensionE[OF assms(2,4)]]
dimI[OF assms(1)] finite_dimensionI
by auto
end