src/HOL/Algebra/Module.thy
changeset 68551 b680e74eb6f2
parent 61565 352c73a689da
child 68552 391e89e03eef
     1.1 --- a/src/HOL/Algebra/Module.thy	Fri Jun 29 23:04:36 2018 +0200
     1.2 +++ b/src/HOL/Algebra/Module.thy	Sat Jun 30 15:44:04 2018 +0100
     1.3 @@ -76,87 +76,95 @@
     1.4        "!!a x y. [| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
     1.5        (a \<odot>\<^bsub>M\<^esub> x) \<otimes>\<^bsub>M\<^esub> y = a \<odot>\<^bsub>M\<^esub> (x \<otimes>\<^bsub>M\<^esub> y)"
     1.6    shows "algebra R M"
     1.7 -apply intro_locales
     1.8 -apply (rule cring.axioms ring.axioms abelian_group.axioms comm_monoid.axioms assms)+
     1.9 -apply (rule module_axioms.intro)
    1.10 - apply (simp add: smult_closed)
    1.11 - apply (simp add: smult_l_distr)
    1.12 - apply (simp add: smult_r_distr)
    1.13 - apply (simp add: smult_assoc1)
    1.14 - apply (simp add: smult_one)
    1.15 -apply (rule cring.axioms ring.axioms abelian_group.axioms comm_monoid.axioms assms)+
    1.16 -apply (rule algebra_axioms.intro)
    1.17 - apply (simp add: smult_assoc2)
    1.18 -done
    1.19 +  apply intro_locales
    1.20 +             apply (rule cring.axioms ring.axioms abelian_group.axioms comm_monoid.axioms assms)+
    1.21 +      apply (rule module_axioms.intro)
    1.22 +          apply (simp add: smult_closed)
    1.23 +         apply (simp add: smult_l_distr)
    1.24 +        apply (simp add: smult_r_distr)
    1.25 +       apply (simp add: smult_assoc1)
    1.26 +      apply (simp add: smult_one)
    1.27 +     apply (rule cring.axioms ring.axioms abelian_group.axioms comm_monoid.axioms assms)+
    1.28 +  apply (rule algebra_axioms.intro)
    1.29 +  apply (simp add: smult_assoc2)
    1.30 +  done
    1.31  
    1.32 -lemma (in algebra) R_cring:
    1.33 -  "cring R"
    1.34 -  ..
    1.35 +lemma (in algebra) R_cring: "cring R" ..
    1.36  
    1.37 -lemma (in algebra) M_cring:
    1.38 -  "cring M"
    1.39 -  ..
    1.40 +lemma (in algebra) M_cring: "cring M" ..
    1.41  
    1.42 -lemma (in algebra) module:
    1.43 -  "module R M"
    1.44 -  by (auto intro: moduleI R_cring is_abelian_group
    1.45 -    smult_l_distr smult_r_distr smult_assoc1)
    1.46 +lemma (in algebra) module: "module R M"
    1.47 +  by (auto intro: moduleI R_cring is_abelian_group smult_l_distr smult_r_distr smult_assoc1)
    1.48  
    1.49  
    1.50 -subsection \<open>Basic Properties of Algebras\<close>
    1.51 +subsection \<open>Basic Properties of Modules\<close>
    1.52  
    1.53 -lemma (in algebra) smult_l_null [simp]:
    1.54 -  "x \<in> carrier M ==> \<zero> \<odot>\<^bsub>M\<^esub> x = \<zero>\<^bsub>M\<^esub>"
    1.55 -proof -
    1.56 -  assume M: "x \<in> carrier M"
    1.57 +lemma (in module) smult_l_null [simp]:
    1.58 + "x \<in> carrier M ==> \<zero> \<odot>\<^bsub>M\<^esub> x = \<zero>\<^bsub>M\<^esub>"
    1.59 +proof-
    1.60 +  assume M : "x \<in> carrier M"
    1.61    note facts = M smult_closed [OF R.zero_closed]
    1.62 -  from facts have "\<zero> \<odot>\<^bsub>M\<^esub> x = (\<zero> \<odot>\<^bsub>M\<^esub> x \<oplus>\<^bsub>M\<^esub> \<zero> \<odot>\<^bsub>M\<^esub> x) \<oplus>\<^bsub>M\<^esub> \<ominus>\<^bsub>M\<^esub> (\<zero> \<odot>\<^bsub>M\<^esub> x)" by algebra
    1.63 -  also from M have "... = (\<zero> \<oplus> \<zero>) \<odot>\<^bsub>M\<^esub> x \<oplus>\<^bsub>M\<^esub> \<ominus>\<^bsub>M\<^esub> (\<zero> \<odot>\<^bsub>M\<^esub> x)"
    1.64 -    by (simp add: smult_l_distr del: R.l_zero R.r_zero)
    1.65 -  also from facts have "... = \<zero>\<^bsub>M\<^esub>" apply algebra apply algebra done
    1.66 -  finally show ?thesis .
    1.67 +  from facts have "\<zero> \<odot>\<^bsub>M\<^esub> x = (\<zero> \<oplus> \<zero>) \<odot>\<^bsub>M\<^esub> x "
    1.68 +    using smult_l_distr by auto
    1.69 +  also have "... = \<zero> \<odot>\<^bsub>M\<^esub> x \<oplus>\<^bsub>M\<^esub> \<zero> \<odot>\<^bsub>M\<^esub> x"
    1.70 +    using smult_l_distr[of \<zero> \<zero> x] facts by auto
    1.71 +  finally show "\<zero> \<odot>\<^bsub>M\<^esub> x = \<zero>\<^bsub>M\<^esub>" using facts
    1.72 +    by (metis M.add.r_cancel_one')
    1.73  qed
    1.74  
    1.75 -lemma (in algebra) smult_r_null [simp]:
    1.76 +lemma (in module) smult_r_null [simp]:
    1.77    "a \<in> carrier R ==> a \<odot>\<^bsub>M\<^esub> \<zero>\<^bsub>M\<^esub> = \<zero>\<^bsub>M\<^esub>"
    1.78  proof -
    1.79    assume R: "a \<in> carrier R"
    1.80    note facts = R smult_closed
    1.81    from facts have "a \<odot>\<^bsub>M\<^esub> \<zero>\<^bsub>M\<^esub> = (a \<odot>\<^bsub>M\<^esub> \<zero>\<^bsub>M\<^esub> \<oplus>\<^bsub>M\<^esub> a \<odot>\<^bsub>M\<^esub> \<zero>\<^bsub>M\<^esub>) \<oplus>\<^bsub>M\<^esub> \<ominus>\<^bsub>M\<^esub> (a \<odot>\<^bsub>M\<^esub> \<zero>\<^bsub>M\<^esub>)"
    1.82 -    by algebra
    1.83 +    by (simp add: M.add.inv_solve_right)
    1.84    also from R have "... = a \<odot>\<^bsub>M\<^esub> (\<zero>\<^bsub>M\<^esub> \<oplus>\<^bsub>M\<^esub> \<zero>\<^bsub>M\<^esub>) \<oplus>\<^bsub>M\<^esub> \<ominus>\<^bsub>M\<^esub> (a \<odot>\<^bsub>M\<^esub> \<zero>\<^bsub>M\<^esub>)"
    1.85      by (simp add: smult_r_distr del: M.l_zero M.r_zero)
    1.86 -  also from facts have "... = \<zero>\<^bsub>M\<^esub>" by algebra
    1.87 +  also from facts have "... = \<zero>\<^bsub>M\<^esub>"
    1.88 +    by (simp add: M.r_neg)
    1.89    finally show ?thesis .
    1.90  qed
    1.91  
    1.92 -lemma (in algebra) smult_l_minus:
    1.93 -  "[| a \<in> carrier R; x \<in> carrier M |] ==> (\<ominus>a) \<odot>\<^bsub>M\<^esub> x = \<ominus>\<^bsub>M\<^esub> (a \<odot>\<^bsub>M\<^esub> x)"
    1.94 -proof -
    1.95 +lemma (in module) smult_l_minus:
    1.96 +"\<lbrakk> a \<in> carrier R; x \<in> carrier M \<rbrakk> \<Longrightarrow> (\<ominus>a) \<odot>\<^bsub>M\<^esub> x = \<ominus>\<^bsub>M\<^esub> (a \<odot>\<^bsub>M\<^esub> x)"
    1.97 +proof-
    1.98    assume RM: "a \<in> carrier R" "x \<in> carrier M"
    1.99    from RM have a_smult: "a \<odot>\<^bsub>M\<^esub> x \<in> carrier M" by simp
   1.100    from RM have ma_smult: "\<ominus>a \<odot>\<^bsub>M\<^esub> x \<in> carrier M" by simp
   1.101    note facts = RM a_smult ma_smult
   1.102    from facts have "(\<ominus>a) \<odot>\<^bsub>M\<^esub> x = (\<ominus>a \<odot>\<^bsub>M\<^esub> x \<oplus>\<^bsub>M\<^esub> a \<odot>\<^bsub>M\<^esub> x) \<oplus>\<^bsub>M\<^esub> \<ominus>\<^bsub>M\<^esub>(a \<odot>\<^bsub>M\<^esub> x)"
   1.103 -    by algebra
   1.104 +    by (simp add: M.add.inv_solve_right)
   1.105    also from RM have "... = (\<ominus>a \<oplus> a) \<odot>\<^bsub>M\<^esub> x \<oplus>\<^bsub>M\<^esub> \<ominus>\<^bsub>M\<^esub>(a \<odot>\<^bsub>M\<^esub> x)"
   1.106      by (simp add: smult_l_distr)
   1.107    also from facts smult_l_null have "... = \<ominus>\<^bsub>M\<^esub>(a \<odot>\<^bsub>M\<^esub> x)"
   1.108 -    apply algebra apply algebra done
   1.109 +    by (simp add: R.l_neg)
   1.110    finally show ?thesis .
   1.111  qed
   1.112  
   1.113 -lemma (in algebra) smult_r_minus:
   1.114 +lemma (in module) smult_r_minus:
   1.115    "[| a \<in> carrier R; x \<in> carrier M |] ==> a \<odot>\<^bsub>M\<^esub> (\<ominus>\<^bsub>M\<^esub>x) = \<ominus>\<^bsub>M\<^esub> (a \<odot>\<^bsub>M\<^esub> x)"
   1.116  proof -
   1.117    assume RM: "a \<in> carrier R" "x \<in> carrier M"
   1.118    note facts = RM smult_closed
   1.119    from facts have "a \<odot>\<^bsub>M\<^esub> (\<ominus>\<^bsub>M\<^esub>x) = (a \<odot>\<^bsub>M\<^esub> \<ominus>\<^bsub>M\<^esub>x \<oplus>\<^bsub>M\<^esub> a \<odot>\<^bsub>M\<^esub> x) \<oplus>\<^bsub>M\<^esub> \<ominus>\<^bsub>M\<^esub>(a \<odot>\<^bsub>M\<^esub> x)"
   1.120 -    by algebra
   1.121 +    by (simp add: M.add.inv_solve_right)
   1.122    also from RM have "... = a \<odot>\<^bsub>M\<^esub> (\<ominus>\<^bsub>M\<^esub>x \<oplus>\<^bsub>M\<^esub> x) \<oplus>\<^bsub>M\<^esub> \<ominus>\<^bsub>M\<^esub>(a \<odot>\<^bsub>M\<^esub> x)"
   1.123      by (simp add: smult_r_distr)
   1.124 -  also from facts smult_r_null have "... = \<ominus>\<^bsub>M\<^esub>(a \<odot>\<^bsub>M\<^esub> x)" by algebra
   1.125 +  also from facts smult_l_null have "... = \<ominus>\<^bsub>M\<^esub>(a \<odot>\<^bsub>M\<^esub> x)"
   1.126 +    by (metis M.add.inv_closed M.add.inv_solve_right M.l_neg R.zero_closed r_null smult_assoc1)
   1.127    finally show ?thesis .
   1.128  qed
   1.129  
   1.130 +lemma (in module) finsum_smult_ldistr:
   1.131 +  "\<lbrakk> finite A; a \<in> carrier R; f: A \<rightarrow> carrier M \<rbrakk> \<Longrightarrow>
   1.132 +     a \<odot>\<^bsub>M\<^esub> (\<Oplus>\<^bsub>M\<^esub> i \<in> A. (f i)) = (\<Oplus>\<^bsub>M\<^esub> i \<in> A. ( a \<odot>\<^bsub>M\<^esub> (f i)))"
   1.133 +proof (induct set: finite)
   1.134 +  case empty then show ?case
   1.135 +    by (metis M.finsum_empty M.zero_closed R.zero_closed r_null smult_assoc1 smult_l_null)
   1.136 +next
   1.137 +  case (insert x F) then show ?case
   1.138 +    by (simp add: Pi_def smult_r_distr)
   1.139 +qed
   1.140 +
   1.141  end