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