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: "a∈carrier R"  and h2: "a≠𝟬⇘R⇙"
  shows "inv⇘R⇙ a∈ 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: "m∈carrier M"
  shows "𝟬⇘R⇙⊙⇘M⇙ m=𝟬⇘M⇙"
proof - 
  from 1 have 0: "𝟬⇘R⇙⊙⇘M⇙ m∈carrier M" by simp
  from 1 have 2: "𝟬⇘R⇙⊙⇘M⇙ m = (𝟬⇘R⇙ ⊕⇘R⇙ 𝟬⇘R⇙) ⊙⇘M⇙ m" by simp
  from 1 have 3: "(𝟬⇘R⇙ ⊕⇘R⇙ 𝟬⇘R⇙) ⊙⇘M⇙ m=(𝟬⇘R⇙⊙⇘M⇙ m) ⊕⇘M⇙ (𝟬⇘R⇙⊙⇘M⇙ m)"  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: "𝟬⇘R⇙⊙⇘M⇙ m =(𝟬⇘R⇙⊙⇘M⇙ m) ⊕⇘M⇙ (𝟬⇘R⇙⊙⇘M⇙ m)" 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: "r∈carrier R"
  shows "r⊙⇘M⇙ 𝟬⇘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:"v∈carrier M"
  shows "(⊖⇘R⇙ 𝟭⇘R⇙) ⊙⇘M⇙ v= (⊖⇘M⇙  v)"
(*(simp add: M.l_neg)*)
proof -
  from 0 have a0: "𝟭⇘R⇙ ⊙⇘M⇙ v = v" by simp
  from 0 have 1: "((⊖⇘R⇙ 𝟭⇘R⇙)⊕⇘R⇙ 𝟭⇘R⇙) ⊙⇘M⇙ v=𝟬⇘M⇙" 
    by (simp add:R.l_neg)
  from 0 have 2: "((⊖⇘R⇙ 𝟭⇘R⇙)⊕⇘R⇙ 𝟭⇘R⇙) ⊙⇘M⇙ v=(⊖⇘R⇙ 𝟭⇘R⇙) ⊙⇘M⇙ v ⊕⇘M⇙ 𝟭⇘R⇙⊙⇘M⇙ v"
    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 ⊙⇘M⇙ x) = (a ⊗ b) ⊙⇘M⇙ x "
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: "r∈carrier R"
    from 1 2 have 3: "𝟭⇘R⇙⊗⇘R⇙ r = 𝟬⇘R⇙⊗⇘R⇙ r" 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]:
  "⟦a∈carrier G; b∈carrier G⟧ ⟹ (a⊖⇘G⇙b = 𝟬⇘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. x⊗⇘R⇙ y), 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