Theory More_Modules

(* Author: Alexander Maletzky *)

theory More_Modules
  imports HOL.Modules
begin

text ‹More facts about modules.›

section ‹Modules over Commutative Rings›

context module
begin

lemma scale_minus_both [simp]: "(- a) *s (- x) = a *s x"
  by simp

subsection ‹Submodules Spanned by Sets of Module-Elements›

lemma span_insertI:
  assumes "p ∈ span B"
  shows "p ∈ span (insert r B)"
proof -
  have "B ⊆ insert r B" by blast
  hence "span B ⊆ span (insert r B)" by (rule span_mono)
  with assms show ?thesis ..
qed

lemma span_insertD:
  assumes "p ∈ span (insert r B)" and "r ∈ span B"
  shows "p ∈ span B"
  using assms(1)
proof (induct p rule: span_induct_alt)
  case base
  show "0 ∈ span B" by (fact span_zero)
next
  case step: (step q b a)
  from step(1) have "b = r ∨ b ∈ B" by simp
  thus "q *s b + a ∈ span B"
  proof
    assume eq: "b = r"
    from step(2) assms(2) show ?thesis unfolding eq by (intro span_add span_scale)
  next
    assume "b ∈ B"
    hence "b ∈ span B" using span_superset ..
    with step(2) show ?thesis by (intro span_add span_scale)
  qed
qed

lemma span_insert_idI:
  assumes "r ∈ span B"
  shows "span (insert r B) = span B"
proof (intro subset_antisym subsetI)
  fix p
  assume "p ∈ span (insert r B)"
  from this assms show "p ∈ span B" by (rule span_insertD)
next
  fix p
  assume "p ∈ span B"
  thus "p ∈ span (insert r B)" by (rule span_insertI)
qed

lemma span_insert_zero: "span (insert 0 B) = span B"
  using span_zero by (rule span_insert_idI)

lemma span_Diff_zero: "span (B - {0}) = span B"
  by (metis span_insert_zero insert_Diff_single)

lemma span_insert_subset:
  assumes "span A ⊆ span B" and "r ∈ span B"
  shows "span (insert r A) ⊆ span B"
proof
  fix p
  assume "p ∈ span (insert r A)"
  thus "p ∈ span B"
  proof (induct p rule: span_induct_alt)
    case base
    show ?case by (fact span_zero)
  next
    case step: (step q b a)
    show ?case
    proof (intro span_add span_scale)
      from ‹b ∈ insert r A› show "b ∈ span B"
      proof
        assume "b = r"
        thus "b ∈ span B" using assms(2) by simp
      next
        assume "b ∈ A"
        hence "b ∈ span A" using span_superset ..
        thus "b ∈ span B" using assms(1) ..
      qed
    qed fact
  qed
qed

lemma replace_span:
  assumes "q ∈ span B"
  shows "span (insert q (B - {p})) ⊆ span B"
  by (rule span_insert_subset, rule span_mono, fact Diff_subset, fact)

lemma sum_in_spanI: "(∑b∈B. q b *s b) ∈ span B"
  by (auto simp: intro: span_sum span_scale dest: span_base)

lemma span_closed_sum_list: "(⋀x. x ∈ set xs ⟹ x ∈ span B) ⟹ sum_list xs ∈ span B"
  by (induct xs) (auto intro: span_zero span_add)

lemma spanE:
  assumes "p ∈ span B"
  obtains A q where "finite A" and "A ⊆ B" and "p = (∑b∈A. (q b) *s b)"
  using assms by (auto simp: span_explicit)

lemma span_finite_subset:
  assumes "p ∈ span B"
  obtains A where "finite A" and "A ⊆ B" and "p ∈ span A"
proof -
  from assms obtain A q where "finite A" and "A ⊆ B" and p: "p = (∑a∈A. q a *s a)"
    by (rule spanE)
  note this(1, 2)
  moreover have "p ∈ span A" unfolding p by (rule sum_in_spanI)
  ultimately show ?thesis ..
qed

lemma span_finiteE:
  assumes "finite B" and "p ∈ span B"
  obtains q where "p = (∑b∈B. (q b) *s b)"
  using assms by (auto simp: span_finite)

lemma span_subset_spanI:
  assumes "A ⊆ span B"
  shows "span A ⊆ span B"
  using assms subspace_span by (rule span_minimal)

lemma span_insert_cong:
  assumes "span A = span B"
  shows "span (insert p A) = span (insert p B)" (is "?l = ?r")
proof
  have 1: "span (insert p C1) ⊆ span (insert p C2)" if "span C1 = span C2" for C1 C2
  proof (rule span_subset_spanI)
    show "insert p C1 ⊆ span (insert p C2)"
    proof (rule insert_subsetI)
      show "p ∈ span (insert p C2)" by (rule span_base) simp
    next
      have "C1 ⊆ span C1" by (rule span_superset)
      also from that have "… = span C2" .
      also have "… ⊆ span (insert p C2)" by (rule span_mono) blast
      finally show "C1 ⊆ span (insert p C2)" .
    qed
  qed
  from assms show "?l ⊆ ?r" by (rule 1)
  from assms[symmetric] show "?r ⊆ ?l" by (rule 1)
qed

lemma span_induct' [consumes 1, case_names base step]:
  assumes "p ∈ span B" and "P 0"
    and "⋀a q p. a ∈ span B ⟹ P a ⟹ p ∈ B ⟹ q ≠ 0 ⟹ P (a + q *s p)"
  shows "P p"
  using assms(1, 1)
proof (induct p rule: span_induct_alt)
  case base
  from assms(2) show ?case .
next
  case (step q b a)
  from step.hyps(1) have "b ∈ span B" by (rule span_base)
  hence "q *s b ∈ span B" by (rule span_scale)
  with step.prems have "a ∈ span B" by (simp only: span_add_eq)
  hence "P a" by (rule step.hyps)
  show ?case
  proof (cases "q = 0")
    case True
    from ‹P a› show ?thesis by (simp add: True)
  next
    case False
    with ‹a ∈ span B› ‹P a› step.hyps(1) have "P (a + q *s b)" by (rule assms(3))
    thus ?thesis by (simp only: add.commute)
  qed
qed

lemma span_INT_subset: "span (⋂a∈A. f a) ⊆ (⋂a∈A. span (f a))" (is "?l ⊆ ?r")
proof
  fix p
  assume "p ∈ ?l"
  show "p ∈ ?r"
  proof
    fix a
    assume "a ∈ A"
    from ‹p ∈ ?l› show "p ∈ span (f a)"
    proof (induct p rule: span_induct')
      case base
      show ?case by (fact span_zero)
    next
      case (step p q b)
      from step(3) ‹a ∈ A› have "b ∈ f a" ..
      hence "b ∈ span (f a)" by (rule span_base)
      with step(2) show ?case by (intro span_add span_scale)
    qed
  qed
qed

lemma span_INT: "span (⋂a∈A. span (f a)) = (⋂a∈A. span (f a))" (is "?l = ?r")
proof
  have "?l ⊆ (⋂a∈A. span (span (f a)))" by (rule span_INT_subset)
  also have "... = ?r" by (simp add: span_span)
  finally show "?l ⊆ ?r" .
qed (fact span_superset)

lemma span_Int_subset: "span (A ∩ B) ⊆ span A ∩ span B"
proof -
  have "span (A ∩ B) = span (⋂x∈{A, B}. x)" by simp
  also have "… ⊆ (⋂x∈{A, B}. span x)" by (fact span_INT_subset)
  also have "… = span A ∩ span B" by simp
  finally show ?thesis .
qed

lemma span_Int: "span (span A ∩ span B) = span A ∩ span B"
proof -
  have "span (span A ∩ span B) = span (⋂x∈{A, B}. span x)" by simp
  also have "… = (⋂x∈{A, B}. span x)" by (fact span_INT)
  also have "… = span A ∩ span B" by simp
  finally show ?thesis .
qed

lemma span_image_scale_eq_image_scale: "span ((*s) q ` F) = (*s) q ` span F" (is "?A = ?B")
proof (intro subset_antisym subsetI)
  fix p
  assume "p ∈ ?A"
  thus "p ∈ ?B"
  proof (induct p rule: span_induct')
    case base
    from span_zero show ?case by (rule rev_image_eqI) simp
  next
    case (step p r a)
    from step.hyps(2) obtain p' where "p' ∈ span F" and p: "p = q *s p'" ..
    from step.hyps(3) obtain a' where "a' ∈ F" and a: "a = q *s a'" ..
    from this(1) have "a' ∈ span F" by (rule span_base)
    hence "r *s a' ∈ span F" by (rule span_scale)
    with ‹p' ∈ span F› have "p' + r *s a' ∈ span F" by (rule span_add)
    hence "q *s (p' + r *s a') ∈ ?B" by (rule imageI)
    also have "q *s (p' + r *s a') = p + r *s a" by (simp add: a p algebra_simps)
    finally show ?case .
  qed
next
  fix p
  assume "p ∈ ?B"
  then obtain p' where "p' ∈ span F" and "p = q *s p'" ..
  from this(1) show "p ∈ ?A" unfolding ‹p = q *s p'›
  proof (induct p' rule: span_induct')
    case base
    show ?case by (simp add: span_zero)
  next
    case (step p r a)
    from step.hyps(3) have "q *s a ∈ (*s) q ` F" by (rule imageI)
    hence "q *s a ∈ ?A" by (rule span_base)
    hence "r *s (q *s a) ∈ ?A" by (rule span_scale)
    with step.hyps(2) have "q *s p + r *s (q *s a) ∈ ?A" by (rule span_add)
    also have "q *s p + r *s (q *s a) = q *s (p + r *s a)" by (simp add: algebra_simps)
    finally show ?case .
  qed
qed

end (* module *)

section ‹Ideals over Commutative Rings›

lemma module_times: "module (*)"
  by (standard, simp_all add: algebra_simps)

interpretation ideal: module times
  by (fact module_times)

declare ideal.scale_scale[simp del]

abbreviation "ideal ≡ ideal.span"

lemma ideal_eq_UNIV_iff_contains_one: "ideal B = UNIV ⟷ 1 ∈ ideal B"
proof
  assume *: "1 ∈ ideal B"
  show "ideal B = UNIV"
  proof
    show "UNIV ⊆ ideal B"
    proof
      fix x
      from * have "x * 1 ∈ ideal B" by (rule ideal.span_scale)
      thus "x ∈ ideal B" by simp
    qed
  qed simp
qed simp

lemma ideal_eq_zero_iff [iff]: "ideal F = {0} ⟷ F ⊆ {0}"
  by (metis empty_subsetI ideal.span_empty ideal.span_eq)

lemma ideal_field_cases:
  obtains "ideal B = {0}" | "ideal (B::'a::field set) = UNIV"
proof (cases "ideal B = {0}")
  case True
  thus ?thesis ..
next
  case False
  hence "¬ B ⊆ {0}" by simp
  then obtain b where "b ∈ B" and "b ≠ 0" by blast
  from this(1) have "b ∈ ideal B" by (rule ideal.span_base)
  hence "inverse b * b ∈ ideal B" by (rule ideal.span_scale)
  with ‹b ≠ 0› have "ideal B = UNIV" by (simp add: ideal_eq_UNIV_iff_contains_one)
  thus ?thesis ..
qed

corollary ideal_field_disj: "ideal B = {0} ∨ ideal (B::'a::field set) = UNIV"
  by (rule ideal_field_cases) blast+

lemma image_ideal_subset:
  assumes "⋀x y. h (x + y) = h x + h y" and "⋀x y. h (x * y) = h x * h y"
  shows "h ` ideal F ⊆ ideal (h ` F)"
proof (intro subsetI, elim imageE)
  fix g f
  assume g: "g = h f"
  assume "f ∈ ideal F"
  thus "g ∈ ideal (h ` F)" unfolding g
  proof (induct f rule: ideal.span_induct_alt)
    case base
    have "h 0 = h (0 + 0)" by simp
    also have "… = h 0 + h 0" by (simp only: assms(1))
    finally show ?case by (simp add: ideal.span_zero)
  next
    case (step c f g)
    from step.hyps(1) have "h f ∈ ideal (h ` F)"
      by (intro ideal.span_base imageI)
    hence "h c * h f ∈ ideal (h ` F)" by (rule ideal.span_scale)
    hence "h c * h f + h g ∈ ideal (h ` F)"
      using step.hyps(2) by (rule ideal.span_add)
    thus ?case by (simp only: assms)
  qed
qed

lemma image_ideal_eq_surj:
  assumes "⋀x y. h (x + y) = h x + h y" and "⋀x y. h (x * y) = h x * h y" and "surj h"
  shows "h ` ideal B = ideal (h ` B)"
proof
  from assms(1, 2) show "h ` ideal B ⊆ ideal (h ` B)" by (rule image_ideal_subset)
next
  show "ideal (h ` B) ⊆ h ` ideal B"
  proof
    fix b
    assume "b ∈ ideal (h ` B)"
    thus "b ∈ h ` ideal B"
    proof (induct b rule: ideal.span_induct_alt)
      case base
      have "h 0 = h (0 + 0)" by simp
      also have "… = h 0 + h 0" by (simp only: assms(1))
      finally have "0 = h 0" by simp
      with ideal.span_zero show ?case by (rule rev_image_eqI)
    next
      case (step c b a)
      from assms(3) obtain c' where c: "c = h c'" by (rule surjE)
      from step.hyps(2) obtain a' where "a' ∈ ideal B" and a: "a = h a'" ..
      from step.hyps(1) obtain b' where "b' ∈ B" and b: "b = h b'" ..
      from this(1) have "b' ∈ ideal B" by (rule ideal.span_base)
      hence "c' * b' ∈ ideal B" by (rule ideal.span_scale)
      hence "c' * b' + a' ∈ ideal B" using ‹a' ∈ _› by (rule ideal.span_add)
      moreover have "c * b + a = h (c' * b' + a')"
        by (simp add: c b a assms(1, 2))
      ultimately show ?case by (rule rev_image_eqI)
    qed
  qed
qed

context
  fixes h :: "'a ⇒ 'a::comm_ring_1"
  assumes h_plus: "h (x + y) = h x + h y"
  assumes h_times: "h (x * y) = h x * h y"
  assumes h_idem: "h (h x) = h x"
begin

lemma in_idealE_homomorphism_finite:
  assumes "finite B" and "B ⊆ range h" and "p ∈ range h" and "p ∈ ideal B"
  obtains q where "⋀b. q b ∈ range h" and "p = (∑b∈B. q b * b)"
proof -
  from assms(1, 4) obtain q0 where p: "p = (∑b∈B. q0 b * b)" by (rule ideal.span_finiteE)
  define q where "q = (λb. h (q0 b))"
  show ?thesis
  proof
    fix b
    show "q b ∈ range h" unfolding q_def by (rule rangeI)
  next
    from assms(3) obtain p' where "p = h p'" ..
    hence "p = h p" by (simp only: h_idem)
    also from ‹finite B› have "… = (∑b∈B. q b * h b)" unfolding p
    proof (induct B)
      case empty
      have "h 0 = h (0 + 0)" by simp
      also have "… = h 0 + h 0" by (simp only: h_plus)
      finally show ?case by simp
    next
      case (insert b B)
      thus ?case by (simp add: h_plus h_times q_def)
    qed
    also from refl have "… = (∑b∈B. q b * b)"
    proof (rule sum.cong)
      fix b
      assume "b ∈ B"
      hence "b ∈ range h" using assms(2) ..
      then obtain b' where "b = h b'" ..
      thus "q b * h b = q b * b" by (simp only: h_idem)
    qed
    finally show "p = (∑b∈B. q b * b)" .
  qed
qed

corollary in_idealE_homomorphism:
  assumes "B ⊆ range h" and "p ∈ range h" and "p ∈ ideal B"
  obtains A q where "finite A" and "A ⊆ B" and "⋀b. q b ∈ range h" and "p = (∑b∈A. q b * b)"
proof -
  from assms(3) obtain A where "finite A" and "A ⊆ B" and "p ∈ ideal A"
    by (rule ideal.span_finite_subset)
  from this(2) assms(1) have "A ⊆ range h" by (rule subset_trans)
  with ‹finite A› obtain q where "⋀b. q b ∈ range h" and "p = (∑b∈A. q b * b)"
    using assms(2) ‹p ∈ ideal A› by (rule in_idealE_homomorphism_finite) blast
  with ‹finite A› ‹A ⊆ B› show ?thesis ..
qed

lemma ideal_induct_homomorphism [consumes 3, case_names 0 plus]:
  assumes "B ⊆ range h" and "p ∈ range h" and "p ∈ ideal B"
  assumes "P 0" and "⋀c b a. c ∈ range h ⟹ b ∈ B ⟹ P a ⟹ a ∈ range h ⟹ P (c * b + a)"
  shows "P p"
proof -
  from assms(1-3) obtain A q where "finite A" and "A ⊆ B" and rl: "⋀f. q f ∈ range h"
    and p: "p = (∑f∈A. q f * f)" by (rule in_idealE_homomorphism) blast
  show ?thesis unfolding p using ‹finite A› ‹A ⊆ B›
  proof (induct A)
    case empty
    from assms(4) show ?case by simp
  next
    case (insert a A)
    from insert.hyps(1, 2) have "(∑f∈insert a A. q f * f) = q a * a + (∑f∈A. q f * f)" by simp
    also from rl have "P …"
    proof (rule assms(5))
      have "a ∈ insert a A" by simp
      thus "a ∈ B" using insert.prems ..
    next
      from insert.prems have "A ⊆ B" by simp
      thus "P (∑f∈A. q f * f)" by (rule insert.hyps)
    next
      from insert.prems have "A ⊆ B" by simp
      hence "A ⊆ range h" using assms(1) by (rule subset_trans)
      with ‹finite A› show "(∑f∈A. q f * f) ∈ range h"
      proof (induct A)
        case empty
        have "h 0 = h (0 + 0)" by simp
        also have "… = h 0 + h 0" by (simp only: h_plus)
        finally have "(∑f∈{}. q f * f) = h 0" by simp
        thus ?case by (rule image_eqI) simp
      next
        case (insert a A)
        from insert.prems have "a ∈ range h" and "A ⊆ range h" by simp_all
        from this(1) obtain a' where a: "a = h a'" ..
        from ‹q a ∈ range h› obtain q' where q: "q a = h q'" ..
        from ‹A ⊆ _› have "(∑f∈A. q f * f) ∈ range h" by (rule insert.hyps)
        then obtain m where eq: "(∑f∈A. q f * f) = h m" ..
        from insert.hyps(1, 2) have "(∑f∈insert a A. q f * f) = q a * a + (∑f∈A. q f * f)" by simp
        also have "… = h (q' * a' + m)" unfolding q by (simp add: a eq h_plus h_times)
        also have "… ∈ range h" by (rule rangeI)
        finally show ?case .
      qed
    qed
    finally show ?case .
  qed
qed

lemma image_ideal_eq_Int: "h ` ideal B = ideal (h ` B) ∩ range h"
proof
  from h_plus h_times have "h ` ideal B ⊆ ideal (h ` B)" by (rule image_ideal_subset)
  thus "h ` ideal B ⊆ ideal (h ` B) ∩ range h" by blast
next
  show "ideal (h ` B) ∩ range h ⊆ h ` ideal B"
  proof
    fix b
    assume "b ∈ ideal (h ` B) ∩ range h"
    hence "b ∈ ideal (h ` B)" and "b ∈ range h" by simp_all
    have "h ` B ⊆ range h" by blast
    thus "b ∈ h ` ideal B" using ‹b ∈ range h› ‹b ∈ ideal (h ` B)›
    proof (induct b rule: ideal_induct_homomorphism)
      case 0
      have "h 0 = h (0 + 0)" by simp
      also have "… = h 0 + h 0" by (simp only: h_plus)
      finally have "0 = h 0" by simp
      with ideal.span_zero show ?case by (rule rev_image_eqI)
    next
      case (plus c b a)
      from plus.hyps(1) obtain c' where c: "c = h c'" ..
      from plus.hyps(3) obtain a' where "a' ∈ ideal B" and a: "a = h a'" ..
      from plus.hyps(2) obtain b' where "b' ∈ B" and b: "b = h b'" ..
      from this(1) have "b' ∈ ideal B" by (rule ideal.span_base)
      hence "c' * b' ∈ ideal B" by (rule ideal.span_scale)
      hence "c' * b' + a' ∈ ideal B" using ‹a' ∈ _› by (rule ideal.span_add)
      moreover have "c * b + a = h (c' * b' + a')" by (simp add: a b c h_plus h_times)
      ultimately show ?case by (rule rev_image_eqI)
    qed
  qed
qed

end

end (* theory *)