68578
|
1 |
(* ************************************************************************** *)
|
|
2 |
(* Title: Exact_Sequence.thy *)
|
|
3 |
(* Author: Martin Baillon *)
|
|
4 |
(* ************************************************************************** *)
|
|
5 |
|
|
6 |
theory Exact_Sequence
|
|
7 |
imports Group Coset Solvable_Groups
|
|
8 |
|
|
9 |
begin
|
|
10 |
|
|
11 |
section \<open>Exact Sequences\<close>
|
|
12 |
|
|
13 |
|
|
14 |
subsection \<open>Definitions\<close>
|
|
15 |
|
|
16 |
inductive exact_seq :: "'a monoid list \<times> ('a \<Rightarrow> 'a) list \<Rightarrow> bool" where
|
|
17 |
unity: " group_hom G1 G2 f \<Longrightarrow> exact_seq ([G2, G1], [f])" |
|
|
18 |
extension: "\<lbrakk> exact_seq ((G # K # l), (g # q)); group H ; h \<in> hom G H ;
|
|
19 |
kernel G H h = image g (carrier K) \<rbrakk> \<Longrightarrow> exact_seq (H # G # K # l, h # g # q)"
|
|
20 |
|
|
21 |
abbreviation exact_seq_arrow ::
|
|
22 |
"('a \<Rightarrow> 'a) \<Rightarrow> 'a monoid list \<times> ('a \<Rightarrow> 'a) list \<Rightarrow> 'a monoid \<Rightarrow> 'a monoid list \<times> ('a \<Rightarrow> 'a) list"
|
|
23 |
("(3_ / \<longlongrightarrow>\<index> _)" [1000, 60])
|
|
24 |
where "exact_seq_arrow f t G \<equiv> (G # (fst t), f # (snd t))"
|
|
25 |
|
|
26 |
|
|
27 |
subsection \<open>Basic Properties\<close>
|
|
28 |
|
|
29 |
lemma exact_seq_length1: "exact_seq t \<Longrightarrow> length (fst t) = Suc (length (snd t))"
|
|
30 |
by (induct t rule: exact_seq.induct) auto
|
|
31 |
|
|
32 |
lemma exact_seq_length2: "exact_seq t \<Longrightarrow> length (snd t) \<ge> Suc 0"
|
|
33 |
by (induct t rule: exact_seq.induct) auto
|
|
34 |
|
|
35 |
lemma dropped_seq_is_exact_seq:
|
|
36 |
assumes "exact_seq (G, F)" and "(i :: nat) < length F"
|
|
37 |
shows "exact_seq (drop i G, drop i F)"
|
|
38 |
proof-
|
|
39 |
{ fix t i assume "exact_seq t" "i < length (snd t)"
|
|
40 |
hence "exact_seq (drop i (fst t), drop i (snd t))"
|
|
41 |
proof (induction arbitrary: i)
|
|
42 |
case (unity G1 G2 f) thus ?case
|
|
43 |
by (simp add: exact_seq.unity)
|
|
44 |
next
|
|
45 |
case (extension G K l g q H h) show ?case
|
|
46 |
proof (cases)
|
|
47 |
assume "i = 0" thus ?case
|
|
48 |
using exact_seq.extension[OF extension.hyps] by simp
|
|
49 |
next
|
|
50 |
assume "i \<noteq> 0" hence "i \<ge> Suc 0" by simp
|
|
51 |
then obtain k where "k < length (snd (G # K # l, g # q))" "i = Suc k"
|
|
52 |
using Suc_le_D extension.prems by auto
|
|
53 |
thus ?thesis using extension.IH by simp
|
|
54 |
qed
|
|
55 |
qed }
|
|
56 |
|
|
57 |
thus ?thesis using assms by auto
|
|
58 |
qed
|
|
59 |
|
|
60 |
lemma truncated_seq_is_exact_seq:
|
|
61 |
assumes "exact_seq (l, q)" and "length l \<ge> 3"
|
|
62 |
shows "exact_seq (tl l, tl q)"
|
|
63 |
using exact_seq_length1[OF assms(1)] dropped_seq_is_exact_seq[OF assms(1), of "Suc 0"]
|
|
64 |
exact_seq_length2[OF assms(1)] assms(2) by (simp add: drop_Suc)
|
|
65 |
|
|
66 |
lemma exact_seq_imp_exact_hom:
|
|
67 |
assumes "exact_seq (G1 # l,q) \<longlongrightarrow>\<^bsub>g1\<^esub> G2 \<longlongrightarrow>\<^bsub>g2\<^esub> G3"
|
|
68 |
shows "g1 ` (carrier G1) = kernel G2 G3 g2"
|
|
69 |
proof-
|
|
70 |
{ fix t assume "exact_seq t" and "length (fst t) \<ge> 3 \<and> length (snd t) \<ge> 2"
|
|
71 |
hence "(hd (tl (snd t))) ` (carrier (hd (tl (tl (fst t))))) =
|
|
72 |
kernel (hd (tl (fst t))) (hd (fst t)) (hd (snd t))"
|
|
73 |
proof (induction)
|
|
74 |
case (unity G1 G2 f)
|
|
75 |
then show ?case by auto
|
|
76 |
next
|
|
77 |
case (extension G l g q H h)
|
|
78 |
then show ?case by auto
|
|
79 |
qed }
|
|
80 |
thus ?thesis using assms by fastforce
|
|
81 |
qed
|
|
82 |
|
|
83 |
lemma exact_seq_imp_exact_hom_arbitrary:
|
|
84 |
assumes "exact_seq (G, F)"
|
|
85 |
and "Suc i < length F"
|
|
86 |
shows "(F ! (Suc i)) ` (carrier (G ! (Suc (Suc i)))) = kernel (G ! (Suc i)) (G ! i) (F ! i)"
|
|
87 |
proof -
|
|
88 |
have "length (drop i F) \<ge> 2" "length (drop i G) \<ge> 3"
|
|
89 |
using assms(2) exact_seq_length1[OF assms(1)] by auto
|
|
90 |
then obtain l q
|
|
91 |
where "drop i G = (G ! i) # (G ! (Suc i)) # (G ! (Suc (Suc i))) # l"
|
|
92 |
and "drop i F = (F ! i) # (F ! (Suc i)) # q"
|
|
93 |
by (metis Cons_nth_drop_Suc Suc_less_eq assms exact_seq_length1 fst_conv
|
|
94 |
le_eq_less_or_eq le_imp_less_Suc prod.sel(2))
|
|
95 |
thus ?thesis
|
|
96 |
using dropped_seq_is_exact_seq[OF assms(1), of i] assms(2)
|
|
97 |
exact_seq_imp_exact_hom[of "G ! i" "G ! (Suc i)" "G ! (Suc (Suc i))" l q] by auto
|
|
98 |
qed
|
|
99 |
|
|
100 |
lemma exact_seq_imp_group_hom :
|
|
101 |
assumes "exact_seq ((G # l, q)) \<longlongrightarrow>\<^bsub>g\<^esub> H"
|
|
102 |
shows "group_hom G H g"
|
|
103 |
proof-
|
|
104 |
{ fix t assume "exact_seq t"
|
|
105 |
hence "group_hom (hd (tl (fst t))) (hd (fst t)) (hd(snd t))"
|
|
106 |
proof (induction)
|
|
107 |
case (unity G1 G2 f)
|
|
108 |
then show ?case by auto
|
|
109 |
next
|
|
110 |
case (extension G l g q H h)
|
|
111 |
then show ?case unfolding group_hom_def group_hom_axioms_def by auto
|
|
112 |
qed }
|
|
113 |
note aux_lemma = this
|
|
114 |
show ?thesis using aux_lemma[OF assms]
|
|
115 |
by simp
|
|
116 |
qed
|
|
117 |
|
|
118 |
lemma exact_seq_imp_group_hom_arbitrary:
|
|
119 |
assumes "exact_seq (G, F)" and "(i :: nat) < length F"
|
|
120 |
shows "group_hom (G ! (Suc i)) (G ! i) (F ! i)"
|
|
121 |
proof -
|
|
122 |
have "length (drop i F) \<ge> 1" "length (drop i G) \<ge> 2"
|
|
123 |
using assms(2) exact_seq_length1[OF assms(1)] by auto
|
|
124 |
then obtain l q
|
|
125 |
where "drop i G = (G ! i) # (G ! (Suc i)) # l"
|
|
126 |
and "drop i F = (F ! i) # q"
|
|
127 |
by (metis Cons_nth_drop_Suc Suc_leI assms exact_seq_length1 fst_conv
|
|
128 |
le_eq_less_or_eq le_imp_less_Suc prod.sel(2))
|
|
129 |
thus ?thesis
|
|
130 |
using dropped_seq_is_exact_seq[OF assms(1), of i] assms(2)
|
|
131 |
exact_seq_imp_group_hom[of "G ! i" "G ! (Suc i)" l q "F ! i"] by simp
|
|
132 |
qed
|
|
133 |
|
|
134 |
|
|
135 |
subsection \<open>Link Between Exact Sequences and Solvable Conditions\<close>
|
|
136 |
|
|
137 |
lemma exact_seq_solvable_imp :
|
|
138 |
assumes "exact_seq ([G1],[]) \<longlongrightarrow>\<^bsub>g1\<^esub> G2 \<longlongrightarrow>\<^bsub>g2\<^esub> G3"
|
|
139 |
and "inj_on g1 (carrier G1)"
|
|
140 |
and "g2 ` (carrier G2) = carrier G3"
|
|
141 |
shows "solvable G2 \<Longrightarrow> (solvable G1) \<and> (solvable G3)"
|
|
142 |
proof -
|
|
143 |
assume G2: "solvable G2"
|
|
144 |
have "group_hom G1 G2 g1"
|
|
145 |
using exact_seq_imp_group_hom_arbitrary[OF assms(1), of "Suc 0"] by simp
|
|
146 |
hence "solvable G1"
|
|
147 |
using group_hom.inj_hom_imp_solvable[of G1 G2 g1] assms(2) G2 by simp
|
|
148 |
moreover have "group_hom G2 G3 g2"
|
|
149 |
using exact_seq_imp_group_hom_arbitrary[OF assms(1), of 0] by simp
|
|
150 |
hence "solvable G3"
|
|
151 |
using group_hom.surj_hom_imp_solvable[of G2 G3 g2] assms(3) G2 by simp
|
|
152 |
ultimately show ?thesis by simp
|
|
153 |
qed
|
|
154 |
|
|
155 |
lemma exact_seq_solvable_recip :
|
|
156 |
assumes "exact_seq ([G1],[]) \<longlongrightarrow>\<^bsub>g1\<^esub> G2 \<longlongrightarrow>\<^bsub>g2\<^esub> G3"
|
|
157 |
and "inj_on g1 (carrier G1)"
|
|
158 |
and "g2 ` (carrier G2) = carrier G3"
|
|
159 |
shows "(solvable G1) \<and> (solvable G3) \<Longrightarrow> solvable G2"
|
|
160 |
proof -
|
|
161 |
assume "(solvable G1) \<and> (solvable G3)"
|
|
162 |
hence G1: "solvable G1" and G3: "solvable G3" by auto
|
|
163 |
have g1: "group_hom G1 G2 g1" and g2: "group_hom G2 G3 g2"
|
|
164 |
using exact_seq_imp_group_hom_arbitrary[OF assms(1), of "Suc 0"]
|
|
165 |
exact_seq_imp_group_hom_arbitrary[OF assms(1), of 0] by auto
|
|
166 |
show ?thesis
|
|
167 |
using solvable_condition[OF g1 g2 assms(3)]
|
|
168 |
exact_seq_imp_exact_hom[OF assms(1)] G1 G3 by auto
|
|
169 |
qed
|
|
170 |
|
|
171 |
proposition exact_seq_solvable_iff :
|
|
172 |
assumes "exact_seq ([G1],[]) \<longlongrightarrow>\<^bsub>g1\<^esub> G2 \<longlongrightarrow>\<^bsub>g2\<^esub> G3"
|
|
173 |
and "inj_on g1 (carrier G1)"
|
|
174 |
and "g2 ` (carrier G2) = carrier G3"
|
|
175 |
shows "(solvable G1) \<and> (solvable G3) \<longleftrightarrow> solvable G2"
|
|
176 |
using exact_seq_solvable_recip exact_seq_solvable_imp assms by blast
|
|
177 |
|
|
178 |
end
|
|
179 |
|