section ‹Basic facts about rings and modules›
theory RingModuleFacts
imports Main
"HOL-Algebra.Module"
"HOL-Algebra.Coset"
begin
subsection ‹Basic facts›
text ‹In a field, every nonzero element has an inverse.›
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]]
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.›
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⇙"
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.›
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)
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$.›
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$.›
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.›
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.›
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.›
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