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: "(bB. 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 = (bA. (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 = (aA. 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 = (bB. (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 (aA. f a)  (aA. 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 (aA. span (f a)) = (aA. span (f a))" (is "?l = ?r")
proof
  have "?l  (aA. 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 = (bB. q b * b)"
proof -
  from assms(1, 4) obtain q0 where p: "p = (bB. 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 " = (bB. 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 " = (bB. 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 = (bB. 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 = (bA. 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 = (bA. 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 = (fA. 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 "(finsert a A. q f * f) = q a * a + (fA. 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 (fA. 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 "(fA. 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 "(fA. q f * f)  range h" by (rule insert.hyps)
        then obtain m where eq: "(fA. q f * f) = h m" ..
        from insert.hyps(1, 2) have "(finsert a A. q f * f) = q a * a + (fA. 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 *)