Theory Ring

theory Ring
imports Group
(* Title:  ZF/ex/Ring.thy

*)


header {* 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] => i" (infixl "⊕\<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 "⊕\<index>" 65) where
"ring_add(M,x,y) = add_field(M) ` <x,y>"

definition
zero :: "i => i" ("\<zero>\<index>") where
"zero(M) = fst(snd(snd(snd(snd(M)))))"


lemma add_field_eq [simp]: "add_field(<C,M,I,A,z>) = A"
by (simp add: add_field_def)

lemma add_eq [simp]: "ring_add(<C,M,I,A,z>, x, y) = A ` <x,y>"
by (simp add: ring_add_def)

lemma zero_eq [simp]: "zero(<C,M,I,A,Z,z>) = Z"
by (simp add: zero_def)


text {* Derived operations. *}

definition
a_inv :: "[i,i] => i" ("\<ominus>\<index> _" [81] 80) where
"a_inv(R) == m_inv (<carrier(R), add_field(R), zero(R), 0>)"

definition
minus :: "[i,i,i] => i" (infixl "\<ominus>\<index>" 65) where
"[|x ∈ carrier(R); y ∈ carrier(R)|] ==> x \<ominus>R y = x ⊕R (\<ominus>R y)"

locale abelian_monoid = fixes G (structure)
assumes a_comm_monoid:
"comm_monoid (<carrier(G), add_field(G), zero(G), 0>)"

text {*
The following definition is redundant but simple to use.
*}


locale abelian_group = abelian_monoid +
assumes a_comm_group:
"comm_group (<carrier(G), add_field(G), zero(G), 0>)"

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]: "\<one> ≠ \<zero>"
and integral: "[|a · b = \<zero>; a ∈ carrier(R); b ∈ carrier(R)|] ==>
a = \<zero> | b = \<zero>"



subsection {* Basic Properties *}

lemma (in abelian_monoid) a_monoid:
"monoid (<carrier(G), add_field(G), zero(G), 0>)"
apply (insert a_comm_monoid)
apply (simp add: comm_monoid_def)
done

lemma (in abelian_group) a_group:
"group (<carrier(G), add_field(G), zero(G), 0>)"
apply (insert a_comm_group)
apply (simp add: comm_group_def group_def)
done


lemma (in abelian_monoid) l_zero [simp]:
"x ∈ carrier(G) ==> \<zero> ⊕ 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]:
"\<zero> ∈ carrier(G)"
by (rule monoid.one_closed [OF a_monoid, simplified])

lemma (in abelian_group) a_inv_closed [intro, simp]:
"x ∈ carrier(G) ==> \<ominus> 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 \<ominus> 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) ==> \<ominus> x ⊕ x = \<zero>"
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 ⊕ \<zero> = 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 ⊕ (\<ominus> x) = \<zero>"
using group.r_inv [OF a_group]
by (simp add: a_inv_def ring_add_def [symmetric])

lemma (in abelian_group) minus_zero [simp]:
"\<ominus> \<zero> = \<zero>"
by (simp add: a_inv_def
group.inv_one [OF a_group, simplified ])

lemma (in abelian_group) minus_minus [simp]:
"x ∈ carrier(G) ==> \<ominus> (\<ominus> 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)|] ==> \<ominus> (x ⊕ y) = \<ominus> x ⊕ \<ominus> 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) ==> \<zero> · x = \<zero>"
proof -
assume R: "x ∈ carrier(R)"
then have "\<zero> · x ⊕ \<zero> · x = (\<zero> ⊕ \<zero>) · x"
by (blast intro: l_distr [THEN sym])
also from R have "... = \<zero> · x ⊕ \<zero>" by simp
finally have "\<zero> · x ⊕ \<zero> · x = \<zero> · x ⊕ \<zero>" .
with R show ?thesis by (simp del: r_zero)
qed

lemma r_null [simp]: "x ∈ carrier(R) ==> x · \<zero> = \<zero>"
proof -
assume R: "x ∈ carrier(R)"
then have "x · \<zero> ⊕ x · \<zero> = x · (\<zero> ⊕ \<zero>)"
by (simp add: r_distr del: l_zero r_zero)
also from R have "... = x · \<zero> ⊕ \<zero>" by simp
finally have "x · \<zero> ⊕ x · \<zero> = x · \<zero> ⊕ \<zero>" .
with R show ?thesis by (simp del: r_zero)
qed

lemma l_minus:
"[|x ∈ carrier(R); y ∈ carrier(R)|] ==> \<ominus> x · y = \<ominus> (x · y)"
proof -
assume R: "x ∈ carrier(R)" "y ∈ carrier(R)"
then have "(\<ominus> x) · y ⊕ x · y = (\<ominus> x ⊕ x) · y" by (simp add: l_distr)
also from R have "... = \<zero>" by (simp add: l_neg)
finally have "(\<ominus> x) · y ⊕ x · y = \<zero>" .
with R have "(\<ominus> x) · y ⊕ x · y ⊕ \<ominus> (x · y) = \<zero> ⊕ \<ominus> (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 · \<ominus> y = \<ominus> (x · y)"
proof -
assume R: "x ∈ carrier(R)" "y ∈ carrier(R)"
then have "x · (\<ominus> y) ⊕ x · y = x · (\<ominus> y ⊕ y)" by (simp add: r_distr)
also from R have "... = \<zero>" by (simp add: l_neg)
finally have "x · (\<ominus> y) ⊕ x · y = \<zero>" .
with R have "x · (\<ominus> y) ⊕ x · y ⊕ \<ominus> (x · y) = \<zero> ⊕ \<ominus> (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 \<ominus> y = x ⊕ \<ominus> 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 ` \<one>R = \<one>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 ` \<one>R = \<one>S"
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 ` \<one>R = \<one>S"
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 ` \<zero>R = \<zero>S"
proof -
have "h ` \<zero>RS h ` \<zero> = h ` \<zero>RS \<zero>S"
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 ` (\<ominus>R x) = \<ominus>S h ` x"
proof -
assume R: "x ∈ carrier(R)"
then have "h ` x ⊕S h ` (\<ominus> x) = h ` x ⊕S (\<ominus>S (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