(*  Title:      HOL/Algebra/Exact_Sequence.thy
    Author:     Martin Baillon
*)

theory Exact_Sequence
  imports Group Coset Solvable_Groups
begin

section \<open>Exact Sequences\<close>


subsection \<open>Definitions\<close>

inductive exact_seq :: "'a monoid list \<times> ('a \<Rightarrow> 'a) list \<Rightarrow> bool"  where
unity:     " group_hom G1 G2 f \<Longrightarrow> exact_seq ([G2, G1], [f])" |
extension: "\<lbrakk> exact_seq ((G # K # l), (g # q)); group H ; h \<in> hom G H ;
              kernel G H h = image g (carrier K) \<rbrakk> \<Longrightarrow> exact_seq (H # G # K # l, h # g # q)"

abbreviation exact_seq_arrow ::
  "('a \<Rightarrow> 'a) \<Rightarrow> 'a monoid list \<times> ('a \<Rightarrow> 'a) list \<Rightarrow>  'a monoid \<Rightarrow> 'a monoid list \<times> ('a \<Rightarrow> 'a) list"
  ("(3_ / \<longlongrightarrow>\<index> _)" [1000, 60])
  where "exact_seq_arrow  f t G \<equiv> (G # (fst t), f # (snd t))"


subsection \<open>Basic Properties\<close>

lemma exact_seq_length1: "exact_seq t \<Longrightarrow> length (fst t) = Suc (length (snd t))"
  by (induct t rule: exact_seq.induct) auto

lemma exact_seq_length2: "exact_seq t \<Longrightarrow> length (snd t) \<ge> Suc 0"
  by (induct t rule: exact_seq.induct) auto

lemma dropped_seq_is_exact_seq:
  assumes "exact_seq (G, F)" and "(i :: nat) < length F"
  shows "exact_seq (drop i G, drop i F)"
proof-
  { fix t i assume "exact_seq t" "i < length (snd t)"
    hence "exact_seq (drop i (fst t), drop i (snd t))"
    proof (induction arbitrary: i)
      case (unity G1 G2 f) thus ?case
        by (simp add: exact_seq.unity)
    next
      case (extension G K l g q H h) show ?case
      proof (cases)
        assume "i = 0" thus ?case
          using exact_seq.extension[OF extension.hyps] by simp
      next
        assume "i \<noteq> 0" hence "i \<ge> Suc 0" by simp
        then obtain k where "k < length (snd (G # K # l, g # q))" "i = Suc k"
          using Suc_le_D extension.prems by auto
        thus ?thesis using extension.IH by simp 
      qed
    qed }

  thus ?thesis using assms by auto
qed

lemma truncated_seq_is_exact_seq:
  assumes "exact_seq (l, q)" and "length l \<ge> 3"
  shows "exact_seq (tl l, tl q)"
  using exact_seq_length1[OF assms(1)] dropped_seq_is_exact_seq[OF assms(1), of "Suc 0"]
        exact_seq_length2[OF assms(1)] assms(2) by (simp add: drop_Suc)

lemma exact_seq_imp_exact_hom:
   assumes "exact_seq (G1 # l,q) \<longlongrightarrow>\<^bsub>g1\<^esub> G2 \<longlongrightarrow>\<^bsub>g2\<^esub> G3"
   shows "g1 ` (carrier G1) = kernel G2 G3 g2"
proof-
  { fix t assume "exact_seq t" and "length (fst t) \<ge> 3 \<and> length (snd t) \<ge> 2"
    hence "(hd (tl (snd t))) ` (carrier (hd (tl (tl (fst t))))) =
            kernel (hd (tl (fst t))) (hd (fst t)) (hd (snd t))"
    proof (induction)
      case (unity G1 G2 f)
      then show ?case by auto
    next
      case (extension G l g q H h)
      then show ?case by auto
    qed }
  thus ?thesis using assms by fastforce
qed

lemma exact_seq_imp_exact_hom_arbitrary:
   assumes "exact_seq (G, F)"
     and "Suc i < length F"
   shows "(F ! (Suc i)) ` (carrier (G ! (Suc (Suc i)))) = kernel (G ! (Suc i)) (G ! i) (F ! i)"
proof -
  have "length (drop i F) \<ge> 2" "length (drop i G) \<ge> 3"
    using assms(2) exact_seq_length1[OF assms(1)] by auto
  then obtain l q
    where "drop i G = (G ! i) # (G ! (Suc i)) # (G ! (Suc (Suc i))) # l"
     and  "drop i F = (F ! i) # (F ! (Suc i)) # q"
    by (metis Cons_nth_drop_Suc Suc_less_eq assms exact_seq_length1 fst_conv
        le_eq_less_or_eq le_imp_less_Suc prod.sel(2))
  thus ?thesis
  using dropped_seq_is_exact_seq[OF assms(1), of i] assms(2)
        exact_seq_imp_exact_hom[of "G ! i" "G ! (Suc i)" "G ! (Suc (Suc i))" l q] by auto
qed

lemma exact_seq_imp_group_hom :
  assumes "exact_seq ((G # l, q)) \<longlongrightarrow>\<^bsub>g\<^esub> H"
  shows "group_hom G H g"
proof-
  { fix t assume "exact_seq t"
    hence "group_hom (hd (tl (fst t))) (hd (fst t)) (hd(snd t))"
    proof (induction)
      case (unity G1 G2 f)
      then show ?case by auto
    next
      case (extension G l g q H h)
      then show ?case unfolding group_hom_def group_hom_axioms_def by auto
    qed }
  note aux_lemma = this
  show ?thesis using aux_lemma[OF assms]
    by simp
qed

lemma exact_seq_imp_group_hom_arbitrary:
  assumes "exact_seq (G, F)" and "(i :: nat) < length F"
  shows "group_hom (G ! (Suc i)) (G ! i) (F ! i)"
proof -
  have "length (drop i F) \<ge> 1" "length (drop i G) \<ge> 2"
    using assms(2) exact_seq_length1[OF assms(1)] by auto
  then obtain l q
    where "drop i G = (G ! i) # (G ! (Suc i)) # l"
     and  "drop i F = (F ! i) # q"
    by (metis Cons_nth_drop_Suc Suc_leI assms exact_seq_length1 fst_conv
        le_eq_less_or_eq le_imp_less_Suc prod.sel(2))
  thus ?thesis
  using dropped_seq_is_exact_seq[OF assms(1), of i] assms(2)
        exact_seq_imp_group_hom[of "G ! i" "G ! (Suc i)" l q "F ! i"] by simp
qed


subsection \<open>Link Between Exact Sequences and Solvable Conditions\<close>

lemma exact_seq_solvable_imp :
  assumes "exact_seq ([G1],[]) \<longlongrightarrow>\<^bsub>g1\<^esub> G2 \<longlongrightarrow>\<^bsub>g2\<^esub> G3"
    and "inj_on g1 (carrier G1)"
    and "g2 ` (carrier G2) = carrier G3"
  shows "solvable G2 \<Longrightarrow> (solvable G1) \<and> (solvable G3)"
proof -
  assume G2: "solvable G2"
  have "group_hom G1 G2 g1"
    using exact_seq_imp_group_hom_arbitrary[OF assms(1), of "Suc 0"] by simp
  hence "solvable G1"
    using group_hom.inj_hom_imp_solvable[of G1 G2 g1] assms(2) G2 by simp
  moreover have "group_hom G2 G3 g2"
    using exact_seq_imp_group_hom_arbitrary[OF assms(1), of 0] by simp
  hence "solvable G3"
    using group_hom.surj_hom_imp_solvable[of G2 G3 g2] assms(3) G2 by simp
  ultimately show ?thesis by simp
qed

lemma exact_seq_solvable_recip :
  assumes "exact_seq ([G1],[]) \<longlongrightarrow>\<^bsub>g1\<^esub> G2 \<longlongrightarrow>\<^bsub>g2\<^esub> G3"
    and "inj_on g1 (carrier G1)"
    and "g2 ` (carrier G2) = carrier G3"
  shows "(solvable G1) \<and> (solvable G3) \<Longrightarrow> solvable G2"
proof -
  assume "(solvable G1) \<and> (solvable G3)"
  hence G1: "solvable G1" and G3: "solvable G3" by auto
  have g1: "group_hom G1 G2 g1" and g2: "group_hom G2 G3 g2"
    using exact_seq_imp_group_hom_arbitrary[OF assms(1), of "Suc 0"]
          exact_seq_imp_group_hom_arbitrary[OF assms(1), of 0] by auto
  show ?thesis
    using solvable_condition[OF g1 g2 assms(3)]
          exact_seq_imp_exact_hom[OF assms(1)] G1 G3 by auto
qed

proposition exact_seq_solvable_iff :
  assumes "exact_seq ([G1],[]) \<longlongrightarrow>\<^bsub>g1\<^esub> G2 \<longlongrightarrow>\<^bsub>g2\<^esub> G3"
    and "inj_on g1 (carrier G1)"
    and "g2 ` (carrier G2) = carrier G3"
  shows "(solvable G1) \<and> (solvable G3) \<longleftrightarrow>  solvable G2"
  using exact_seq_solvable_recip exact_seq_solvable_imp assms by blast

end