Quelle Embedded_Algebras.thy Sprache: Isabelle

(*  Title:      HOL/Algebra/Embedded_Algebras.thy
    Author:     Paulo Emílio de Vilhena
*)

theory Embedded_Algebras
  imports Subrings Generated_Groups
begin

section \<open>Definitions\<close>

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) <+>\<^bsub>R\<^esub> 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 \<open>Syntactic Definitions\<close>

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 \<open>Basic Properties - First Part\<close>

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 \<in> carrier R \<Longrightarrow> k \<otimes> (combine Ks Us) = combine (map ((\<otimes>) 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 \<in> carrier R \<Longrightarrow> (combine Ks Us) \<otimes> u = combine Ks (map (\<lambda>u'. u' \<otimes> 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 \<zero>) @ 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 \<otimes> u) \<oplus> combine Cs Us) \<oplus> ((c' \<otimes> u) \<oplus> 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) \<zero>) 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 \<open>Some Basic Properties of Linear Independence\<close>

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 \<open>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.\<close>

context
  fixes K :: "'a set" assumes K: "subfield K R"
begin

subsection \<open>Basic Properties - Second Part\<close>

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 \<open>Span as Linear Combinations\<close>

text \<open>We show that Span is the set of linear combinations\<close>

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 \<subseteq> 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) \<and> set Ks \<subseteq> 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 \<open>Corollaries\<close>

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 \<open>Span as the minimal subgroup that contains \<^term>\<open>K <#> (set Us)\<close>\<close>

text \<open>Now we show the link between Span and Group.generate\<close>

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 \<open>set Ks \<subseteq> K\<close> \<open>set Us \<subseteq> carrier R\<close> and \<open>K <#> (set Us) \<subseteq> E\<close>
    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 \<open>Corollaries\<close>

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 \<open>Span K Us \<subset> Span K Vs\<close> and \<open>Span K Vs \<subseteq> Span K Us\<close>
    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 <+>\<^bsub>R\<^esub> 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 <+>\<^bsub>R\<^esub> Span K Vs) = (Span K (u # Us) <+>\<^bsub>R\<^esub> Span K Vs)"
  proof
    show "line_extension K u (Span K Us <+>\<^bsub>R\<^esub> Span K Vs) \ (Span K (u # Us) <+>\<^bsub>R\<^esub> Span K Vs)"
    proof
      fix v assume "v \ line_extension K u (Span K Us <+>\<^bsub>R\<^esub> 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 <+>\<^bsub>R\<^esub> 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) <+>\<^bsub>R\<^esub> Span K Vs"
        unfolding set_add_def' using v(3) by auto
    qed
  next
    show "Span K (u # Us) <+>\<^bsub>R\<^esub> Span K Vs \ line_extension K u (Span K Us <+>\<^bsub>R\<^esub> Span K Vs)"
    proof
      fix v assume "v \ Span K (u # Us) <+>\<^bsub>R\<^esub> 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 <+>\<^bsub>R\<^esub> Span K Vs)"
        using line_extension_mem_iff[of "(k \ u) \ (u' \ v')" K u "Span K Us <+>\<^bsub>R\<^esub> Span K Vs"]
        unfolding set_add_def' using v by auto
    qed
  qed
  thus ?case
    using Cons by auto
qed

subsection \<open>Characterisation of Linearly Independent "Sets"\<close>

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' \<in> Span K Us" "u' \<in> carrier R"
          and v': "v' \<in> Span K Vs" "v' \<in> carrier R" "v' \<noteq> \<zero>"
          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' \<in> Span K Us" "u' \<in> carrier R"
        and v': "v' \<in> Span K Vs" "v' \<in> carrier R" and u:"u = u' \<oplus> 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) \<open>u \<oplus> \<ominus> u' = v'\<close> 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 \<open>k = \<zero>\<close> and \<open>k \<noteq> \<zero>\<close> 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 \<open>Replacement Theorem\<close>

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) \<Longrightarrow> 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 \<open>Dimension\<close>

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 \<one> "{ \<zero> }"] 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 \<open>set Us \<subseteq> carrier R\<close> have "\<exists>Vs. independent K Vs \<and> 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 <+>\<^bsub>R\<^esub> 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 <+>\<^bsub>R\<^esub> 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 <+>\<^bsub>R\<^esub> 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 <+>\<^bsub>R\<^esub> 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) <+>\<^bsub>R\<^esub> F \ E <+>\<^bsub>R\<^esub> F"
    using mono_Span_append(1)[OF in_carrier(1) Bs(1)] Us(3) unfolding set_add_def' by auto
  moreover have "E <+>\<^bsub>R\<^esub> F \ (Span K Us) <+>\<^bsub>R\<^esub> F"
  proof
    fix v assume "v \ E <+>\<^bsub>R\<^esub> 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' \<in> Span K Us" and u2': "u2' \<in> Span K Bs" and u': "u' = u1' \<oplus> 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) <+>\<^bsub>R\<^esub> F"
      using u1' unfolding set_add_def' by auto
  qed
  ultimately have "Span K (Us @ (Vs @ Bs)) = E <+>\<^bsub>R\<^esub> 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(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 ] <+>\<^bsub>R\<^esub> 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: "\\<^bsub>S\<^esub> \ \\<^bsub>S\<^esub>"
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) = \\<^bsub>S\<^esub>" "set Ks \ h ` K" "set Ks \ { \\<^bsub>S\<^esub> }"
    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) = \\<^bsub>S\<^esub>"
    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 \ { \\<^bsub>S\<^esub> }"
    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 \<open>dependent (h ` K) (map h Us)\<close> 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
--> --------------------

--> maximum size reached

--> --------------------

quality100%

¤ Dauer der Verarbeitung: 0.26 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.