equal
deleted
inserted
replaced
5 *) |
5 *) |
6 |
6 |
7 theory RingHom |
7 theory RingHom |
8 imports Ideal |
8 imports Ideal |
9 begin |
9 begin |
10 |
|
11 |
10 |
12 section {* Homomorphisms of Non-Commutative Rings *} |
11 section {* Homomorphisms of Non-Commutative Rings *} |
13 |
12 |
14 text {* Lifting existing lemmas in a @{text ring_hom_ring} locale *} |
13 text {* Lifting existing lemmas in a @{text ring_hom_ring} locale *} |
15 locale ring_hom_ring = ring R + ring S + var h + |
14 locale ring_hom_ring = ring R + ring S + var h + |
65 lemma ring_hom_ringI3: |
64 lemma ring_hom_ringI3: |
66 includes abelian_group_hom R S + ring R + ring S |
65 includes abelian_group_hom R S + ring R + ring S |
67 assumes compatible_mult: "!!x y. [| x : carrier R; y : carrier R |] ==> h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y" |
66 assumes compatible_mult: "!!x y. [| x : carrier R; y : carrier R |] ==> h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y" |
68 and compatible_one: "h \<one> = \<one>\<^bsub>S\<^esub>" |
67 and compatible_one: "h \<one> = \<one>\<^bsub>S\<^esub>" |
69 shows "ring_hom_ring R S h" |
68 shows "ring_hom_ring R S h" |
70 apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro, assumption+) |
69 apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro, rule R.is_ring, rule S.is_ring) |
71 apply (insert group_hom.homh[OF a_group_hom]) |
70 apply (insert group_hom.homh[OF a_group_hom]) |
72 apply (unfold hom_def ring_hom_def, simp) |
71 apply (unfold hom_def ring_hom_def, simp) |
73 apply safe |
72 apply safe |
74 apply (erule (1) compatible_mult) |
73 apply (erule (1) compatible_mult) |
75 apply (rule compatible_one) |
74 apply (rule compatible_one) |