Quelle  RingHom.thy   Sprache: Isabelle

(*  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
proof 
  show "h \ hom (add_monoid R) (add_monoid S)"
    using homh by (simp add: hom_def ring_hom_def)
qed

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 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 \\<^bsub>S\<^esub> h y"
      and compatible_add: "\x y. [| x \ carrier R; y \ carrier R |] ==> h (x \ y) = h x \\<^bsub>S\<^esub> h y"
      and compatible_one: "h \ = \\<^bsub>S\<^esub>"
  shows "ring_hom_ring R S h"
proof -
  interpret ring R by fact
  interpret ring S by fact
  show ?thesis
  proof
    show "h \ ring_hom R S"
      unfolding ring_hom_def
      by (auto simp: compatible_mult compatible_add compatible_one hom_closed)
  qed
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 
  proof
    show "h \ ring_hom R S"
      using h .
  qed
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 \\<^bsub>S\<^esub> h y"
      and compatible_one: "h \ = \\<^bsub>S\<^esub>"
  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
  proof
    show "h \ ring_hom R S"
      unfolding ring_hom_def by (auto simp: compatible_one compatible_mult)
  qed
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 
  proof
    show "h \ ring_hom R S"
      by (simp add: homh)
  qed
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: "ideal (a_kernel R S h) R"
  apply (rule idealI [OF R.ring_axioms])
    apply (rule additive_subgroup.a_subgroup[OF additive_subgroup_a_kernel])
   apply (auto simp: a_kernel_def')
  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 = \\<^bsub>S\<^esub>"
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 \\<^bsub>S\<^esub> h a" by simp
  also from iker
      have "\ = \\<^bsub>S\<^esub> \\<^bsub>S\<^esub> 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 \\<^bsub>S\<^esub> \\<^bsub>S\<^esub>h a = \\<^bsub>S\<^esub>" by algebra
  from carr
      have "h x \\<^bsub>S\<^esub> \\<^bsub>S\<^esub>h a = h (x \ \a)" by simp
  from a and this
      have b: "h (x \ \a) = \\<^bsub>S\<^esub>" 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}"
proof -
  interpret ideal "a_kernel R S h" "R" by (rule kernel_is_ideal)
  show ?thesis
    using assms by (auto simp: intro: homeq_imp_rcos rcos_imp_homeq a_elemrcos_carrier)
qed

lemma (in ring_hom_ring) hom_nat_pow:
  "x \ carrier R \ h (x [^] (n :: nat)) = (h x) [^]\<^bsub>S\<^esub> n"
  by (induct n) (auto)


lemma (in ring_hom_ring) inj_on_domain: 🍋‹contributor ‹Paulo Emílio de Vilhena››
  assumes "inj_on h (carrier R)"
  shows "domain S \ domain R"
proof -
  assume A: "domain S" show "domain R"
  proof
    have "h \ = \\<^bsub>S\<^esub> \ h \ = \\<^bsub>S\<^esub>" 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) \\<^bsub>S\<^esub> (h b)" by (simp add: a b)
    also have " ... = (h b) \\<^bsub>S\<^esub> (h a)" using a b A cringE(1)[of S]
      by (simp add: cring.cring_simprules(14) domain_def)
    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) = \\<^bsub>S\<^esub>" by simp
    hence "(h a) \\<^bsub>S\<^esub> (h b) = \\<^bsub>S\<^esub>" using a b by simp
    hence "h a = \\<^bsub>S\<^esub> \ h b = \\<^bsub>S\<^esub>" 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