# Theory RingHom

Up to index of Isabelle/HOL/Free-Groups

theory RingHom
imports Ideal
`(*  Title:      HOL/Algebra/RingHom.thy    Author:     Stephan Hohe, TU Muenchen*)theory RingHomimports Idealbeginsection {* Homomorphisms of Non-Commutative Rings *}text {* Lifting existing lemmas in a @{text 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 default (rule homh)sublocale ring_hom_ring ⊆ abelian_group: abelian_group_hom R Sapply (rule abelian_group_homI)  apply (rule R.is_abelian_group) apply (rule S.is_abelian_group)apply (intro group_hom.intro group_hom_axioms.intro)  apply (rule R.a_group) apply (rule S.a_group)apply (insert homh, unfold hom_def ring_hom_def)apply simpdonelemma (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 \<one> = \<one>⇘S⇙"  shows "ring_hom_ring R S h"proof -  interpret ring R by fact  interpret ring S by fact  show ?thesis apply unfold_localesapply (unfold ring_hom_def, safe)   apply (simp add: hom_closed Pi_def)  apply (erule (1) compatible_mult) apply (erule (1) compatible_add)apply (rule compatible_one)doneqedlemma 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)    doneqedlemma 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 \<one> = \<one>⇘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)    doneqedlemma 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)qedsubsection {* 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 (rule additive_subgroup.a_subgroup[OF additive_subgroup_a_kernel]) apply (unfold a_kernel_def', simp+)donetext {* Elements of the kernel are mapped to zero *}lemma (in abelian_group_hom) kernel_zero [simp]:  "i ∈ a_kernel R S h ==> h i = \<zero>⇘S⇙"by (simp add: a_kernel_defs)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 "… = \<zero>⇘S⇙ ⊕⇘S⇙ h a" by simp  also from carr      have "… = h a" by simp  finally      show "h x = h a" .qedlemma (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⇙ \<ominus>⇘S⇙h a = \<zero>⇘S⇙" by algebra  from carr      have "h x ⊕⇘S⇙ \<ominus>⇘S⇙h a = h (x ⊕ \<ominus>a)" by simp  from a and this      have b: "h (x ⊕ \<ominus>a) = \<zero>⇘S⇙" by simp  from carr have "x ⊕ \<ominus>a ∈ carrier R" by simp  from this and b      have "x ⊕ \<ominus>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)qedcorollary (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 1apply clarsimp defer 1proof  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 fastnext  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)qedend`