(* 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)