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