author | wenzelm |
Fri, 08 Feb 2019 14:42:28 +0100 | |
changeset 69794 | a19fdf64726c |
parent 69597 | ff784d5a5bfb |
child 80914 | d97fdabd9e2b |
permissions | -rw-r--r-- |
35849 | 1 |
(* Title: HOL/Algebra/AbelCoset.thy |
2 |
Author: Stephan Hohe, TU Muenchen |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
3 |
*) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
4 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
5 |
theory AbelCoset |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
6 |
imports Coset Ring |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
7 |
begin |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
8 |
|
61382 | 9 |
subsection \<open>More Lifting from Groups to Abelian Groups\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
10 |
|
61382 | 11 |
subsubsection \<open>Definitions\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
12 |
|
69597 | 13 |
text \<open>Hiding \<open><+>\<close> from \<^theory>\<open>HOL.Sum_Type\<close> until I come |
61382 | 14 |
up with better syntax here\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
15 |
|
40271 | 16 |
no_notation Sum_Type.Plus (infixr "<+>" 65) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
17 |
|
35847 | 18 |
definition |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
19 |
a_r_coset :: "[_, 'a set, 'a] \<Rightarrow> 'a set" (infixl "+>\<index>" 60) |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
20 |
where "a_r_coset G = r_coset (add_monoid G)" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
21 |
|
35847 | 22 |
definition |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
23 |
a_l_coset :: "[_, 'a, 'a set] \<Rightarrow> 'a set" (infixl "<+\<index>" 60) |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
24 |
where "a_l_coset G = l_coset (add_monoid G)" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
25 |
|
35847 | 26 |
definition |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
27 |
A_RCOSETS :: "[_, 'a set] \<Rightarrow> ('a set)set" ("a'_rcosets\<index> _" [81] 80) |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
28 |
where "A_RCOSETS G H = RCOSETS (add_monoid G) H" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
29 |
|
35847 | 30 |
definition |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
31 |
set_add :: "[_, 'a set ,'a set] \<Rightarrow> 'a set" (infixl "<+>\<index>" 60) |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
32 |
where "set_add G = set_mult (add_monoid G)" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
33 |
|
35847 | 34 |
definition |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
35 |
A_SET_INV :: "[_,'a set] \<Rightarrow> 'a set" ("a'_set'_inv\<index> _" [81] 80) |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
36 |
where "A_SET_INV G H = SET_INV (add_monoid G) H" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
37 |
|
35847 | 38 |
definition |
45006 | 39 |
a_r_congruent :: "[('a,'b)ring_scheme, 'a set] \<Rightarrow> ('a*'a)set" ("racong\<index>") |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
40 |
where "a_r_congruent G = r_congruent (add_monoid G)" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
41 |
|
35848
5443079512ea
slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents:
35847
diff
changeset
|
42 |
definition |
5443079512ea
slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents:
35847
diff
changeset
|
43 |
A_FactGroup :: "[('a,'b) ring_scheme, 'a set] \<Rightarrow> ('a set) monoid" (infixl "A'_Mod" 65) |
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
67091
diff
changeset
|
44 |
\<comment> \<open>Actually defined for groups rather than monoids\<close> |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
45 |
where "A_FactGroup G H = FactGroup (add_monoid G) H" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
46 |
|
35848
5443079512ea
slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents:
35847
diff
changeset
|
47 |
definition |
5443079512ea
slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents:
35847
diff
changeset
|
48 |
a_kernel :: "('a, 'm) ring_scheme \<Rightarrow> ('b, 'n) ring_scheme \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a set" |
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
67091
diff
changeset
|
49 |
\<comment> \<open>the kernel of a homomorphism (additive)\<close> |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
50 |
where "a_kernel G H h = kernel (add_monoid G) (add_monoid H) h" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
51 |
|
61565
352c73a689da
Qualifiers in locale expressions default to mandatory regardless of the command.
ballarin
parents:
61382
diff
changeset
|
52 |
locale abelian_group_hom = G?: abelian_group G + H?: abelian_group H |
29237 | 53 |
for G (structure) and H (structure) + |
54 |
fixes h |
|
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
55 |
assumes a_group_hom: "group_hom (add_monoid G) (add_monoid H) h" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
56 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
57 |
lemmas a_r_coset_defs = |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
58 |
a_r_coset_def r_coset_def |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
59 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
60 |
lemma a_r_coset_def': |
27611 | 61 |
fixes G (structure) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
62 |
shows "H +> a \<equiv> \<Union>h\<in>H. {h \<oplus> a}" |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
63 |
unfolding a_r_coset_defs by simp |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
64 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
65 |
lemmas a_l_coset_defs = |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
66 |
a_l_coset_def l_coset_def |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
67 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
68 |
lemma a_l_coset_def': |
27611 | 69 |
fixes G (structure) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
70 |
shows "a <+ H \<equiv> \<Union>h\<in>H. {a \<oplus> h}" |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
71 |
unfolding a_l_coset_defs by simp |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
72 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
73 |
lemmas A_RCOSETS_defs = |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
74 |
A_RCOSETS_def RCOSETS_def |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
75 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
76 |
lemma A_RCOSETS_def': |
27611 | 77 |
fixes G (structure) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
78 |
shows "a_rcosets H \<equiv> \<Union>a\<in>carrier G. {H +> a}" |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
79 |
unfolding A_RCOSETS_defs by (fold a_r_coset_def, simp) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
80 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
81 |
lemmas set_add_defs = |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
82 |
set_add_def set_mult_def |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
83 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
84 |
lemma set_add_def': |
27611 | 85 |
fixes G (structure) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
86 |
shows "H <+> K \<equiv> \<Union>h\<in>H. \<Union>k\<in>K. {h \<oplus> k}" |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
87 |
unfolding set_add_defs by simp |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
88 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
89 |
lemmas A_SET_INV_defs = |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
90 |
A_SET_INV_def SET_INV_def |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
91 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
92 |
lemma A_SET_INV_def': |
27611 | 93 |
fixes G (structure) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
94 |
shows "a_set_inv H \<equiv> \<Union>h\<in>H. {\<ominus> h}" |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
95 |
unfolding A_SET_INV_defs by (fold a_inv_def) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
96 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
97 |
|
61382 | 98 |
subsubsection \<open>Cosets\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
99 |
|
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
100 |
sublocale abelian_group < |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
101 |
add: group "(add_monoid G)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
102 |
rewrites "carrier (add_monoid G) = carrier G" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
103 |
and " mult (add_monoid G) = add G" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
104 |
and " one (add_monoid G) = zero G" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
105 |
and " m_inv (add_monoid G) = a_inv G" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
106 |
and "finprod (add_monoid G) = finsum G" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
107 |
and "r_coset (add_monoid G) = a_r_coset G" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
108 |
and "l_coset (add_monoid G) = a_l_coset G" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
109 |
and "(\<lambda>a k. pow (add_monoid G) a k) = (\<lambda>a k. add_pow G k a)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
110 |
by (rule a_group) |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
111 |
(auto simp: m_inv_def a_inv_def finsum_def a_r_coset_def a_l_coset_def add_pow_def) |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
112 |
|
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
113 |
context abelian_group |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
114 |
begin |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
115 |
|
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
116 |
thm add.coset_mult_assoc |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
117 |
lemmas a_repr_independence' = add.repr_independence |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
118 |
|
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
119 |
(* |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
120 |
lemmas a_coset_add_assoc = add.coset_mult_assoc |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
121 |
lemmas a_coset_add_zero [simp] = add.coset_mult_one |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
122 |
lemmas a_coset_add_inv1 = add.coset_mult_inv1 |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
123 |
lemmas a_coset_add_inv2 = add.coset_mult_inv2 |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
124 |
lemmas a_coset_join1 = add.coset_join1 |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
125 |
lemmas a_coset_join2 = add.coset_join2 |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
126 |
lemmas a_solve_equation = add.solve_equation |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
127 |
lemmas a_repr_independence = add.repr_independence |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
128 |
lemmas a_rcosI = add.rcosI |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
129 |
lemmas a_rcosetsI = add.rcosetsI |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
130 |
*) |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
131 |
|
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
132 |
end |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
133 |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
134 |
lemma (in abelian_group) a_coset_add_assoc: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
135 |
"[| M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G |] |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
136 |
==> (M +> g) +> h = M +> (g \<oplus> h)" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
137 |
by (rule group.coset_mult_assoc [OF a_group, |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
138 |
folded a_r_coset_def, simplified monoid_record_simps]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
139 |
|
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
140 |
thm abelian_group.a_coset_add_assoc |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
141 |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
142 |
lemma (in abelian_group) a_coset_add_zero [simp]: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
143 |
"M \<subseteq> carrier G ==> M +> \<zero> = M" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
144 |
by (rule group.coset_mult_one [OF a_group, |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
145 |
folded a_r_coset_def, simplified monoid_record_simps]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
146 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
147 |
lemma (in abelian_group) a_coset_add_inv1: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
148 |
"[| M +> (x \<oplus> (\<ominus> y)) = M; x \<in> carrier G ; y \<in> carrier G; |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
149 |
M \<subseteq> carrier G |] ==> M +> x = M +> y" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
150 |
by (rule group.coset_mult_inv1 [OF a_group, |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
151 |
folded a_r_coset_def a_inv_def, simplified monoid_record_simps]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
152 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
153 |
lemma (in abelian_group) a_coset_add_inv2: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
154 |
"[| M +> x = M +> y; x \<in> carrier G; y \<in> carrier G; M \<subseteq> carrier G |] |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
155 |
==> M +> (x \<oplus> (\<ominus> y)) = M" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
156 |
by (rule group.coset_mult_inv2 [OF a_group, |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
157 |
folded a_r_coset_def a_inv_def, simplified monoid_record_simps]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
158 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
159 |
lemma (in abelian_group) a_coset_join1: |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
160 |
"[| H +> x = H; x \<in> carrier G; subgroup H (add_monoid G) |] ==> x \<in> H" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
161 |
by (rule group.coset_join1 [OF a_group, |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
162 |
folded a_r_coset_def, simplified monoid_record_simps]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
163 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
164 |
lemma (in abelian_group) a_solve_equation: |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
165 |
"\<lbrakk>subgroup H (add_monoid G); x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> \<exists>h\<in>H. y = h \<oplus> x" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
166 |
by (rule group.solve_equation [OF a_group, |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
167 |
folded a_r_coset_def, simplified monoid_record_simps]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
168 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
169 |
lemma (in abelian_group) a_repr_independence: |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
170 |
"\<lbrakk> y \<in> H +> x; x \<in> carrier G; subgroup H (add_monoid G) \<rbrakk> \<Longrightarrow> |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
171 |
H +> x = H +> y" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
172 |
using a_repr_independence' by (simp add: a_r_coset_def) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
173 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
174 |
lemma (in abelian_group) a_coset_join2: |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
175 |
"\<lbrakk>x \<in> carrier G; subgroup H (add_monoid G); x\<in>H\<rbrakk> \<Longrightarrow> H +> x = H" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
176 |
by (rule group.coset_join2 [OF a_group, |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
177 |
folded a_r_coset_def, simplified monoid_record_simps]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
178 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
179 |
lemma (in abelian_monoid) a_r_coset_subset_G: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
180 |
"[| H \<subseteq> carrier G; x \<in> carrier G |] ==> H +> x \<subseteq> carrier G" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
181 |
by (rule monoid.r_coset_subset_G [OF a_monoid, |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
182 |
folded a_r_coset_def, simplified monoid_record_simps]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
183 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
184 |
lemma (in abelian_group) a_rcosI: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
185 |
"[| h \<in> H; H \<subseteq> carrier G; x \<in> carrier G|] ==> h \<oplus> x \<in> H +> x" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
186 |
by (rule group.rcosI [OF a_group, |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
187 |
folded a_r_coset_def, simplified monoid_record_simps]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
188 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
189 |
lemma (in abelian_group) a_rcosetsI: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
190 |
"\<lbrakk>H \<subseteq> carrier G; x \<in> carrier G\<rbrakk> \<Longrightarrow> H +> x \<in> a_rcosets H" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
191 |
by (rule group.rcosetsI [OF a_group, |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
192 |
folded a_r_coset_def A_RCOSETS_def, simplified monoid_record_simps]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
193 |
|
61382 | 194 |
text\<open>Really needed?\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
195 |
lemma (in abelian_group) a_transpose_inv: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
196 |
"[| x \<oplus> y = z; x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
197 |
==> (\<ominus> x) \<oplus> z = y" |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
198 |
using r_neg1 by blast |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
199 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
200 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
201 |
|
61382 | 202 |
subsubsection \<open>Subgroups\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
203 |
|
29237 | 204 |
locale additive_subgroup = |
205 |
fixes H and G (structure) |
|
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
206 |
assumes a_subgroup: "subgroup H (add_monoid G)" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
207 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
208 |
lemma (in additive_subgroup) is_additive_subgroup: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
209 |
shows "additive_subgroup H G" |
26203 | 210 |
by (rule additive_subgroup_axioms) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
211 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
212 |
lemma additive_subgroupI: |
27611 | 213 |
fixes G (structure) |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
214 |
assumes a_subgroup: "subgroup H (add_monoid G)" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
215 |
shows "additive_subgroup H G" |
23350 | 216 |
by (rule additive_subgroup.intro) (rule a_subgroup) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
217 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
218 |
lemma (in additive_subgroup) a_subset: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
219 |
"H \<subseteq> carrier G" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
220 |
by (rule subgroup.subset[OF a_subgroup, |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
221 |
simplified monoid_record_simps]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
222 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
223 |
lemma (in additive_subgroup) a_closed [intro, simp]: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
224 |
"\<lbrakk>x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> x \<oplus> y \<in> H" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
225 |
by (rule subgroup.m_closed[OF a_subgroup, |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
226 |
simplified monoid_record_simps]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
227 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
228 |
lemma (in additive_subgroup) zero_closed [simp]: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
229 |
"\<zero> \<in> H" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
230 |
by (rule subgroup.one_closed[OF a_subgroup, |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
231 |
simplified monoid_record_simps]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
232 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
233 |
lemma (in additive_subgroup) a_inv_closed [intro,simp]: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
234 |
"x \<in> H \<Longrightarrow> \<ominus> x \<in> H" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
235 |
by (rule subgroup.m_inv_closed[OF a_subgroup, |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
236 |
folded a_inv_def, simplified monoid_record_simps]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
237 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
238 |
|
61382 | 239 |
subsubsection \<open>Additive subgroups are normal\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
240 |
|
63167 | 241 |
text \<open>Every subgroup of an \<open>abelian_group\<close> is normal\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
242 |
|
29237 | 243 |
locale abelian_subgroup = additive_subgroup + abelian_group G + |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
244 |
assumes a_normal: "normal H (add_monoid G)" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
245 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
246 |
lemma (in abelian_subgroup) is_abelian_subgroup: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
247 |
shows "abelian_subgroup H G" |
26203 | 248 |
by (rule abelian_subgroup_axioms) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
249 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
250 |
lemma abelian_subgroupI: |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
251 |
assumes a_normal: "normal H (add_monoid G)" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
252 |
and a_comm: "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<oplus>\<^bsub>G\<^esub> y = y \<oplus>\<^bsub>G\<^esub> x" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
253 |
shows "abelian_subgroup H G" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
254 |
proof - |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
255 |
interpret normal "H" "(add_monoid G)" |
44655 | 256 |
by (rule a_normal) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
257 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
258 |
show "abelian_subgroup H G" |
61169 | 259 |
by standard (simp add: a_comm) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
260 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
261 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
262 |
lemma abelian_subgroupI2: |
27611 | 263 |
fixes G (structure) |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
264 |
assumes a_comm_group: "comm_group (add_monoid G)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
265 |
and a_subgroup: "subgroup H (add_monoid G)" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
266 |
shows "abelian_subgroup H G" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
267 |
proof - |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
268 |
interpret comm_group "(add_monoid G)" |
45388 | 269 |
by (rule a_comm_group) |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
270 |
interpret subgroup "H" "(add_monoid G)" |
45388 | 271 |
by (rule a_subgroup) |
68684 | 272 |
have "(\<Union>xa\<in>H. {xa \<oplus> x}) = (\<Union>xa\<in>H. {x \<oplus> xa})" if "x \<in> carrier G" for x |
273 |
proof - |
|
274 |
have "H \<subseteq> carrier G" |
|
275 |
using a_subgroup that unfolding subgroup_def by simp |
|
276 |
with that show "(\<Union>h\<in>H. {h \<oplus>\<^bsub>G\<^esub> x}) = (\<Union>h\<in>H. {x \<oplus>\<^bsub>G\<^esub> h})" |
|
62343
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
61565
diff
changeset
|
277 |
using m_comm [simplified] by fastforce |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
278 |
qed |
68684 | 279 |
then show "abelian_subgroup H G" |
280 |
by unfold_locales (auto simp: r_coset_def l_coset_def) |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
281 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
282 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
283 |
lemma abelian_subgroupI3: |
27611 | 284 |
fixes G (structure) |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
285 |
assumes "additive_subgroup H G" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
286 |
and "abelian_group G" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
287 |
shows "abelian_subgroup H G" |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
288 |
using assms abelian_subgroupI2 abelian_group.a_comm_group additive_subgroup_def by blast |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
289 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
290 |
lemma (in abelian_subgroup) a_coset_eq: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
291 |
"(\<forall>x \<in> carrier G. H +> x = x <+ H)" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
292 |
by (rule normal.coset_eq[OF a_normal, |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
293 |
folded a_r_coset_def a_l_coset_def, simplified monoid_record_simps]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
294 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
295 |
lemma (in abelian_subgroup) a_inv_op_closed1: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
296 |
shows "\<lbrakk>x \<in> carrier G; h \<in> H\<rbrakk> \<Longrightarrow> (\<ominus> x) \<oplus> h \<oplus> x \<in> H" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
297 |
by (rule normal.inv_op_closed1 [OF a_normal, |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
298 |
folded a_inv_def, simplified monoid_record_simps]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
299 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
300 |
lemma (in abelian_subgroup) a_inv_op_closed2: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
301 |
shows "\<lbrakk>x \<in> carrier G; h \<in> H\<rbrakk> \<Longrightarrow> x \<oplus> h \<oplus> (\<ominus> x) \<in> H" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
302 |
by (rule normal.inv_op_closed2 [OF a_normal, |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
303 |
folded a_inv_def, simplified monoid_record_simps]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
304 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
305 |
lemma (in abelian_group) a_lcos_m_assoc: |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
306 |
"\<lbrakk> M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G \<rbrakk> \<Longrightarrow> g <+ (h <+ M) = (g \<oplus> h) <+ M" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
307 |
by (rule group.lcos_m_assoc [OF a_group, |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
308 |
folded a_l_coset_def, simplified monoid_record_simps]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
309 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
310 |
lemma (in abelian_group) a_lcos_mult_one: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
311 |
"M \<subseteq> carrier G ==> \<zero> <+ M = M" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
312 |
by (rule group.lcos_mult_one [OF a_group, |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
313 |
folded a_l_coset_def, simplified monoid_record_simps]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
314 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
315 |
lemma (in abelian_group) a_l_coset_subset_G: |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
316 |
"\<lbrakk> H \<subseteq> carrier G; x \<in> carrier G \<rbrakk> \<Longrightarrow> x <+ H \<subseteq> carrier G" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
317 |
by (rule group.l_coset_subset_G [OF a_group, |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
318 |
folded a_l_coset_def, simplified monoid_record_simps]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
319 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
320 |
lemma (in abelian_group) a_l_coset_swap: |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
321 |
"\<lbrakk>y \<in> x <+ H; x \<in> carrier G; subgroup H (add_monoid G)\<rbrakk> \<Longrightarrow> x \<in> y <+ H" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
322 |
by (rule group.l_coset_swap [OF a_group, |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
323 |
folded a_l_coset_def, simplified monoid_record_simps]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
324 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
325 |
lemma (in abelian_group) a_l_coset_carrier: |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
326 |
"[| y \<in> x <+ H; x \<in> carrier G; subgroup H (add_monoid G) |] ==> y \<in> carrier G" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
327 |
by (rule group.l_coset_carrier [OF a_group, |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
328 |
folded a_l_coset_def, simplified monoid_record_simps]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
329 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
330 |
lemma (in abelian_group) a_l_repr_imp_subset: |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
331 |
assumes "y \<in> x <+ H" "x \<in> carrier G" "subgroup H (add_monoid G)" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
332 |
shows "y <+ H \<subseteq> x <+ H" |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
333 |
by (metis (full_types) a_l_coset_defs(1) add.l_repr_independence assms set_eq_subset) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
334 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
335 |
lemma (in abelian_group) a_l_repr_independence: |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
336 |
assumes y: "y \<in> x <+ H" and x: "x \<in> carrier G" and sb: "subgroup H (add_monoid G)" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
337 |
shows "x <+ H = y <+ H" |
23350 | 338 |
apply (rule group.l_repr_independence [OF a_group, |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
339 |
folded a_l_coset_def, simplified monoid_record_simps]) |
23350 | 340 |
apply (rule y) |
341 |
apply (rule x) |
|
342 |
apply (rule sb) |
|
343 |
done |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
344 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
345 |
lemma (in abelian_group) setadd_subset_G: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
346 |
"\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G\<rbrakk> \<Longrightarrow> H <+> K \<subseteq> carrier G" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
347 |
by (rule group.setmult_subset_G [OF a_group, |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
348 |
folded set_add_def, simplified monoid_record_simps]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
349 |
|
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
350 |
lemma (in abelian_group) subgroup_add_id: "subgroup H (add_monoid G) \<Longrightarrow> H <+> H = H" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
351 |
by (rule group.subgroup_mult_id [OF a_group, |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
352 |
folded set_add_def, simplified monoid_record_simps]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
353 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
354 |
lemma (in abelian_subgroup) a_rcos_inv: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
355 |
assumes x: "x \<in> carrier G" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
356 |
shows "a_set_inv (H +> x) = H +> (\<ominus> x)" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
357 |
by (rule normal.rcos_inv [OF a_normal, |
23350 | 358 |
folded a_r_coset_def a_inv_def A_SET_INV_def, simplified monoid_record_simps]) (rule x) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
359 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
360 |
lemma (in abelian_group) a_setmult_rcos_assoc: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
361 |
"\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G\<rbrakk> |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
362 |
\<Longrightarrow> H <+> (K +> x) = (H <+> K) +> x" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
363 |
by (rule group.setmult_rcos_assoc [OF a_group, |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
364 |
folded set_add_def a_r_coset_def, simplified monoid_record_simps]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
365 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
366 |
lemma (in abelian_group) a_rcos_assoc_lcos: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
367 |
"\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G\<rbrakk> |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
368 |
\<Longrightarrow> (H +> x) <+> K = H <+> (x <+ K)" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
369 |
by (rule group.rcos_assoc_lcos [OF a_group, |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
370 |
folded set_add_def a_r_coset_def a_l_coset_def, simplified monoid_record_simps]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
371 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
372 |
lemma (in abelian_subgroup) a_rcos_sum: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
373 |
"\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk> |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
374 |
\<Longrightarrow> (H +> x) <+> (H +> y) = H +> (x \<oplus> y)" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
375 |
by (rule normal.rcos_sum [OF a_normal, |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
376 |
folded set_add_def a_r_coset_def, simplified monoid_record_simps]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
377 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
378 |
lemma (in abelian_subgroup) rcosets_add_eq: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
379 |
"M \<in> a_rcosets H \<Longrightarrow> H <+> M = M" |
63167 | 380 |
\<comment> \<open>generalizes \<open>subgroup_mult_id\<close>\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
381 |
by (rule normal.rcosets_mult_eq [OF a_normal, |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
382 |
folded set_add_def A_RCOSETS_def, simplified monoid_record_simps]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
383 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
384 |
|
61382 | 385 |
subsubsection \<open>Congruence Relation\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
386 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
387 |
lemma (in abelian_subgroup) a_equiv_rcong: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
388 |
shows "equiv (carrier G) (racong H)" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
389 |
by (rule subgroup.equiv_rcong [OF a_subgroup a_group, |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
390 |
folded a_r_congruent_def, simplified monoid_record_simps]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
391 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
392 |
lemma (in abelian_subgroup) a_l_coset_eq_rcong: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
393 |
assumes a: "a \<in> carrier G" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
394 |
shows "a <+ H = racong H `` {a}" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
395 |
by (rule subgroup.l_coset_eq_rcong [OF a_subgroup a_group, |
23350 | 396 |
folded a_r_congruent_def a_l_coset_def, simplified monoid_record_simps]) (rule a) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
397 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
398 |
lemma (in abelian_subgroup) a_rcos_equation: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
399 |
shows |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
400 |
"\<lbrakk>ha \<oplus> a = h \<oplus> b; a \<in> carrier G; b \<in> carrier G; |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
401 |
h \<in> H; ha \<in> H; hb \<in> H\<rbrakk> |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
402 |
\<Longrightarrow> hb \<oplus> a \<in> (\<Union>h\<in>H. {h \<oplus> b})" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
403 |
by (rule group.rcos_equation [OF a_group a_subgroup, |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
404 |
folded a_r_congruent_def a_l_coset_def, simplified monoid_record_simps]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
405 |
|
68975
5ce4d117cea7
A few new results, elimination of duplicates and more use of "pairwise"
paulson <lp15@cam.ac.uk>
parents:
68684
diff
changeset
|
406 |
lemma (in abelian_subgroup) a_rcos_disjoint: "pairwise disjnt (a_rcosets H)" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
407 |
by (rule group.rcos_disjoint [OF a_group a_subgroup, |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
408 |
folded A_RCOSETS_def, simplified monoid_record_simps]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
409 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
410 |
lemma (in abelian_subgroup) a_rcos_self: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
411 |
shows "x \<in> carrier G \<Longrightarrow> x \<in> H +> x" |
26310 | 412 |
by (rule group.rcos_self [OF a_group _ a_subgroup, |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
413 |
folded a_r_coset_def, simplified monoid_record_simps]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
414 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
415 |
lemma (in abelian_subgroup) a_rcosets_part_G: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
416 |
shows "\<Union>(a_rcosets H) = carrier G" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
417 |
by (rule group.rcosets_part_G [OF a_group a_subgroup, |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
418 |
folded A_RCOSETS_def, simplified monoid_record_simps]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
419 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
420 |
lemma (in abelian_subgroup) a_cosets_finite: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
421 |
"\<lbrakk>c \<in> a_rcosets H; H \<subseteq> carrier G; finite (carrier G)\<rbrakk> \<Longrightarrow> finite c" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
422 |
by (rule group.cosets_finite [OF a_group, |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
423 |
folded A_RCOSETS_def, simplified monoid_record_simps]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
424 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
425 |
lemma (in abelian_group) a_card_cosets_equal: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
426 |
"\<lbrakk>c \<in> a_rcosets H; H \<subseteq> carrier G; finite(carrier G)\<rbrakk> |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
427 |
\<Longrightarrow> card c = card H" |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
428 |
by (simp add: A_RCOSETS_defs(1) add.card_rcosets_equal) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
429 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
430 |
lemma (in abelian_group) rcosets_subset_PowG: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
431 |
"additive_subgroup H G \<Longrightarrow> a_rcosets H \<subseteq> Pow(carrier G)" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
432 |
by (rule group.rcosets_subset_PowG [OF a_group, |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
433 |
folded A_RCOSETS_def, simplified monoid_record_simps], |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
434 |
rule additive_subgroup.a_subgroup) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
435 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
436 |
theorem (in abelian_group) a_lagrange: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
437 |
"\<lbrakk>finite(carrier G); additive_subgroup H G\<rbrakk> |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
438 |
\<Longrightarrow> card(a_rcosets H) * card(H) = order(G)" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
439 |
by (rule group.lagrange [OF a_group, |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
440 |
folded A_RCOSETS_def, simplified monoid_record_simps order_def, folded order_def]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
441 |
(fast intro!: additive_subgroup.a_subgroup)+ |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
442 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
443 |
|
61382 | 444 |
subsubsection \<open>Factorization\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
445 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
446 |
lemmas A_FactGroup_defs = A_FactGroup_def FactGroup_def |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
447 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
448 |
lemma A_FactGroup_def': |
27611 | 449 |
fixes G (structure) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
450 |
shows "G A_Mod H \<equiv> \<lparr>carrier = a_rcosets\<^bsub>G\<^esub> H, mult = set_add G, one = H\<rparr>" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
451 |
unfolding A_FactGroup_defs |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
452 |
by (fold A_RCOSETS_def set_add_def) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
453 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
454 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
455 |
lemma (in abelian_subgroup) a_setmult_closed: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
456 |
"\<lbrakk>K1 \<in> a_rcosets H; K2 \<in> a_rcosets H\<rbrakk> \<Longrightarrow> K1 <+> K2 \<in> a_rcosets H" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
457 |
by (rule normal.setmult_closed [OF a_normal, |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
458 |
folded A_RCOSETS_def set_add_def, simplified monoid_record_simps]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
459 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
460 |
lemma (in abelian_subgroup) a_setinv_closed: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
461 |
"K \<in> a_rcosets H \<Longrightarrow> a_set_inv K \<in> a_rcosets H" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
462 |
by (rule normal.setinv_closed [OF a_normal, |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
463 |
folded A_RCOSETS_def A_SET_INV_def, simplified monoid_record_simps]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
464 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
465 |
lemma (in abelian_subgroup) a_rcosets_assoc: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
466 |
"\<lbrakk>M1 \<in> a_rcosets H; M2 \<in> a_rcosets H; M3 \<in> a_rcosets H\<rbrakk> |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
467 |
\<Longrightarrow> M1 <+> M2 <+> M3 = M1 <+> (M2 <+> M3)" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
468 |
by (rule normal.rcosets_assoc [OF a_normal, |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
469 |
folded A_RCOSETS_def set_add_def, simplified monoid_record_simps]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
470 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
471 |
lemma (in abelian_subgroup) a_subgroup_in_rcosets: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
472 |
"H \<in> a_rcosets H" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
473 |
by (rule subgroup.subgroup_in_rcosets [OF a_subgroup a_group, |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
474 |
folded A_RCOSETS_def, simplified monoid_record_simps]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
475 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
476 |
lemma (in abelian_subgroup) a_rcosets_inv_mult_group_eq: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
477 |
"M \<in> a_rcosets H \<Longrightarrow> a_set_inv M <+> M = H" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
478 |
by (rule normal.rcosets_inv_mult_group_eq [OF a_normal, |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
479 |
folded A_RCOSETS_def A_SET_INV_def set_add_def, simplified monoid_record_simps]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
480 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
481 |
theorem (in abelian_subgroup) a_factorgroup_is_group: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
482 |
"group (G A_Mod H)" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
483 |
by (rule normal.factorgroup_is_group [OF a_normal, |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
484 |
folded A_FactGroup_def, simplified monoid_record_simps]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
485 |
|
61382 | 486 |
text \<open>Since the Factorization is based on an \emph{abelian} subgroup, is results in |
487 |
a commutative group\<close> |
|
68684 | 488 |
theorem (in abelian_subgroup) a_factorgroup_is_comm_group: "comm_group (G A_Mod H)" |
489 |
proof - |
|
490 |
have "Group.comm_monoid_axioms (G A_Mod H)" |
|
491 |
apply (rule comm_monoid_axioms.intro) |
|
492 |
apply (auto simp: A_FactGroup_def FactGroup_def RCOSETS_def a_normal add.m_comm normal.rcos_sum) |
|
493 |
done |
|
494 |
then show ?thesis |
|
495 |
by (intro comm_group.intro comm_monoid.intro) (simp_all add: a_factorgroup_is_group group.is_monoid) |
|
496 |
qed |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
497 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
498 |
lemma add_A_FactGroup [simp]: "X \<otimes>\<^bsub>(G A_Mod H)\<^esub> X' = X <+>\<^bsub>G\<^esub> X'" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
499 |
by (simp add: A_FactGroup_def set_add_def) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
500 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
501 |
lemma (in abelian_subgroup) a_inv_FactGroup: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
502 |
"X \<in> carrier (G A_Mod H) \<Longrightarrow> inv\<^bsub>G A_Mod H\<^esub> X = a_set_inv X" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
503 |
by (rule normal.inv_FactGroup [OF a_normal, |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
504 |
folded A_FactGroup_def A_SET_INV_def, simplified monoid_record_simps]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
505 |
|
69597 | 506 |
text\<open>The coset map is a homomorphism from \<^term>\<open>G\<close> to the quotient group |
507 |
\<^term>\<open>G Mod H\<close>\<close> |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
508 |
lemma (in abelian_subgroup) a_r_coset_hom_A_Mod: |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
509 |
"(\<lambda>a. H +> a) \<in> hom (add_monoid G) (G A_Mod H)" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
510 |
by (rule normal.r_coset_hom_Mod [OF a_normal, |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
511 |
folded A_FactGroup_def a_r_coset_def, simplified monoid_record_simps]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
512 |
|
61382 | 513 |
text \<open>The isomorphism theorems have been omitted from lifting, at |
514 |
least for now\<close> |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
515 |
|
35849 | 516 |
|
61382 | 517 |
subsubsection\<open>The First Isomorphism Theorem\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
518 |
|
61382 | 519 |
text\<open>The quotient by the kernel of a homomorphism is isomorphic to the |
520 |
range of that homomorphism.\<close> |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
521 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
522 |
lemmas a_kernel_defs = |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
523 |
a_kernel_def kernel_def |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
524 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
525 |
lemma a_kernel_def': |
35848
5443079512ea
slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents:
35847
diff
changeset
|
526 |
"a_kernel R S h = {x \<in> carrier R. h x = \<zero>\<^bsub>S\<^esub>}" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
527 |
by (rule a_kernel_def[unfolded kernel_def, simplified ring_record_simps]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
528 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
529 |
|
61382 | 530 |
subsubsection \<open>Homomorphisms\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
531 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
532 |
lemma abelian_group_homI: |
27611 | 533 |
assumes "abelian_group G" |
534 |
assumes "abelian_group H" |
|
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
535 |
assumes a_group_hom: "group_hom (add_monoid G) |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
536 |
(add_monoid H) h" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
537 |
shows "abelian_group_hom G H h" |
27611 | 538 |
proof - |
30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
29237
diff
changeset
|
539 |
interpret G: abelian_group G by fact |
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
29237
diff
changeset
|
540 |
interpret H: abelian_group H by fact |
45388 | 541 |
show ?thesis |
68684 | 542 |
by (intro abelian_group_hom.intro abelian_group_hom_axioms.intro |
543 |
G.abelian_group_axioms H.abelian_group_axioms a_group_hom) |
|
27611 | 544 |
qed |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
545 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
546 |
lemma (in abelian_group_hom) is_abelian_group_hom: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
547 |
"abelian_group_hom G H h" |
28823 | 548 |
.. |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
549 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
550 |
lemma (in abelian_group_hom) hom_add [simp]: |
67613 | 551 |
"[| x \<in> carrier G; y \<in> carrier G |] |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
552 |
==> h (x \<oplus>\<^bsub>G\<^esub> y) = h x \<oplus>\<^bsub>H\<^esub> h y" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
553 |
by (rule group_hom.hom_mult[OF a_group_hom, |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
554 |
simplified ring_record_simps]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
555 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
556 |
lemma (in abelian_group_hom) hom_closed [simp]: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
557 |
"x \<in> carrier G \<Longrightarrow> h x \<in> carrier H" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
558 |
by (rule group_hom.hom_closed[OF a_group_hom, |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
559 |
simplified ring_record_simps]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
560 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
561 |
lemma (in abelian_group_hom) zero_closed [simp]: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
562 |
"h \<zero> \<in> carrier H" |
68684 | 563 |
by simp |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
564 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
565 |
lemma (in abelian_group_hom) hom_zero [simp]: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
566 |
"h \<zero> = \<zero>\<^bsub>H\<^esub>" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
567 |
by (rule group_hom.hom_one[OF a_group_hom, |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
568 |
simplified ring_record_simps]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
569 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
570 |
lemma (in abelian_group_hom) a_inv_closed [simp]: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
571 |
"x \<in> carrier G ==> h (\<ominus>x) \<in> carrier H" |
68684 | 572 |
by simp |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
573 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
574 |
lemma (in abelian_group_hom) hom_a_inv [simp]: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
575 |
"x \<in> carrier G ==> h (\<ominus>x) = \<ominus>\<^bsub>H\<^esub> (h x)" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
576 |
by (rule group_hom.hom_inv[OF a_group_hom, |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
577 |
folded a_inv_def, simplified ring_record_simps]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
578 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
579 |
lemma (in abelian_group_hom) additive_subgroup_a_kernel: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
580 |
"additive_subgroup (a_kernel G H h) G" |
68684 | 581 |
by (simp add: additive_subgroup.intro a_group_hom a_kernel_def group_hom.subgroup_kernel) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
582 |
|
61382 | 583 |
text\<open>The kernel of a homomorphism is an abelian subgroup\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
584 |
lemma (in abelian_group_hom) abelian_subgroup_a_kernel: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
585 |
"abelian_subgroup (a_kernel G H h) G" |
68684 | 586 |
apply (rule abelian_subgroupI) |
587 |
apply (simp add: G.abelian_group_axioms abelian_subgroup.a_normal abelian_subgroupI3 additive_subgroup_a_kernel) |
|
588 |
apply (simp add: G.a_comm) |
|
589 |
done |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
590 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
591 |
lemma (in abelian_group_hom) A_FactGroup_nonempty: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
592 |
assumes X: "X \<in> carrier (G A_Mod a_kernel G H h)" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
593 |
shows "X \<noteq> {}" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
594 |
by (rule group_hom.FactGroup_nonempty[OF a_group_hom, |
23350 | 595 |
folded a_kernel_def A_FactGroup_def, simplified ring_record_simps]) (rule X) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
596 |
|
39910 | 597 |
lemma (in abelian_group_hom) FactGroup_the_elem_mem: |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
598 |
assumes X: "X \<in> carrier (G A_Mod (a_kernel G H h))" |
39910 | 599 |
shows "the_elem (h`X) \<in> carrier H" |
600 |
by (rule group_hom.FactGroup_the_elem_mem[OF a_group_hom, |
|
23350 | 601 |
folded a_kernel_def A_FactGroup_def, simplified ring_record_simps]) (rule X) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
602 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
603 |
lemma (in abelian_group_hom) A_FactGroup_hom: |
39910 | 604 |
"(\<lambda>X. the_elem (h`X)) \<in> hom (G A_Mod (a_kernel G H h)) |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
605 |
(add_monoid H)" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
606 |
by (rule group_hom.FactGroup_hom[OF a_group_hom, |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
607 |
folded a_kernel_def A_FactGroup_def, simplified ring_record_simps]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
608 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
609 |
lemma (in abelian_group_hom) A_FactGroup_inj_on: |
39910 | 610 |
"inj_on (\<lambda>X. the_elem (h ` X)) (carrier (G A_Mod a_kernel G H h))" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
611 |
by (rule group_hom.FactGroup_inj_on[OF a_group_hom, |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
612 |
folded a_kernel_def A_FactGroup_def, simplified ring_record_simps]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
613 |
|
69597 | 614 |
text\<open>If the homomorphism \<^term>\<open>h\<close> is onto \<^term>\<open>H\<close>, then so is the |
61382 | 615 |
homomorphism from the quotient group\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
616 |
lemma (in abelian_group_hom) A_FactGroup_onto: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
617 |
assumes h: "h ` carrier G = carrier H" |
39910 | 618 |
shows "(\<lambda>X. the_elem (h ` X)) ` carrier (G A_Mod a_kernel G H h) = carrier H" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
619 |
by (rule group_hom.FactGroup_onto[OF a_group_hom, |
23350 | 620 |
folded a_kernel_def A_FactGroup_def, simplified ring_record_simps]) (rule h) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
621 |
|
69597 | 622 |
text\<open>If \<^term>\<open>h\<close> is a homomorphism from \<^term>\<open>G\<close> onto \<^term>\<open>H\<close>, then the |
623 |
quotient group \<^term>\<open>G Mod (kernel G H h)\<close> is isomorphic to \<^term>\<open>H\<close>.\<close> |
|
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
624 |
theorem (in abelian_group_hom) A_FactGroup_iso_set: |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
625 |
"h ` carrier G = carrier H |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
626 |
\<Longrightarrow> (\<lambda>X. the_elem (h`X)) \<in> iso (G A_Mod (a_kernel G H h)) (add_monoid H)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
627 |
by (rule group_hom.FactGroup_iso_set[OF a_group_hom, |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
628 |
folded a_kernel_def A_FactGroup_def, simplified ring_record_simps]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
629 |
|
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
630 |
corollary (in abelian_group_hom) A_FactGroup_iso : |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
631 |
"h ` carrier G = carrier H |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
632 |
\<Longrightarrow> (G A_Mod (a_kernel G H h)) \<cong> (add_monoid H)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
633 |
using A_FactGroup_iso_set unfolding is_iso_def by auto |
35849 | 634 |
|
61382 | 635 |
subsubsection \<open>Cosets\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
636 |
|
61382 | 637 |
text \<open>Not eveything from \texttt{CosetExt.thy} is lifted here.\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
638 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
639 |
lemma (in additive_subgroup) a_Hcarr [simp]: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
640 |
assumes hH: "h \<in> H" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
641 |
shows "h \<in> carrier G" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
642 |
by (rule subgroup.mem_carrier [OF a_subgroup, |
23350 | 643 |
simplified monoid_record_simps]) (rule hH) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
644 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
645 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
646 |
lemma (in abelian_subgroup) a_elemrcos_carrier: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
647 |
assumes acarr: "a \<in> carrier G" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
648 |
and a': "a' \<in> H +> a" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
649 |
shows "a' \<in> carrier G" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
650 |
by (rule subgroup.elemrcos_carrier [OF a_subgroup a_group, |
23350 | 651 |
folded a_r_coset_def, simplified monoid_record_simps]) (rule acarr, rule a') |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
652 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
653 |
lemma (in abelian_subgroup) a_rcos_const: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
654 |
assumes hH: "h \<in> H" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
655 |
shows "H +> h = H" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
656 |
by (rule subgroup.rcos_const [OF a_subgroup a_group, |
23350 | 657 |
folded a_r_coset_def, simplified monoid_record_simps]) (rule hH) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
658 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
659 |
lemma (in abelian_subgroup) a_rcos_module_imp: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
660 |
assumes xcarr: "x \<in> carrier G" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
661 |
and x'cos: "x' \<in> H +> x" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
662 |
shows "(x' \<oplus> \<ominus>x) \<in> H" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
663 |
by (rule subgroup.rcos_module_imp [OF a_subgroup a_group, |
23350 | 664 |
folded a_r_coset_def a_inv_def, simplified monoid_record_simps]) (rule xcarr, rule x'cos) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
665 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
666 |
lemma (in abelian_subgroup) a_rcos_module_rev: |
23350 | 667 |
assumes "x \<in> carrier G" "x' \<in> carrier G" |
668 |
and "(x' \<oplus> \<ominus>x) \<in> H" |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
669 |
shows "x' \<in> H +> x" |
23350 | 670 |
using assms |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
671 |
by (rule subgroup.rcos_module_rev [OF a_subgroup a_group, |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
672 |
folded a_r_coset_def a_inv_def, simplified monoid_record_simps]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
673 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
674 |
lemma (in abelian_subgroup) a_rcos_module: |
23350 | 675 |
assumes "x \<in> carrier G" "x' \<in> carrier G" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
676 |
shows "(x' \<in> H +> x) = (x' \<oplus> \<ominus>x \<in> H)" |
23350 | 677 |
using assms |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
678 |
by (rule subgroup.rcos_module [OF a_subgroup a_group, |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
679 |
folded a_r_coset_def a_inv_def, simplified monoid_record_simps]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
680 |
|
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
67091
diff
changeset
|
681 |
\<comment> \<open>variant\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
682 |
lemma (in abelian_subgroup) a_rcos_module_minus: |
27611 | 683 |
assumes "ring G" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
684 |
assumes carr: "x \<in> carrier G" "x' \<in> carrier G" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
685 |
shows "(x' \<in> H +> x) = (x' \<ominus> x \<in> H)" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
686 |
proof - |
30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
29237
diff
changeset
|
687 |
interpret G: ring G by fact |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
688 |
from carr |
23350 | 689 |
have "(x' \<in> H +> x) = (x' \<oplus> \<ominus>x \<in> H)" by (rule a_rcos_module) |
690 |
with carr |
|
691 |
show "(x' \<in> H +> x) = (x' \<ominus> x \<in> H)" |
|
692 |
by (simp add: minus_eq) |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
693 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
694 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
695 |
lemma (in abelian_subgroup) a_repr_independence': |
68684 | 696 |
assumes "y \<in> H +> x" "x \<in> carrier G" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
697 |
shows "H +> x = H +> y" |
68684 | 698 |
using a_repr_independence a_subgroup assms by blast |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
699 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
700 |
lemma (in abelian_subgroup) a_repr_independenceD: |
68684 | 701 |
assumes "y \<in> carrier G" "H +> x = H +> y" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
702 |
shows "y \<in> H +> x" |
68684 | 703 |
by (simp add: a_rcos_self assms) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
704 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
705 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
706 |
lemma (in abelian_subgroup) a_rcosets_carrier: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
707 |
"X \<in> a_rcosets H \<Longrightarrow> X \<subseteq> carrier G" |
68684 | 708 |
using a_rcosets_part_G by auto |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
709 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
710 |
|
61382 | 711 |
subsubsection \<open>Addition of Subgroups\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
712 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
713 |
lemma (in abelian_monoid) set_add_closed: |
68684 | 714 |
assumes "A \<subseteq> carrier G" "B \<subseteq> carrier G" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
715 |
shows "A <+> B \<subseteq> carrier G" |
68684 | 716 |
by (simp add: assms add.set_mult_closed set_add_defs(1)) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
717 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
718 |
lemma (in abelian_group) add_additive_subgroups: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
719 |
assumes subH: "additive_subgroup H G" |
68684 | 720 |
and subK: "additive_subgroup K G" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
721 |
shows "additive_subgroup (H <+> K) G" |
68684 | 722 |
unfolding set_add_def |
723 |
using add.mult_subgroups additive_subgroup_def subH subK |
|
724 |
by (blast intro: additive_subgroup.intro) |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
725 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
726 |
end |