# Theory Polynomials.More_Modules

(* Author: Alexander Maletzky *)

theory More_Modules
imports HOL.Modules
begin

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
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:

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:
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)"
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 *)