(* Title: ZF/ex/Ring.thy
*)
section ‹Rings
›
theory Ring
imports Group
begin
no_notation cadd (
infixl ‹⊕› 65)
and cmult (
infixl ‹⊗› 70)
(*First, we must simulate a record declaration:
record ring = monoid +
add :: "[i, i] \<Rightarrow> i" (infixl "\<oplus>\<index>" 65)
zero :: i ("\<zero>\<index>")
*)
definition
add_field ::
"i \ i" where
"add_field(M) = fst(snd(snd(snd(M))))"
definition
ring_add ::
"[i, i, i] \ i" (
infixl ‹⊕🍋› 65)
where
"ring_add(M,x,y) = add_field(M) ` \x,y\"
definition
zero ::
"i \ i" (
‹0🍋›)
where
"zero(M) = fst(snd(snd(snd(snd(M)))))"
lemma add_field_eq [simp]:
"add_field() = A"
by (simp add: add_field_def)
lemma add_eq [simp]:
"ring_add(, x, y) = A ` \x,y\"
by (simp add: ring_add_def)
lemma zero_eq [simp]:
"zero() = Z"
by (simp add: zero_def)
text ‹Derived operations.
›
definition
a_inv ::
"[i,i] \ i" (
‹⊖🍋 _
› [81] 80)
where
"a_inv(R) \ m_inv ()"
definition
minus ::
"[i,i,i] \ i" (
‹(
‹notation=
‹infix ⊖››_
⊖🍋 _)
› [65,66] 65)
where
"\x \ carrier(R); y \ carrier(R)\ \ x \\<^bsub>R\<^esub> y = x \\<^bsub>R\<^esub> (\\<^bsub>R\<^esub> y)"
locale abelian_monoid =
fixes G (
structure)
assumes a_comm_monoid:
"comm_monoid ()"
text ‹
The following
definition is redundant but simple
to use.
›
locale abelian_group = abelian_monoid +
assumes a_comm_group:
"comm_group ()"
locale ring = abelian_group R + monoid R
for R (
structure) +
assumes l_distr:
"\x \ carrier(R); y \ carrier(R); z \ carrier(R)\
==> (x
⊕ y)
⋅ z = x
⋅ z
⊕ y
⋅ z
"
and r_distr:
"\x \ carrier(R); y \ carrier(R); z \ carrier(R)\
==> z
⋅ (x
⊕ y) = z
⋅ x
⊕ z
⋅ y
"
locale cring = ring + comm_monoid R
locale "domain" = cring +
assumes one_not_zero [simp]:
"\ \ \"
and integral:
"\a \ b = \; a \ carrier(R); b \ carrier(R)\ \
a =
0 | b =
0"
subsection ‹Basic Properties
›
lemma (
in abelian_monoid) a_monoid:
"monoid ()"
apply (insert a_comm_monoid)
apply (simp add: comm_monoid_def)
done
lemma (
in abelian_group) a_group:
"group ()"
apply (insert a_comm_group)
apply (simp add: comm_group_def group_def)
done
lemma (
in abelian_monoid) l_zero [simp]:
"x \ carrier(G) \ \ \ x = x"
apply (insert monoid.l_one [OF a_monoid])
apply (simp add: ring_add_def)
done
lemma (
in abelian_monoid) zero_closed [intro, simp]:
"\ \ carrier(G)"
by (rule monoid.one_closed [OF a_monoid, simplified])
lemma (
in abelian_group) a_inv_closed [intro, simp]:
"x \ carrier(G) \ \ x \ carrier(G)"
by (simp add: a_inv_def group.inv_closed [OF a_group, simplified])
lemma (
in abelian_monoid) a_closed [intro, simp]:
"\x \ carrier(G); y \ carrier(G)\ \ x \ y \ carrier(G)"
by (rule monoid.m_closed [OF a_monoid,
simplified, simplified ring_add_def [symmetric]])
lemma (
in abelian_group) minus_closed [intro, simp]:
"\x \ carrier(G); y \ carrier(G)\ \ x \ y \ carrier(G)"
by (simp add: minus_def)
lemma (
in abelian_group) a_l_cancel [simp]:
"\x \ carrier(G); y \ carrier(G); z \ carrier(G)\
==> (x
⊕ y = x
⊕ z)
⟷ (y = z)
"
by (rule group.l_cancel [OF a_group,
simplified, simplified ring_add_def [symmetric]])
lemma (
in abelian_group) a_r_cancel [simp]:
"\x \ carrier(G); y \ carrier(G); z \ carrier(G)\
==> (y
⊕ x = z
⊕ x)
⟷ (y = z)
"
by (rule group.r_cancel [OF a_group, simplified, simplified ring_add_def [symmetric]])
lemma (
in abelian_monoid) a_assoc:
"\x \ carrier(G); y \ carrier(G); z \ carrier(G)\
==> (x
⊕ y)
⊕ z = x
⊕ (y
⊕ z)
"
by (rule monoid.m_assoc [OF a_monoid, simplified, simplified ring_add_def [symmetric]])
lemma (
in abelian_group) l_neg:
"x \ carrier(G) \ \ x \ x = \"
by (simp add: a_inv_def
group.l_inv [OF a_group, simplified, simplified ring_add_def [symmetric]])
lemma (
in abelian_monoid) a_comm:
"\x \ carrier(G); y \ carrier(G)\ \ x \ y = y \ x"
by (rule comm_monoid.m_comm [OF a_comm_monoid,
simplified, simplified ring_add_def [symmetric]])
lemma (
in abelian_monoid) a_lcomm:
"\x \ carrier(G); y \ carrier(G); z \ carrier(G)\
==> x
⊕ (y
⊕ z) = y
⊕ (x
⊕ z)
"
by (rule comm_monoid.m_lcomm [OF a_comm_monoid,
simplified, simplified ring_add_def [symmetric]])
lemma (
in abelian_monoid) r_zero [simp]:
"x \ carrier(G) \ x \ \ = x"
using monoid.r_one [OF a_monoid]
by (simp add: ring_add_def [symmetric])
lemma (
in abelian_group) r_neg:
"x \ carrier(G) \ x \ (\ x) = \"
using group.r_inv [OF a_group]
by (simp add: a_inv_def ring_add_def [symmetric])
lemma (
in abelian_group) minus_zero [simp]:
"\ \ = \"
by (simp add: a_inv_def
group.inv_one [OF a_group, simplified ])
lemma (
in abelian_group) minus_minus [simp]:
"x \ carrier(G) \ \ (\ x) = x"
using group.inv_inv [OF a_group, simplified]
by (simp add: a_inv_def)
lemma (
in abelian_group) minus_add:
"\x \ carrier(G); y \ carrier(G)\ \ \ (x \ y) = \ x \ \ y"
using comm_group.inv_mult [OF a_comm_group]
by (simp add: a_inv_def ring_add_def [symmetric])
lemmas (
in abelian_monoid) a_ac = a_assoc a_comm a_lcomm
text ‹
The following proofs are
from Jacobson, Basic Algebra I, pp.
¬88--89
›
context ring
begin
lemma l_null [simp]:
"x \ carrier(R) \ \ \ x = \"
proof -
assume R:
"x \ carrier(R)"
then have "\ \ x \ \ \ x = (\ \ \) \ x"
by (blast intro: l_distr [
THEN sym])
also from R
have "... = \ \ x \ \" by simp
finally have "\ \ x \ \ \ x = \ \ x \ \" .
with R
show ?thesis
by (simp del: r_zero)
qed
lemma r_null [simp]:
"x \ carrier(R) \ x \ \ = \"
proof -
assume R:
"x \ carrier(R)"
then have "x \ \ \ x \ \ = x \ (\ \ \)"
by (simp add: r_distr del: l_zero r_zero)
also from R
have "... = x \ \ \ \" by simp
finally have "x \ \ \ x \ \ = x \ \ \ \" .
with R
show ?thesis
by (simp del: r_zero)
qed
lemma l_minus:
"\x \ carrier(R); y \ carrier(R)\ \ \ x \ y = \ (x \ y)"
proof -
assume R:
"x \ carrier(R)" "y \ carrier(R)"
then have "(\ x) \ y \ x \ y = (\ x \ x) \ y" by (simp add: l_distr)
also from R
have "... = \" by (simp add: l_neg)
finally have "(\ x) \ y \ x \ y = \" .
with R
have "(\ x) \ y \ x \ y \ \ (x \ y) = \ \ \ (x \ y)" by simp
with R
show ?thesis
by (simp add: a_assoc r_neg)
qed
lemma r_minus:
"\x \ carrier(R); y \ carrier(R)\ \ x \ \ y = \ (x \ y)"
proof -
assume R:
"x \ carrier(R)" "y \ carrier(R)"
then have "x \ (\ y) \ x \ y = x \ (\ y \ y)" by (simp add: r_distr)
also from R
have "... = \" by (simp add: l_neg)
finally have "x \ (\ y) \ x \ y = \" .
with R
have "x \ (\ y) \ x \ y \ \ (x \ y) = \ \ \ (x \ y)" by simp
with R
show ?thesis
by (simp add: a_assoc r_neg)
qed
lemma minus_eq:
"\x \ carrier(R); y \ carrier(R)\ \ x \ y = x \ \ y"
by (simp only: minus_def)
end
subsection ‹Morphisms›
definition
ring_hom ::
"[i,i] \ i" where
"ring_hom(R,S) \
{h
∈ carrier(R) -> carrier(S).
(
∀x y. x
∈ carrier(R)
∧ y
∈ carrier(R)
⟶
h ` (x
⋅🚫R
🚫 y) = (h ` x)
⋅🚫S
🚫 (h ` y)
∧
h ` (x
⊕🚫R
🚫 y) = (h ` x)
⊕🚫S
🚫 (h ` y))
∧
h `
1🚫R
🚫 =
1🚫S
🚫}
"
lemma ring_hom_memI:
assumes hom_type:
"h \ carrier(R) \ carrier(S)"
and hom_mult:
"\x y. \x \ carrier(R); y \ carrier(R)\ \
h ` (x
⋅🚫R
🚫 y) = (h ` x)
⋅🚫S
🚫 (h ` y)
"
and hom_add:
"\x y. \x \ carrier(R); y \ carrier(R)\ \
h ` (x
⊕🚫R
🚫 y) = (h ` x)
⊕🚫S
🚫 (h ` y)
"
and hom_one:
"h ` \\<^bsub>R\<^esub> = \\<^bsub>S\<^esub>"
shows "h \ ring_hom(R,S)"
by (auto simp add: ring_hom_def assms)
lemma ring_hom_closed:
"\h \ ring_hom(R,S); x \ carrier(R)\ \ h ` x \ carrier(S)"
by (auto simp add: ring_hom_def)
lemma ring_hom_mult:
"\h \ ring_hom(R,S); x \ carrier(R); y \ carrier(R)\
==> h ` (x
⋅🚫R
🚫 y) = (h ` x)
⋅🚫S
🚫 (h ` y)
"
by (simp add: ring_hom_def)
lemma ring_hom_add:
"\h \ ring_hom(R,S); x \ carrier(R); y \ carrier(R)\
==> h ` (x
⊕🚫R
🚫 y) = (h ` x)
⊕🚫S
🚫 (h ` y)
"
by (simp add: ring_hom_def)
lemma ring_hom_one:
"h \ ring_hom(R,S) \ h ` \\<^bsub>R\<^esub> = \\<^bsub>S\<^esub>"
by (simp add: ring_hom_def)
locale ring_hom_cring = R: cring R + S: cring S
for R (
structure)
and S (
structure)
and h +
assumes homh [simp, intro]:
"h \ ring_hom(R,S)"
notes hom_closed [simp, intro] = ring_hom_closed [OF homh]
and hom_mult [simp] = ring_hom_mult [OF homh]
and hom_add [simp] = ring_hom_add [OF homh]
and hom_one [simp] = ring_hom_one [OF homh]
lemma (
in ring_hom_cring) hom_zero [simp]:
"h ` \\<^bsub>R\<^esub> = \\<^bsub>S\<^esub>"
proof -
have "h ` \\<^bsub>R\<^esub> \\<^bsub>S\<^esub> h ` \ = h ` \\<^bsub>R\<^esub> \\<^bsub>S\<^esub> \\<^bsub>S\<^esub>"
by (simp add: hom_add [symmetric] del: hom_add)
then show ?thesis
by (simp del: S.r_zero)
qed
lemma (
in ring_hom_cring) hom_a_inv [simp]:
"x \ carrier(R) \ h ` (\\<^bsub>R\<^esub> x) = \\<^bsub>S\<^esub> h ` x"
proof -
assume R:
"x \ carrier(R)"
then have "h ` x \\<^bsub>S\<^esub> h ` (\ x) = h ` x \\<^bsub>S\<^esub> (\\<^bsub>S\<^esub> (h ` x))"
by (simp add: hom_add [symmetric] R.r_neg S.r_neg del: hom_add)
with R
show ?thesis
by simp
qed
lemma (
in ring) id_ring_hom [simp]:
"id(carrier(R)) \ ring_hom(R,R)"
apply (rule ring_hom_memI)
apply (auto simp add: id_type)
done
end
