Theory HOL-Algebra.Embedded_Algebras

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

theory Embedded_Algebras
  imports Subrings Generated_Groups
begin

section ‹Definitions›

locale embedded_algebra =
  K?: subfield K R + R?: ring R for K :: "'a set" and R :: "('a, 'b) ring_scheme" (structure)

definition (in ring) line_extension :: "'a set  'a  'a set  'a set"
  where "line_extension K a E = (K #> a) <+>RE"

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 termK <#> (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 <+>RSpan 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 <+>RSpan K Vs) = (Span K (u # Us) <+>RSpan K Vs)"
  proof
    show "line_extension K u (Span K Us <+>RSpan K Vs)  (Span K (u # Us) <+>RSpan K Vs)"
    proof
      fix v assume "v  line_extension K u (Span K Us <+>RSpan 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 <+>RSpan 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) <+>RSpan K Vs"
        unfolding set_add_def' using v(3) by auto
    qed
  next
    show "Span K (u # Us) <+>RSpan K Vs  line_extension K u (Span K Us <+>RSpan K Vs)"
    proof
      fix v assume "v  Span K (u # Us) <+>RSpan 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 <+>RSpan K Vs)"
        using line_extension_mem_iff[of "(k  u)  (u'  v')" K u "Span K Us <+>RSpan K Vs"]
        unfolding set_add_def' using v by auto
    qed
  qed
  thus ?case
    using Cons by auto
qed


subsection ‹Characterisation of Linearly Independent "Sets"›

declare independent_backwards [intro]
declare independent_in_carrier [intro]

lemma independent_distinct: "independent K Us  distinct Us"
proof (induct Us rule: list.induct)
  case Nil thus ?case by simp
next
  case Cons thus ?case
    using independent_backwards[OF Cons(2)]
          independent_in_carrier[OF Cons(2)]
          Span_base_incl
    by auto
qed

lemma independent_strict_incl:
  assumes "independent K (u # Us)" shows "Span K Us  Span K (u # Us)"
proof -
  have "u  Span K (u # Us)"
    using Span_base_incl[OF independent_in_carrier[OF assms]] by auto
  moreover have "Span K Us  Span K (u # Us)"
    using mono_Span independent_in_carrier[OF assms] by auto
  ultimately show ?thesis
    using independent_backwards(1)[OF assms] by auto
qed

corollary independent_replacement:
  assumes "independent K (u # Us)" and "independent K Vs"
  shows "Span K (u # Us)  Span K Vs  (v  set Vs. independent K (v # Us))"
proof -
  assume "Span K (u # Us)  Span K Vs"
  hence "Span K Us  Span K Vs"
    using independent_strict_incl[OF assms(1)] by auto
  then obtain v where v: "v  set Vs" "v  Span K Us"
    using Span_strict_incl[of Us Vs] assms[THEN independent_in_carrier] by auto
  thus ?thesis
    using li_Cons[of v K Us] assms independent_in_carrier[OF assms(2)] by auto
qed

lemma independent_split:
  assumes "independent K (Us @ Vs)"
  shows "independent K Vs"
    and "independent K Us"
    and "Span K Us  Span K Vs = { 𝟬 }"
proof -
  from assms show "independent K Vs"
    by (induct Us) (auto)
next
  from assms show "independent K Us"
  proof (induct Us)
    case Nil thus ?case by simp
  next
    case (Cons u Us')
    hence u: "u  carrier R" and "set Us'  carrier R" "set Vs  carrier R"
      using independent_in_carrier[of K "(u # Us') @ Vs"] by auto
    hence "Span K Us'  Span K (Us' @ Vs)"
      using mono_Span_append(1) by simp
    thus ?case
      using independent_backwards[of K u "Us' @ Vs"] Cons li_Cons[OF u] by auto
  qed
next
  from assms show "Span K Us  Span K Vs = { 𝟬 }"
  proof (induct Us rule: list.induct)
    case Nil thus ?case
      using Span_subgroup_props(2)[OF independent_in_carrier[of K Vs]] by simp
  next
    case (Cons u Us)
    hence IH: "Span K Us  Span K Vs = {𝟬}" by auto
    have in_carrier:
      "u  carrier R" "set Us  carrier R" "set Vs  carrier R" "set (u # Us)  carrier R"
      using Cons(2)[THEN independent_in_carrier] by auto
    hence "{ 𝟬 }  Span K (u # Us)  Span K Vs"
      using in_carrier(3-4)[THEN Span_subgroup_props(2)] by auto

    moreover have "Span K (u # Us)  Span K Vs  { 𝟬 }"
    proof (rule ccontr)
      assume "¬ Span K (u # Us)  Span K Vs  {𝟬}"
      hence "a. a  𝟬  a  Span K (u # Us)  a  Span K Vs" by auto
      then obtain k u' v'
        where u': "u'  Span K Us" "u'  carrier R"
          and v': "v'  Span K Vs" "v'  carrier R" "v'  𝟬"
          and k: "k  K" "(k  u  u') = v'"
        using line_extension_mem_iff[of _ _ u "Span K Us"] in_carrier(2-3)[THEN Span_subgroup_props(1)]
              subring_props(1) by force
      hence "v' = 𝟬" if "k = 𝟬"
        using in_carrier(1) that IH by auto
      hence diff_zero: "k  𝟬" using v'(3) by auto

      have "k  carrier R"
        using subring_props(1) k(1) by blast
      hence "k  u = ( u')  v'"
        using in_carrier(1) k(2) u'(2) v'(2) add.m_comm r_neg1 by auto
      hence "k  u  Span K (Us @ Vs)"
        using Span_subgroup_props(4)[OF in_carrier(2) u'(1)] v'(1)
              Span_append_eq_set_add[OF in_carrier(2-3)] unfolding set_add_def' by blast
      hence "u  Span K (Us @ Vs)"
        using Cons(2) Span_m_inv_simprule[OF _ _ in_carrier(1), of "Us @ Vs" k]
              diff_zero k(1) in_carrier(2-3) by auto
      moreover have "u  Span K (Us @ Vs)"
        using independent_backwards(1)[of K u "Us @ Vs"] Cons(2) by auto
      ultimately show False by simp
    qed

    ultimately show ?case by auto
  qed
qed

lemma independent_append:
  assumes "independent K Us" and "independent K Vs" and "Span K Us  Span K Vs = { 𝟬 }"
  shows "independent K (Us @ Vs)"
  using assms
proof (induct Us rule: list.induct)
  case Nil thus ?case by simp
next
  case (Cons u Us)
  hence in_carrier:
    "u  carrier R" "set Us  carrier R" "set Vs  carrier R" "set (u # Us)  carrier R"
    using Cons(2-3)[THEN independent_in_carrier] by auto
  hence "Span K Us  Span K (u # Us)"
    using mono_Span by auto
  hence "Span K Us  Span K Vs = { 𝟬 }"
    using Cons(4) Span_subgroup_props(2)[OF in_carrier(2)] by auto
  hence "independent K (Us @ Vs)"
    using Cons by auto
  moreover have "u  Span K (Us @ Vs)"
  proof (rule ccontr)
    assume "¬ u  Span K (Us @ Vs)"
    then obtain u' v'
      where u': "u'  Span K Us" "u'  carrier R"
        and v': "v'  Span K Vs" "v'  carrier R" and u:"u = u'  v'"
      using Span_append_eq_set_add[OF in_carrier(2-3)] in_carrier(2-3)[THEN Span_subgroup_props(1)]
      unfolding set_add_def' by blast
    hence "u  ( u') = v'"
      using in_carrier(1) by algebra
    moreover have "u  Span K (u # Us)" and "u'  Span K (u # Us)"
      using Span_base_incl[OF in_carrier(4)] mono_Span[OF in_carrier(2,1)] u'(1)
      by (auto simp del: Span.simps)
    hence "u  ( u')  Span K (u # Us)"
      using Span_subgroup_props(3-4)[OF in_carrier(4)] by (auto simp del: Span.simps)
    ultimately have "u  ( u') = 𝟬"
      using Cons(4) v'(1) by auto
    hence "u = u'"
      using Cons(4) v'(1) in_carrier(1) u'(2) u   u' = v' u by auto
    thus False
      using u'(1) independent_backwards(1)[OF Cons(2)] by simp
  qed
  ultimately show ?case
    using in_carrier(1) li_Cons by simp
qed

lemma independent_imp_trivial_combine:
  assumes "independent K Us"
  shows "Ks.  set Ks  K; combine Ks Us = 𝟬   set (take (length Us) Ks)  { 𝟬 }"
  using assms
proof (induct Us rule: list.induct)
  case Nil thus ?case by simp
next
  case (Cons u Us) thus ?case
  proof (cases "Ks = []")
    assume "Ks = []" thus ?thesis by auto
  next
    assume "Ks  []"
    then obtain k Ks' where k: "k  K" and Ks': "set Ks'  K" and Ks: "Ks = k # Ks'"
      using Cons(2) by (metis insert_subset list.exhaust_sel list.simps(15))
    hence Us: "set Us  carrier R" and u: "u  carrier R"
      using independent_in_carrier[OF Cons(4)] by auto
    have "u  Span K Us" if "k  𝟬"
      using that Span_mem_iff[OF Us u] Cons(3-4) Ks' k unfolding Ks by blast
    hence k_zero: "k = 𝟬"
      using independent_backwards[OF Cons(4)] by blast
    hence "combine Ks' Us = 𝟬"
      using combine_in_carrier[OF _ Us, of Ks'] Ks' u Cons(3) subring_props(1) unfolding Ks by auto
    hence "set (take (length Us) Ks')  { 𝟬 }"
      using Cons(1)[OF Ks' _ independent_backwards(2)[OF Cons(4)]] by simp
    thus ?thesis
      using k_zero unfolding Ks by auto
  qed
qed

lemma non_trivial_combine_imp_dependent:
  assumes "set Ks  K" and "combine Ks Us = 𝟬" and "¬ set (take (length Us) Ks)  { 𝟬 }"
  shows "dependent K Us"
  using independent_imp_trivial_combine[OF _ assms(1-2)] assms(3) by blast  

lemma trivial_combine_imp_independent:
  assumes "set Us  carrier R"
    and "Ks.  set Ks  K; combine Ks Us = 𝟬   set (take (length Us) Ks)  { 𝟬 }"
  shows "independent K Us"
  using assms
proof (induct Us)
  case Nil thus ?case by simp
next
  case (Cons u Us)
  hence Us: "set Us  carrier R" and u: "u  carrier R" by auto

  have "Ks.  set Ks  K; combine Ks Us = 𝟬   set (take (length Us) Ks)  { 𝟬 }"
  proof -
    fix Ks assume Ks: "set Ks  K" and lin_c: "combine Ks Us = 𝟬"
    hence "combine (𝟬 # Ks) (u # Us) = 𝟬"
      using u subring_props(1) combine_in_carrier[OF _ Us] by auto
    hence "set (take (length (u # Us)) (𝟬 # Ks))  { 𝟬 }"
      using Cons(3)[of "𝟬 # Ks"] subring_props(2) Ks by auto
    thus "set (take (length Us) Ks)  { 𝟬 }" by auto
  qed
  hence "independent K Us"
    using Cons(1)[OF Us] by simp

  moreover have "u  Span K Us"
  proof (rule ccontr)
    assume "¬ u  Span K Us"
    then obtain k Ks where k: "k  K" "k  𝟬" and Ks: "set Ks  K" and u: "combine (k # Ks) (u # Us) = 𝟬"
      using Span_mem_iff[OF Us u] by auto
    have "set (take (length (u # Us)) (k # Ks))  { 𝟬 }"
      using Cons(3)[OF _ u] k(1) Ks by auto
    hence "k = 𝟬" by auto
    from k = 𝟬 and k  𝟬 show False by simp
  qed

  ultimately show ?case
    using li_Cons[OF u] by simp
qed

corollary dependent_imp_non_trivial_combine:
  assumes "set Us  carrier R" and "dependent K Us"
  obtains Ks where "length Ks = length Us" "combine Ks Us = 𝟬" "set Ks  K" "set Ks  { 𝟬 }"
proof -
  obtain Ks
    where Ks: "set Ks  carrier R" "set Ks  K" "combine Ks Us = 𝟬" "¬ set (take (length Us) Ks)  { 𝟬 }"
    using trivial_combine_imp_independent[OF assms(1)] assms(2) subring_props(1) by blast
  obtain Ks'
    where Ks': "set (take (length Us) Ks)  set Ks'" "set Ks'  set (take (length Us) Ks)  { 𝟬 }"
               "length Ks' = length Us" "combine Ks' Us = 𝟬"
    using combine_normalize[OF Ks(1) assms(1) Ks(3)] by metis
  have "set (take (length Us) Ks)  set Ks"
    by (simp add: set_take_subset) 
  hence "set Ks'  K"
    using Ks(2) Ks'(2) subring_props(2) Un_commute by blast
  moreover have "set Ks'  { 𝟬 }"
    using Ks'(1) Ks(4) by auto
  ultimately show thesis
    using that Ks' by blast
qed

corollary unique_decomposition:
  assumes "independent K Us"
  shows "a  Span K Us  ∃!Ks. set Ks  K  length Ks = length Us  a = combine Ks Us"
proof -
  note in_carrier = independent_in_carrier[OF assms]

  assume "a  Span K Us"
  then obtain Ks where Ks: "set Ks  K" "length Ks = length Us" "a = combine Ks Us"
    using Span_mem_iff_length_version[OF in_carrier] by blast

  moreover
  have "Ks'.  set Ks'  K; length Ks' = length Us; a = combine Ks' Us   Ks = Ks'"
  proof -
    fix Ks' assume Ks': "set Ks'  K" "length Ks' = length Us" "a = combine Ks' Us"
    hence set_Ks: "set Ks  carrier R" and set_Ks': "set Ks'  carrier R"
      using subring_props(1) Ks(1) by blast+
    have same_length: "length Ks = length Ks'"
      using Ks Ks' by simp

    have "(combine Ks Us)  (( 𝟭)  (combine Ks' Us)) = 𝟬"
      using combine_in_carrier[OF set_Ks  in_carrier]
            combine_in_carrier[OF set_Ks' in_carrier] Ks(3) Ks'(3) by algebra
    hence "(combine Ks Us)  (combine (map ((⊗) ( 𝟭)) Ks') Us) = 𝟬"
      using combine_r_distr[OF set_Ks' in_carrier, of " 𝟭"] subring_props by auto
    moreover have set_map: "set (map ((⊗) ( 𝟭)) Ks')  K"
      using Ks'(1) subring_props by (induct Ks') (auto)
    hence "set (map ((⊗) ( 𝟭)) Ks')  carrier R"
      using subring_props(1) by blast
    ultimately have "combine (map2 (⊕) Ks (map ((⊗) ( 𝟭)) Ks')) Us = 𝟬"
      using combine_add[OF Ks(2) _ set_Ks _ in_carrier, of "map ((⊗) ( 𝟭)) Ks'"] Ks'(2) by auto
    moreover have "set (map2 (⊕) Ks (map ((⊗) ( 𝟭)) Ks'))  K"
      using Ks(1) set_map subring_props(7)
      by (induct Ks) (auto, metis contra_subsetD in_set_zipE local.set_map set_ConsD subring_props(7))
    ultimately have "set (take (length Us) (map2 (⊕) Ks (map ((⊗) ( 𝟭)) Ks')))  { 𝟬 }"
      using independent_imp_trivial_combine[OF assms] by auto
    hence "set (map2 (⊕) Ks (map ((⊗) ( 𝟭)) Ks'))  { 𝟬 }"
      using Ks(2) Ks'(2) by auto
    thus "Ks = Ks'"
      using set_Ks set_Ks' same_length
    proof (induct Ks arbitrary: Ks')
      case Nil thus?case by simp
    next
      case (Cons k Ks)
      then obtain k' Ks'' where k': "Ks' = k' # Ks''"
        by (metis Suc_length_conv)
      have "Ks = Ks''"
        using Cons unfolding k' by auto
      moreover have "k = k'"
        using Cons(2-4) l_minus minus_equality unfolding k' by (auto, fastforce)
      ultimately show ?case
        unfolding k' by simp
    qed
  qed

  ultimately show ?thesis by blast
qed


subsection ‹Replacement Theorem›

lemma independent_rotate1_aux:
  "independent K (u # Us @ Vs)  independent K ((Us @ [u]) @ Vs)"
proof -
  assume "independent K (u # Us @ Vs)"
  hence li: "independent K [u]" "independent K Us" "independent K Vs"
    and inter: "Span K [u]  Span K Us = { 𝟬 }"
               "Span K (u # Us)  Span K Vs = { 𝟬 }"
    using independent_split[of "u # Us" Vs] independent_split[of "[u]" Us] by auto
  hence "independent K (Us @ [u])"
    using independent_append[OF li(2,1)] by auto
  moreover have "Span K (Us @ [u])  Span K Vs = { 𝟬 }"
    using Span_same_set[of "u # Us" "Us @ [u]"] li(1-2)[THEN independent_in_carrier] inter(2) by auto
  ultimately show "independent K ((Us @ [u]) @ Vs)"
    using independent_append[OF _ li(3), of "Us @ [u]"] by simp
qed

corollary independent_rotate1:
  "independent K (Us @ Vs)  independent K ((rotate1 Us) @ Vs)"
  using independent_rotate1_aux by (cases Us) (auto)

(*
corollary independent_rotate:
  "independent K (Us @ Vs) ⟹ independent K ((rotate n Us) @ Vs)"
  using independent_rotate1 by (induct n) auto

lemma rotate_append: "rotate (length l) (l @ q) = q @ l"
  by (induct l arbitrary: q) (auto simp add: rotate1_rotate_swap)
*)

corollary independent_same_set:
  assumes "set Us = set Vs" and "length Us = length Vs"
  shows "independent K Us  independent K Vs"
proof -
  assume "independent K Us" thus ?thesis
    using assms
  proof (induct Us arbitrary: Vs rule: list.induct)
    case Nil thus ?case by simp
  next
    case (Cons u Us)
    then obtain Vs' Vs'' where Vs: "Vs = Vs' @ (u # Vs'')"
      by (metis list.set_intros(1) split_list)

    have in_carrier: "u  carrier R" "set Us  carrier R"
      using independent_in_carrier[OF Cons(2)] by auto

    have "distinct Vs"
      using Cons(3-4) independent_distinct[OF Cons(2)]
      by (metis card_distinct distinct_card)
    hence "u  set (Vs' @ Vs'')" and "u  set Us"
      using independent_distinct[OF Cons(2)] unfolding Vs by auto
    hence set_eq: "set Us = set (Vs' @ Vs'')" and "length (Vs' @ Vs'') = length Us"
      using Cons(3-4) unfolding Vs by auto
    hence "independent K (Vs' @ Vs'')"
      using Cons(1)[OF independent_backwards(2)[OF Cons(2)]] unfolding Vs by simp
    hence "independent K (u # (Vs' @ Vs''))"
      using li_Cons Span_same_set[OF _ set_eq] independent_backwards(1)[OF Cons(2)] in_carrier by auto
    hence "independent K (Vs' @ (u # Vs''))"
      using independent_rotate1[of "u # Vs'" Vs''] by auto
    thus ?case unfolding Vs .
  qed
qed

lemma replacement_theorem:
  assumes "independent K (Us' @ Us)" and "independent K Vs"
    and "Span K (Us' @ Us)  Span K Vs"
  shows "Vs'. set Vs'  set Vs  length Vs' = length Us'  independent K (Vs' @ Us)"
  using assms
proof (induct "length Us'" arbitrary: Us' Us)
  case 0 thus ?case by auto
next
  case (Suc n)
  then obtain u Us'' where Us'': "Us' = Us'' @ [u]"
    by (metis list.size(3) nat.simps(3) rev_exhaust)
  then obtain Vs' where Vs': "set Vs'  set Vs" "length Vs' = n" "independent K (Vs' @ (u # Us))"
    using Suc(1)[of Us'' "u # Us"] Suc(2-5) by auto
  hence li: "independent K ((u # Vs') @ Us)"
    using independent_same_set[OF _ _ Vs'(3), of "(u # Vs') @ Us"] by auto
  moreover have in_carrier:
    "u  carrier R" "set Us  carrier R" "set Us'  carrier R" "set Vs  carrier R"
    using Suc(3-4)[THEN independent_in_carrier] Us'' by auto
  moreover have "Span K ((u # Vs') @ Us)  Span K Vs"
  proof -
    have "set Us  Span K Vs" "u  Span K Vs"
      using Suc(5) Span_base_incl[of "Us' @ Us"] Us'' in_carrier(2-3) by auto
    moreover have "set Vs'  Span K Vs"
      using Span_base_incl[OF in_carrier(4)] Vs'(1) by auto
    ultimately have "set ((u # Vs') @ Us)  Span K Vs" by auto
    thus ?thesis
      using mono_Span_subset[OF _ in_carrier(4)] by (simp del: Span.simps)
  qed
  ultimately obtain v where "v  set Vs" "independent K ((v # Vs') @ Us)"
    using independent_replacement[OF _ Suc(4), of u "Vs' @ Us"] by auto
  thus ?case
    using Vs'(1-2) Suc(2)
    by (metis (mono_tags, lifting) insert_subset length_Cons list.simps(15))
qed

corollary independent_length_le:
  assumes "independent K Us" and "independent K Vs"
  shows "set Us  Span K Vs  length Us  length Vs"
proof -
  assume "set Us  Span K Vs"
  hence "Span K Us  Span K Vs"
    using mono_Span_subset[OF _ independent_in_carrier[OF assms(2)]] by simp
  then obtain Vs' where Vs': "set Vs'  set Vs" "length Vs' = length Us" "independent K Vs'"
    using replacement_theorem[OF _ assms(2), of Us "[]"] assms(1) by auto
  hence "card (set Vs')  card (set Vs)"
    by (simp add: card_mono)
  thus "length Us  length Vs"
    using independent_distinct assms(2) Vs'(2-3) by (simp add: distinct_card)
qed


subsection ‹Dimension›

lemma exists_base:
  assumes "dimension n K E"
  shows "Vs. set Vs  carrier R  independent K Vs  length Vs = n  Span K Vs = E"
    (is "Vs. ?base K Vs E n")
  using assms
proof (induct E rule: dimension.induct)
  case zero_dim thus ?case by auto
next
  case (Suc_dim v E n K)
  then obtain Vs where Vs: "set Vs  carrier R" "independent K Vs" "length Vs = n" "Span K Vs = E"
    by auto
  hence "?base K (v # Vs) (line_extension K v E) (Suc n)"
    using Suc_dim li_Cons by auto
  thus ?case by blast
qed

lemma dimension_zero: "dimension 0 K E  E = { 𝟬 }"
proof -
  assume "dimension 0 K E"
  then obtain Vs where "length Vs = 0" "Span K Vs = E"
    using exists_base by blast
  thus ?thesis
    by auto
qed

lemma dimension_one [iff]: "dimension 1 K K"
proof -
  have "K = Span K [ 𝟭 ]"
    using line_extension_mem_iff[of _ K 𝟭 "{ 𝟬 }"] subfieldE(3)[OF K] by (auto simp add: rev_subsetD)
  thus ?thesis
    using dimension.Suc_dim[OF one_closed _ dimension.zero_dim, of K] subfieldE(6)[OF K] by auto 
qed

lemma dimensionI:
  assumes "independent K Us" "Span K Us = E"
  shows "dimension (length Us) K E"
  using dimension_independent[OF assms(1)] assms(2) by simp

lemma space_subgroup_props:
  assumes "dimension n K E"
  shows "E  carrier R"
    and "𝟬  E"
    and "v1 v2.  v1  E; v2  E   (v1  v2)  E"
    and "v. v  E  ( v)  E"
    and "k v.  k  K; v  E   k  v  E"
    and " k  K - { 𝟬 }; a  carrier R   k  a  E  a  E"
  using exists_base[OF assms] Span_subgroup_props Span_smult_closed Span_m_inv_simprule by auto

lemma independent_length_le_dimension:
  assumes "dimension n K E" and "independent K Us" "set Us  E"
  shows "length Us  n"
proof -
  obtain Vs where Vs: "set Vs  carrier R" "independent K Vs" "length Vs = n" "Span K Vs = E"
    using exists_base[OF assms(1)] by auto
  thus ?thesis
    using independent_length_le assms(2-3) by auto
qed

lemma dimension_is_inj:
  assumes "dimension n K E" and "dimension m K E"
  shows "n = m"
proof -
  { fix n m assume n: "dimension n K E" and m: "dimension m K E"
    then obtain Vs
      where Vs: "set Vs  carrier R" "independent K Vs" "length Vs = n" "Span K Vs = E"
      using exists_base by meson
    hence "n  m"
      using independent_length_le_dimension[OF m Vs(2)] Span_base_incl[OF Vs(1)] by auto
  } note aux_lemma = this

  show ?thesis
    using aux_lemma[OF assms] aux_lemma[OF assms(2,1)] by simp
qed

corollary independent_length_eq_dimension:
  assumes "dimension n K E" and "independent K Us" "set Us  E"
  shows "length Us = n  Span K Us = E"
proof
  assume len: "length Us = n" show "Span K Us = E"
  proof (rule ccontr)
    assume "Span K Us  E"
    hence "Span K Us  E"
      using mono_Span_subset[of Us] exists_base[OF assms(1)] assms(3) by blast
    then obtain v where v: "v  E" "v  Span K Us"
      using Span_strict_incl exists_base[OF assms(1)] space_subgroup_props(1)[OF assms(1)] assms by blast
    hence "independent K (v # Us)"
      using li_Cons[OF _ _ assms(2)] space_subgroup_props(1)[OF assms(1)] by auto
    hence "length (v # Us)  n"
      using independent_length_le_dimension[OF assms(1)] v(1) assms(2-3) by fastforce
    moreover have "length (v # Us) = Suc n"
      using len by simp
    ultimately show False by simp
  qed
next
  assume "Span K Us = E"
  hence "dimension (length Us) K E"
    using dimensionI assms by auto
  thus "length Us = n"
    using dimension_is_inj[OF assms(1)] by auto
qed

lemma complete_base:
  assumes "dimension n K E" and "independent K Us" "set Us  E"
  shows "Vs. length (Vs @ Us) = n  independent K (Vs @ Us)  Span K (Vs @ Us) = E"
proof -
  { fix Us k assume "k  n" "independent K Us" "set Us  E" "length Us = k"
    hence "Vs. length (Vs @ Us) = n  independent K (Vs @ Us)  Span K (Vs @ Us) = E"
    proof (induct arbitrary: Us rule: inc_induct)
      case base thus ?case
        using independent_length_eq_dimension[OF assms(1) base(1-2)] by auto
    next
      case (step m)
      have "Span K Us  E"
        using mono_Span_subset step(4-6) exists_base[OF assms(1)] by blast
      hence "Span K Us  E"
        using independent_length_eq_dimension[OF assms(1) step(4-5)] step(2,6) assms(1) by blast
      then obtain v where v: "v  E" "v  Span K Us"
        using Span_strict_incl exists_base[OF assms(1)] by blast
      hence "independent K (v # Us)"
        using space_subgroup_props(1)[OF assms(1)] li_Cons[OF _ v(2) step(4)] by auto
      then obtain Vs
        where "length (Vs @ (v # Us)) = n" "independent K (Vs @ (v # Us))" "Span K (Vs @ (v # Us)) = E"
        using step(3)[of "v # Us"] step(1-2,4-6) v by auto
      thus ?case
        by (metis append.assoc append_Cons append_Nil)
    qed } note aux_lemma = this

  have "length Us  n"
    using independent_length_le_dimension[OF assms] .
  thus ?thesis
    using aux_lemma[OF _ assms(2-3)] by auto
qed

lemma filter_base:
  assumes "set Us  carrier R"
  obtains Vs where "set Vs  carrier R" and "independent K Vs" and "Span K Vs = Span K Us"
proof -
  from set Us  carrier R have "Vs. independent K Vs  Span K Vs = Span K Us"
  proof (induction Us)
    case Nil thus ?case by auto
  next
    case (Cons u Us)
    then obtain Vs where Vs: "independent K Vs" "Span K Vs = Span K Us"
      by auto
    show ?case
    proof (cases "u  Span K Us")
      case True
      hence "Span K (u # Us) = Span K Us"
        using Span_base_incl mono_Span_subset
        by (metis Cons.prems insert_subset list.simps(15) subset_antisym)
      thus ?thesis
        using Vs by blast
    next
      case False
      hence "Span K (u # Vs) = Span K (u # Us)" and "independent K (u # Vs)"
        using li_Cons[of u K Vs] Cons(2) Vs by auto
      thus ?thesis
        by blast
    qed
  qed
  thus ?thesis
    using independent_in_carrier that by auto
qed

lemma dimension_backwards:
  "dimension (Suc n) K E  v  carrier R. E'. dimension n K E'  v  E'  E = line_extension K v E'"
  by (cases rule: dimension.cases) (auto)

lemma dimension_direct_sum_space:
  assumes "dimension n K E" and "dimension m K F" and "E  F = { 𝟬 }"
  shows "dimension (n + m) K (E <+>RF)"
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 <+>RF"
    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 <+>RF)"
    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 <+>RF)"
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) <+>RF  E <+>RF"
    using mono_Span_append(1)[OF in_carrier(1) Bs(1)] Us(3) unfolding set_add_def' by auto
  moreover have "E <+>RF  (Span K Us) <+>RF"
  proof
    fix v assume "v  E <+>RF"
    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) <+>RF"
      using u1' unfolding set_add_def' by auto
  qed
  ultimately have "Span K (Us @ (Vs @ Bs)) = E <+>RF"
    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 ] <+>RSpan 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 <+>RR.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) <+>Sh ` (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 (* of fixed K context. *)

end (* of ring_hom_ring context. *)

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 <+>RF)"
    and "((dim over K) (E <+>RF)) = ((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 <+>RF)"
    using dimension_sum_space[OF assms(1)] by simp
  thus "finite_dimension K (E <+>RF)"
   and "((dim over K) (E <+>RF)) = ((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