36 constdefs (structure G) |
36 constdefs (structure G) |
37 a_r_congruent :: "[('a,'b)ring_scheme, 'a set] \<Rightarrow> ('a*'a)set" |
37 a_r_congruent :: "[('a,'b)ring_scheme, 'a set] \<Rightarrow> ('a*'a)set" |
38 ("racong\<index> _") |
38 ("racong\<index> _") |
39 "a_r_congruent G \<equiv> r_congruent \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>" |
39 "a_r_congruent G \<equiv> r_congruent \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>" |
40 |
40 |
41 constdefs |
41 definition A_FactGroup :: "[('a,'b) ring_scheme, 'a set] \<Rightarrow> ('a set) monoid" (infixl "A'_Mod" 65) where |
42 A_FactGroup :: "[('a,'b) ring_scheme, 'a set] \<Rightarrow> ('a set) monoid" |
|
43 (infixl "A'_Mod" 65) |
|
44 --{*Actually defined for groups rather than monoids*} |
42 --{*Actually defined for groups rather than monoids*} |
45 "A_FactGroup G H \<equiv> FactGroup \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H" |
43 "A_FactGroup G H \<equiv> FactGroup \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H" |
46 |
44 |
47 constdefs |
45 definition a_kernel :: "('a, 'm) ring_scheme \<Rightarrow> ('b, 'n) ring_scheme \<Rightarrow> |
48 a_kernel :: "('a, 'm) ring_scheme \<Rightarrow> ('b, 'n) ring_scheme \<Rightarrow> |
46 ('a \<Rightarrow> 'b) \<Rightarrow> 'a set" where |
49 ('a \<Rightarrow> 'b) \<Rightarrow> 'a set" |
|
50 --{*the kernel of a homomorphism (additive)*} |
47 --{*the kernel of a homomorphism (additive)*} |
51 "a_kernel G H h \<equiv> kernel \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> |
48 "a_kernel G H h \<equiv> kernel \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> |
52 \<lparr>carrier = carrier H, mult = add H, one = zero H\<rparr> h" |
49 \<lparr>carrier = carrier H, mult = add H, one = zero H\<rparr> h" |
53 |
50 |
54 locale abelian_group_hom = G: abelian_group G + H: abelian_group H |
51 locale abelian_group_hom = G: abelian_group G + H: abelian_group H |