src/HOL/Algebra/Module.thy

 next
   case (insert x F) then show ?case
     by (simp add: Pi_def smult_r_distr)
 qed
 
+
+
+subsection \<open>Submodules\<close>
+
+locale submodule = subgroup H "add_monoid M" for H and R :: "('a, 'b) ring_scheme" and M (structure)
++ assumes smult_closed [simp, intro]:
+      "\<lbrakk>a \<in> carrier R; x \<in> H\<rbrakk> \<Longrightarrow> a \<odot>\<^bsub>M\<^esub> x \<in> H"
+
+
+lemma (in module) submoduleI :
+  assumes subset: "H \<subseteq> carrier M"
+    and zero: "\<zero>\<^bsub>M\<^esub> \<in> H"
+    and a_inv: "!!a. a \<in> H \<Longrightarrow> \<ominus>\<^bsub>M\<^esub> a \<in> H"
+    and add : "\<And> a b. \<lbrakk>a \<in> H ; b \<in> H\<rbrakk> \<Longrightarrow> a \<oplus>\<^bsub>M\<^esub> b \<in> H"
+    and smult_closed : "\<And> a x. \<lbrakk>a \<in> carrier R; x \<in> H\<rbrakk> \<Longrightarrow> a \<odot>\<^bsub>M\<^esub> x \<in> H"
+  shows "submodule H R M"
+  apply (intro submodule.intro subgroup.intro)
+  using assms unfolding submodule_axioms_def
+  by (simp_all add : a_inv_def)
+
+
+lemma (in module) submoduleE :
+  assumes "submodule H R M"
+  shows "H \<subseteq> carrier M"
+    and "H \<noteq> {}"
+    and "\<And>a. a \<in> H \<Longrightarrow> \<ominus>\<^bsub>M\<^esub> a \<in> H"
+    and "\<And>a b. \<lbrakk>a \<in> carrier R; b \<in> H\<rbrakk> \<Longrightarrow> a \<odot>\<^bsub>M\<^esub> b \<in> H"
+    and "\<And> a b. \<lbrakk>a \<in> H ; b \<in> H\<rbrakk> \<Longrightarrow> a \<oplus>\<^bsub>M\<^esub> b \<in> H"
+    and "\<And> x. x \<in> H \<Longrightarrow> (a_inv M x) \<in> H"
+  using group.subgroupE[of "add_monoid M" H, OF _ submodule.axioms(1)[OF assms]] a_comm_group
+        submodule.smult_closed[OF assms]
+  unfolding comm_group_def a_inv_def
+  by auto
+
+
+lemma (in module) carrier_is_submodule :
+"submodule (carrier M) R M"
+  apply (intro  submoduleI)
+  using a_comm_group group.inv_closed unfolding comm_group_def a_inv_def group_def monoid_def
+  by auto
+
+lemma (in submodule) submodule_is_module :
+  assumes "module R M"
+  shows "module R (M\<lparr>carrier := H\<rparr>)"
+proof (auto intro! : moduleI abelian_group.intro)
+  show "cring (R)" using assms unfolding module_def by auto
+  show "abelian_monoid (M\<lparr>carrier := H\<rparr>)"
+    using comm_monoid.submonoid_is_comm_monoid[OF _ subgroup_is_submonoid] assms
+    unfolding abelian_monoid_def module_def abelian_group_def
+    by auto
+  thus "abelian_group_axioms (M\<lparr>carrier := H\<rparr>)"
+    using subgroup_is_group assms
+    unfolding abelian_group_axioms_def comm_group_def abelian_monoid_def module_def abelian_group_def
+    by auto
+  show "\<And>z. z \<in> H \<Longrightarrow> \<one>\<^bsub>R\<^esub> \<odot> z = z"
+    using subgroup_imp_subset[OF subgroup_axioms] module.smult_one[OF assms]
+    by auto
+  fix a b x y assume a : "a \<in> carrier R" and b : "b \<in> carrier R" and x : "x \<in> H" and y : "y \<in> H"
+  show "(a \<oplus>\<^bsub>R\<^esub> b) \<odot> x = a \<odot> x \<oplus> b \<odot> x"
+    using a b x module.smult_l_distr[OF assms] subgroup_imp_subset[OF subgroup_axioms]
+    by auto
+  show "a \<odot> (x \<oplus> y) = a \<odot> x \<oplus> a \<odot> y"
+    using a x y module.smult_r_distr[OF assms] subgroup_imp_subset[OF subgroup_axioms]
+    by auto
+  show "a \<otimes>\<^bsub>R\<^esub> b \<odot> x = a \<odot> (b \<odot> x)"
+    using a b x module.smult_assoc1[OF assms] subgroup_imp_subset[OF subgroup_axioms]
+    by auto
+qed
+
+
+lemma (in module) module_incl_imp_submodule :
+  assumes "H \<subseteq> carrier M"
+    and "module R (M\<lparr>carrier := H\<rparr>)"
+  shows "submodule H R M"
+  apply (intro submodule.intro)
+  using add.group_incl_imp_subgroup[OF assms(1)] assms module.axioms(2)[OF assms(2)]
+        module.smult_closed[OF assms(2)]
+  unfolding abelian_group_def abelian_group_axioms_def comm_group_def submodule_axioms_def
+  by simp_all
+
+
 end