# Theory 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.)›
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]]
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.›
lemma (in module) smult_minus_1:
fixes v
assumes 0:"v∈carrier M"
shows "(⊖⇘R⇙ 𝟭⇘R⇙) ⊙⇘M⇙ v= (⊖⇘M⇙  v)"
proof -
from 0 have a0: "𝟭⇘R⇙ ⊙⇘M⇙ v = v" by simp
from 0 have 1: "((⊖⇘R⇙ 𝟭⇘R⇙)⊕⇘R⇙ 𝟭⇘R⇙) ⊙⇘M⇙ v=𝟬⇘M⇙"
from 0 have 2: "((⊖⇘R⇙ 𝟭⇘R⇙)⊕⇘R⇙ 𝟭⇘R⇙) ⊙⇘M⇙ v=(⊖⇘R⇙ 𝟭⇘R⇙) ⊙⇘M⇙ v ⊕⇘M⇙ 𝟭⇘R⇙⊙⇘M⇙ v"
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 "

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)"

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