Theory VectorSpace.RingModuleFacts

section ‹Basic facts about rings and modules›

theory RingModuleFacts
imports Main
  "HOL-Algebra.Module"
  "HOL-Algebra.Coset"
  (*MonoidSums*)
begin

subsection ‹Basic facts›
text ‹In a field, every nonzero element has an inverse.› (* Add to Ring.*)
lemma (in field) inverse_exists [simp, intro]: 
  assumes h1: "acarrier R"  and h2: "a𝟬R⇙"
  shows "invRa carrier R"
proof - 
  have 1: "Units R = carrier R - {𝟬R} " by (rule field_Units)
  from h1 h2 1 show ?thesis by auto
qed

text ‹Multiplication by 0 in $R$ gives 0. (Note that this fact encompasses smult-l-null 
as this is for module while that is for algebra, so smult-l-null is redundant.)›
(*Add to Module. *)
lemma (in module) lmult_0 [simp]:
  assumes 1: "mcarrier M"
  shows "𝟬RMm=𝟬M⇙"
proof - 
  from 1 have 0: "𝟬RMmcarrier M" by simp
  from 1 have 2: "𝟬RMm = (𝟬RR𝟬R) Mm" by simp
  from 1 have 3: "(𝟬RR𝟬R) Mm=(𝟬RMm) M(𝟬RMm)"  using [[simp_trace, simp_trace_depth_limit=3]]
    by (simp add: smult_l_distr del: R.add.r_one R.add.l_one)
  from 2 3 have 4: "𝟬RMm =(𝟬RMm) M(𝟬RMm)" by auto
  from 0 4 show ?thesis
    using M.l_neg M.r_neg1 by fastforce
qed

text ‹Multiplication by 0 in $M$ gives 0.› (*Add to Module.*)
lemma (in module) rmult_0 [simp]:
  assumes 0: "rcarrier R"
  shows "rM𝟬M=𝟬M⇙"
by (metis M.zero_closed R.zero_closed assms lmult_0 r_null smult_assoc1)

text ‹Multiplication by $-1$ is the same as negation. May be useful as a simp rule.›
(*Add to module.*)
lemma (in module) smult_minus_1:
  fixes v
  assumes 0:"vcarrier M"
  shows "(R𝟭R) Mv= (Mv)"
(*(simp add: M.l_neg)*)
proof -
  from 0 have a0: "𝟭RMv = v" by simp
  from 0 have 1: "((R𝟭R)R𝟭R) Mv=𝟬M⇙" 
    by (simp add:R.l_neg)
  from 0 have 2: "((R𝟭R)R𝟭R) Mv=(R𝟭R) Mv M𝟭RMv"
    by (simp add: smult_l_distr)
  from 1 2 show ?thesis by (metis M.minus_equality R.add.inv_closed 
    a0 assms one_closed smult_closed) 
qed

text ‹The version with equality reversed.›
lemmas (in module)  smult_minus_1_back = smult_minus_1[THEN sym]

text‹-1 is not 0›
lemma (in field) neg_1_not_0 [simp]: "R𝟭R 𝟬R⇙"
by (metis minus_minus minus_zero one_closed zero_not_one) 

text ‹Note smult-assoc1 is the wrong way around for simplification.
This is the reverse of smult-assoc1.›(*Add to Module. *)
lemma (in module) smult_assoc_simp:
"[| a  carrier R; b  carrier R; x  carrier M |] ==>
      a M(b Mx) = (a  b) Mx "
by (auto simp add: smult_assoc1)
  
(* Add to Ring? *)
lemmas (in abelian_group) show_r_zero= add.l_cancel_one
lemmas (in abelian_group) show_l_zero= add.r_cancel_one

text ‹A nontrivial ring has $0\neq 1$.›(*Add to Ring.*)
lemma (in ring) nontrivial_ring [simp]:
  assumes "carrier R{𝟬R}"
  shows "𝟬R𝟭R⇙"
proof (rule ccontr)
  assume 1: "¬(𝟬R𝟭R)"
  {
    fix r
    assume 2: "rcarrier R"
    from 1 2 have 3: "𝟭RRr = 𝟬RRr" by auto
    from 2 3 have "r = 𝟬R⇙" by auto
  }
  from this assms show False by auto
qed

text ‹Use as simp rule. To show $a-b=0$, it suffices to show $a=b$.›(*Add to Ring.*)
lemma (in abelian_group) minus_other_side [simp]:
  "acarrier G; bcarrier G  (aGb = 𝟬G) = (a=b)"
  by (metis a_minus_def add.inv_closed add.m_comm r_neg r_neg2)

subsection ‹Units group›
text ‹Define the units group $R^{\times}$ and show it is actually a group.›(* Add to Ring.*)
definition units_group::"('a,'b) ring_scheme  'a monoid"
  where "units_group R = carrier = Units R, mult = (λx y. xRy), one = 𝟭R"

text ‹The units form a group.›(*Add to Ring.*)
lemma (in ring) units_form_group: "group (units_group R)"
  apply (intro groupI)
  apply (unfold units_group_def, auto)
  apply (intro m_assoc) 
  apply auto
  apply (unfold Units_def) 
  apply auto
  done

text ‹The units of a cring› form a commutative group.›(* Add to Ring.*)
lemma (in cring) units_form_cgroup: "comm_group (units_group R)"
  apply (intro comm_groupI)
  apply (unfold units_group_def) apply auto
  apply (intro m_assoc) apply auto
  apply (unfold Units_def) apply auto
  apply (rule m_comm) apply auto
  done



end