# Theory RingHom

theory RingHom
imports Ideal
```(*  Title:      HOL/Algebra/RingHom.thy
Author:     Stephan Hohe, TU Muenchen
*)

theory RingHom
imports Ideal
begin

section ‹Homomorphisms of Non-Commutative Rings›

text ‹Lifting existing lemmas in a ‹ring_hom_ring› locale›
locale ring_hom_ring = R?: ring R + S?: ring S
for R (structure) and S (structure) +
fixes h
assumes homh: "h ∈ ring_hom R S"
notes hom_mult [simp] = ring_hom_mult [OF homh]
and hom_one [simp] = ring_hom_one [OF homh]

sublocale ring_hom_cring ⊆ ring: ring_hom_ring
by standard (rule homh)

sublocale ring_hom_ring ⊆ abelian_group?: abelian_group_hom R S
apply (intro abelian_group_homI R.is_abelian_group S.is_abelian_group)
apply (intro group_hom.intro group_hom_axioms.intro R.a_group S.a_group)
apply (insert homh, unfold hom_def ring_hom_def)
apply simp
done

lemma (in ring_hom_ring) is_ring_hom_ring:
"ring_hom_ring R S h"
by (rule ring_hom_ring_axioms)

lemma ring_hom_ringI:
fixes R (structure) and S (structure)
assumes "ring R" "ring S"
assumes (* morphism: "h ∈ carrier R → carrier S" *)
hom_closed: "!!x. x ∈ carrier R ==> h x ∈ carrier S"
and compatible_mult: "⋀x y. [| x ∈ carrier R; y ∈ carrier R |] ==> h (x ⊗ y) = h x ⊗⇘S⇙ h y"
and compatible_add: "⋀x y. [| x ∈ carrier R; y ∈ carrier R |] ==> h (x ⊕ y) = h x ⊕⇘S⇙ h y"
and compatible_one: "h 𝟭 = 𝟭⇘S⇙"
shows "ring_hom_ring R S h"
proof -
interpret ring R by fact
interpret ring S by fact
show ?thesis apply unfold_locales
apply (unfold ring_hom_def, safe)
apply (erule (1) compatible_mult)
apply (rule compatible_one)
done
qed

lemma ring_hom_ringI2:
assumes "ring R" "ring S"
assumes h: "h ∈ ring_hom R S"
shows "ring_hom_ring R S h"
proof -
interpret R: ring R by fact
interpret S: ring S by fact
show ?thesis apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro)
apply (rule R.is_ring)
apply (rule S.is_ring)
apply (rule h)
done
qed

lemma ring_hom_ringI3:
fixes R (structure) and S (structure)
assumes "abelian_group_hom R S h" "ring R" "ring S"
assumes compatible_mult: "⋀x y. [| x ∈ carrier R; y ∈ carrier R |] ==> h (x ⊗ y) = h x ⊗⇘S⇙ h y"
and compatible_one: "h 𝟭 = 𝟭⇘S⇙"
shows "ring_hom_ring R S h"
proof -
interpret abelian_group_hom R S h by fact
interpret R: ring R by fact
interpret S: ring S by fact
show ?thesis apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro, rule R.is_ring, rule S.is_ring)
apply (insert group_hom.homh[OF a_group_hom])
apply (unfold hom_def ring_hom_def, simp)
apply safe
apply (erule (1) compatible_mult)
apply (rule compatible_one)
done
qed

lemma ring_hom_cringI:
assumes "ring_hom_ring R S h" "cring R" "cring S"
shows "ring_hom_cring R S h"
proof -
interpret ring_hom_ring R S h by fact
interpret R: cring R by fact
interpret S: cring S by fact
show ?thesis by (intro ring_hom_cring.intro ring_hom_cring_axioms.intro)
(rule R.is_cring, rule S.is_cring, rule homh)
qed

subsection ‹The Kernel of a Ring Homomorphism›

― ‹the kernel of a ring homomorphism is an ideal›
lemma (in ring_hom_ring) kernel_is_ideal:
shows "ideal (a_kernel R S h) R"
apply (rule idealI)
apply (rule R.is_ring)
apply (unfold a_kernel_def', simp+)
done

text ‹Elements of the kernel are mapped to zero›
lemma (in abelian_group_hom) kernel_zero [simp]:
"i ∈ a_kernel R S h ⟹ h i = 𝟬⇘S⇙"

subsection ‹Cosets›

text ‹Cosets of the kernel correspond to the elements of the image of the homomorphism›
lemma (in ring_hom_ring) rcos_imp_homeq:
assumes acarr: "a ∈ carrier R"
and xrcos: "x ∈ a_kernel R S h +> a"
shows "h x = h a"
proof -
interpret ideal "a_kernel R S h" "R" by (rule kernel_is_ideal)

from xrcos
have "∃i ∈ a_kernel R S h. x = i ⊕ a" by (simp add: a_r_coset_defs)
from this obtain i
where iker: "i ∈ a_kernel R S h"
and x: "x = i ⊕ a"
by fast+
note carr = acarr iker[THEN a_Hcarr]

from x
have "h x = h (i ⊕ a)" by simp
also from carr
have "… = h i ⊕⇘S⇙ h a" by simp
also from iker
have "… = 𝟬⇘S⇙ ⊕⇘S⇙ h a" by simp
also from carr
have "… = h a" by simp
finally
show "h x = h a" .
qed

lemma (in ring_hom_ring) homeq_imp_rcos:
assumes acarr: "a ∈ carrier R"
and xcarr: "x ∈ carrier R"
and hx: "h x = h a"
shows "x ∈ a_kernel R S h +> a"
proof -
interpret ideal "a_kernel R S h" "R" by (rule kernel_is_ideal)

note carr = acarr xcarr
note hcarr = acarr[THEN hom_closed] xcarr[THEN hom_closed]

from hx and hcarr
have a: "h x ⊕⇘S⇙ ⊖⇘S⇙h a = 𝟬⇘S⇙" by algebra
from carr
have "h x ⊕⇘S⇙ ⊖⇘S⇙h a = h (x ⊕ ⊖a)" by simp
from a and this
have b: "h (x ⊕ ⊖a) = 𝟬⇘S⇙" by simp

from carr have "x ⊕ ⊖a ∈ carrier R" by simp
from this and b
have "x ⊕ ⊖a ∈ a_kernel R S h"
unfolding a_kernel_def'
by fast

from this and carr
show "x ∈ a_kernel R S h +> a" by (simp add: a_rcos_module_rev)
qed

corollary (in ring_hom_ring) rcos_eq_homeq:
assumes acarr: "a ∈ carrier R"
shows "(a_kernel R S h) +> a = {x ∈ carrier R. h x = h a}"
apply rule defer 1
apply clarsimp defer 1
proof
interpret ideal "a_kernel R S h" "R" by (rule kernel_is_ideal)

fix x
assume xrcos: "x ∈ a_kernel R S h +> a"
from acarr and this
have xcarr: "x ∈ carrier R"
by (rule a_elemrcos_carrier)

from xrcos
have "h x = h a" by (rule rcos_imp_homeq[OF acarr])
from xcarr and this
show "x ∈ {x ∈ carrier R. h x = h a}" by fast
next
interpret ideal "a_kernel R S h" "R" by (rule kernel_is_ideal)

fix x
assume xcarr: "x ∈ carrier R"
and hx: "h x = h a"
from acarr xcarr hx
show "x ∈ a_kernel R S h +> a" by (rule homeq_imp_rcos)
qed

lemma (in ring_hom_ring) nat_pow_hom:
"x ∈ carrier R ⟹ h (x [^] (n :: nat)) = (h x) [^]⇘S⇙ n"
by (induct n) (auto)

(*contributed by Paulo EmÃ­lio de Vilhena*)
lemma (in ring_hom_ring) inj_on_domain:
assumes "inj_on h (carrier R)"
shows "domain S ⟹ domain R"
proof -
assume A: "domain S" show "domain R"
proof
have "h 𝟭 = 𝟭⇘S⇙ ∧ h 𝟬 = 𝟬⇘S⇙" by simp
hence "h 𝟭 ≠ h 𝟬"
using domain.one_not_zero[OF A] by simp
thus "𝟭 ≠ 𝟬"
using assms unfolding inj_on_def by fastforce
next
fix a b
assume a: "a ∈ carrier R"
and b: "b ∈ carrier R"
have "h (a ⊗ b) = (h a) ⊗⇘S⇙ (h b)" by (simp add: a b)
also have " ... = (h b) ⊗⇘S⇙ (h a)" using a b A cringE(1)[of S]
also have " ... = h (b ⊗ a)" by (simp add: a b)
finally have "h (a ⊗ b) = h (b ⊗ a)" .
thus "a ⊗ b = b ⊗ a"
using assms a b unfolding inj_on_def by simp

assume  ab: "a ⊗ b = 𝟬"
hence "h (a ⊗ b) = 𝟬⇘S⇙" by simp
hence "(h a) ⊗⇘S⇙ (h b) = 𝟬⇘S⇙" using a b by simp
hence "h a =  𝟬⇘S⇙ ∨ h b =  𝟬⇘S⇙" using a b domain.integral[OF A] by simp
thus "a = 𝟬 ∨ b = 𝟬"
using a b assms unfolding inj_on_def by force
qed
qed

end
```