Theory Solvable_Transfer

section ‹Transfer of Solvability›

theory Solvable_Transfer
  imports Commutator
begin

text ‹
  Solvability transfers along the basic group constructions: it passes to homomorphic
  (in particular quotient) images, and to subgroups.  These are the load-bearing
  facts connecting a solvable group to its subquotients.
›

context group_homomorphism
begin

text ‹A homomorphism carries commutators to commutators.›
lemma image_commutator_elt:
  assumes "a ∈ G" "b ∈ G"
  shows "η (source.commutator_elt a b) = target.commutator_elt (η a) (η b)"
proof -
  have "η (source.commutator_elt a b) = η a ⋅' η b ⋅' inverse' (η a) ⋅' inverse' (η b)"
    using assms by (simp add: source.commutator_elt_def commutes_with_composition 
        invertible_commutes_with_inverse)
  also have "… = target.commutator_elt (η a) (η b)"
    using assms by (simp add: target.commutator_elt_def)
  finally show ?thesis .
qed

text ‹The image of a generated subgroup is contained in the subgroup generated by the image.›
lemma image_generate_sub: "η ` source.generate S ⊆ target.generate (η ` (S ∩ G))"
proof
  fix y assume "y ∈ η ` source.generate S"
  then obtain x where x: "x ∈ source.generate S" and yx: "y = η x" by auto
  from x have "η x ∈ target.generate (η ` (S ∩ G))"
  proof induction
    case unit
    then show ?case using commutes_with_unit target.generate.unit by simp
  next
    case (incl x)
    then have "η x ∈ η ` (S ∩ G) ∩ G'" by auto
    then show ?case by (rule target.generate.incl)
  next
    case (comp x y)
    have xG: "x ∈ G" "y ∈ G" using comp.hyps source.generate_subset_carrier by auto
    have "η (x ⋅ y) = η x ⋅' η y" using xG by (simp add: commutes_with_composition)
    then show ?case using comp.IH by (simp add: target.generate.comp)
  next
    case (inv x)
    have xG: "x ∈ G" using inv.hyps source.generate_subset_carrier by auto
    have "η (inverse x) = inverse' (η x)" using xG by (simp add: invertible_commutes_with_inverse)
    then show ?case using inv.IH by (simp add: target.generate.inv)
  qed
  then show "y ∈ target.generate (η ` (S ∩ G))" using yx by simp
qed

text ‹The reverse: the subgroup generated by the image is contained in the image of the
  generated subgroup.  (No surjectivity needed.)›
lemma image_generate_super: "target.generate (η ` (S ∩ G)) ⊆ η ` source.generate S"
proof
  fix y assume "y ∈ target.generate (η ` (S ∩ G))"
  then show "y ∈ η ` source.generate S"
  proof induction
    case unit
    then show ?case using commutes_with_unit source.generate.unit by force
  next
    case (incl x)
    then show ?case using source.generate.incl by force
  next
    case (comp x y)
    then obtain a b where §: "a ∈ source.generate S" "x = η a" "b ∈ source.generate S" "y = η b"  "a ∈ G" "b ∈ G" 
      using source.generate_subset_carrier by auto
    then have "a ⋅ b ∈ source.generate S" using source.generate.comp by blast
    with § show ?case by (metis commutes_with_composition image_eqI)
  next
    case (inv x)
    then obtain a where a: "a ∈ source.generate S" "x = η a" "a ∈ G" 
      using source.generate_subset_carrier by auto
    then show ?case
      by (metis source.generate.inv image_eqI invertible_commutes_with_inverse source.invertible)
  qed
qed

text ‹Hence the image of a commutator subgroup is the commutator subgroup of the images.›
lemma image_commutator_subgroup_sub:
  assumes "H ⊆ G" "K ⊆ G"
  shows "η ` source.commutator_subgroup H K ⊆ target.commutator_subgroup (η ` H) (η ` K)"
proof -
  have genset_sub: "{ target.commutator_elt h' k' | h' k'. h' ∈ η ` H ∧ k' ∈ η ` K } ⊆ G'"
    using assms by force
  have "η ` source.commutator_subgroup H K
          ⊆ target.generate (η ` (({ source.commutator_elt h k | h k. h ∈ H ∧ k ∈ K } ∩ G) ∩ G))"
    using image_generate_sub source.Gen_def source.commutator_subgroup_def by presburger
  also have "η ` (({ source.commutator_elt h k | h k. h ∈ H ∧ k ∈ K } ∩ G) ∩ G)
               ⊆ { target.commutator_elt h' k' | h' k'. h' ∈ η ` H ∧ k' ∈ η ` K }"
    using assms by (force simp: image_def image_commutator_elt)
  then have "target.generate (η ` (({ source.commutator_elt h k | h k. h ∈ H ∧ k ∈ K } ∩ G) ∩ G))
               ⊆ target.generate { target.commutator_elt h' k' | h' k'. h' ∈ η ` H ∧ k' ∈ η ` K }"
    by (rule target.generate_mono)
  also have "… = target.commutator_subgroup (η ` H) (η ` K)"
    using genset_sub by (simp add: target.commutator_subgroup_def target.Gen_def Int_absorb2)
  finally show ?thesis .
qed

lemma image_commutator_subgroup_super:
  assumes "H ⊆ G" "K ⊆ G"
  shows "target.commutator_subgroup (η ` H) (η ` K) ⊆ η ` source.commutator_subgroup H K"
proof -
  have seteq: "{ target.commutator_elt h' k' | h' k'. h' ∈ η ` H ∧ k' ∈ η ` K } ∩ G'
                 ⊆ η ` ({ source.commutator_elt h k | h k. h ∈ H ∧ k ∈ K } ∩ G)"
    using assms by (force simp: image_def image_commutator_elt)
  have "target.commutator_subgroup (η ` H) (η ` K)
         ⊆ target.generate (η ` ({ source.commutator_elt h k | h k. h ∈ H ∧ k ∈ K } ∩ G))"
    by (simp add: seteq target.Gen_def target.commutator_subgroup_def target.generate_mono)
  also have "… ⊆ η ` source.commutator_subgroup H K"
    using image_generate_super  
    by (fastforce simp add: source.commutator_subgroup_def source.Gen_def)
  finally show ?thesis .
qed

lemma image_commutator_subgroup_eq:
  assumes "H ⊆ G" "K ⊆ G"
  shows "η ` source.commutator_subgroup H K = target.commutator_subgroup (η ` H) (η ` K)"
  by (meson assms image_commutator_subgroup_sub image_commutator_subgroup_super equalityI)

text ‹For a surjective homomorphism, the derived series of the target is the image of
  the derived series of the source.›
lemma image_derivedSeries:
  assumes "η ` G = G'"
  shows "η ` source.derivedSeries n = target.derivedSeries n"
  by (induction n) (auto simp: assms image_commutator_subgroup_eq source.derivedSeries_subset)

text ‹A surjective homomorphic image of a solvable group is solvable.›
lemma solvable_image:
  assumes "η ` G = G'" and "source.solvable"
  shows "target.solvable"
  using assms unfolding source.solvable_def target.solvable_def
  by (metis commutes_with_unit image_derivedSeries image_empty image_insert)

text ‹Unconditionally (no surjectivity), the image of the source derived series is contained in the
  target derived series.›
lemma image_derivedSeries_subset: "η ` source.derivedSeries n ⊆ target.derivedSeries n"
proof (induction n)
  case 0
  show ?case using map_closed by auto
next
  case (Suc n) then show ?case
    by (simp add: image_commutator_subgroup_eq source.derivedSeries_subset
        target.commutator_subgroup_mono)
qed

text ‹∗‹A group admitting an injective homomorphism into a solvable group is solvable.›  If the target
  is solvable, its derived series reaches @{term "{𝟭'}"} at some step @{term n}; the image of the
  source derived series is contained there (@{thm [source] image_derivedSeries_subset}), so
  @{term η} maps @{term "source.derivedSeries n"} to @{term "𝟭'"}, and injectivity (with
  @{term "η 𝟭 = 𝟭'"}) forces it to be @{term "{𝟭}"}.›
lemma solvable_of_injective:
  assumes inj: "inj_on η G" and solv: "target.solvable"
  shows "source.solvable"
proof -
  from solv obtain n where n: "target.derivedSeries n = {𝟭'}"
    unfolding target.solvable_def by blast
  ― ‹Every element of @{term "source.derivedSeries n"} maps to @{term "𝟭'"}.›
  have mapsto: "η x = 𝟭'" if x: "x ∈ source.derivedSeries n" for x
    by (metis image_derivedSeries_subset image_subset_iff n singletonD x)
  have "source.derivedSeries n ⊆ {𝟭}"
    using inj source.unit_closed source.derivedSeries_subset
    using injective_iff_kernel_unit mapsto by blast
  with source.derivedSeries_unit_closed show ?thesis unfolding source.solvable_def by blast
qed

end (* group_homomorphism *)

text ‹A surjective homomorphic image of a solvable group is solvable (top level).›
theorem (in group_epimorphism) solvable_image_epi:
  assumes "source.solvable"
  shows "target.solvable"
  using solvable_image surjective assms by simp


subsection ‹Subgroups›

text ‹We work in the ambient @{locale Group} and refer to a subgroup's own group
  operations through the locale-qualified constants ‹Group.commutator_elt H (⋅) 𝟭›,
  ‹Group.generate H (⋅) 𝟭› and ‹Group.derivedSeries H (⋅) 𝟭›.  This
  bridge avoids the awkward parameter naming of the bare @{locale Subgroup} locale and
  is reusable for any subgroup.›

context Group
begin

text ‹The subgroup's derived series is contained in the ambient derived series.›
lemma derivedSeries_subgroup_subset:
  assumes H: "Subgroup H G (⋅) 𝟭"
  shows "Group.derivedSeries H (⋅) 𝟭 n ⊆ derivedSeries n"
proof -
  interpret S: Subgroup H G "(⋅)" 𝟭 by (rule H)
  show ?thesis
  proof (induction n)
    case 0
    show ?case using S.subset by simp
  next
    case (Suc n) 
    have "Group.derivedSeries H (⋅) 𝟭 (Suc n)
          ⊆ commutator_subgroup (S.sub.derivedSeries n) (S.sub.derivedSeries n)"
      using commutator_subgroup_subgroup_subset[OF H] S.sub.derivedSeries_subset by simp
    also have "… ⊆ derivedSeries (Suc n)" 
      using commutator_subgroup_mono[OF Suc.IH Suc.IH] by simp
    finally show ?case .
  qed
qed

text ‹A subgroup of a solvable group is solvable.›
theorem solvable_subgroup:
  assumes H: "Subgroup H G (⋅) 𝟭" and solv: solvable
  shows "Group.solvable H (⋅) 𝟭"
proof -
  interpret S: Subgroup H G "(⋅)" 𝟭 by (rule H)
  show ?thesis
    using solv H S.sub.derivedSeries_unit_closed derivedSeries_subgroup_subset
    unfolding S.sub.solvable_def solvable_def by blast
qed

text ‹∗‹Shift lemma.›  Once the derived series has entered a subgroup @{term H} (at step @{term k}),
  the later terms are dominated by @{term H}'s own derived series: @{term "derivedSeries (k + i)"}
  is contained in @{text "H⇗(i)⇖"}.  (Induction on @{term i}, using commutator monotonicity and that a
  commutator of subsets of @{term H} is computed inside @{term H}.)›
lemma derivedSeries_shift_subgroup:
  assumes H: "Subgroup H G (⋅) 𝟭" and k: "derivedSeries k ⊆ H"
  shows "derivedSeries (k + i) ⊆ Group.derivedSeries H (⋅) 𝟭 i"
proof -
  interpret S: Subgroup H G "(⋅)" 𝟭 by (rule H)
  show ?thesis
  proof (induction i)
    case 0
    show ?case using k by simp
  next
    case (Suc i) then 
    have "derivedSeries (k + Suc i) ⊆ commutator_subgroup (S.sub.derivedSeries i) (S.sub.derivedSeries i)"
      using commutator_subgroup_mono[OF Suc.IH Suc.IH] by simp
    also have "… ⊆ S.sub.derivedSeries (Suc i)"
      using commutator_subgroup_subset_subgroup[OF H] S.sub.derivedSeries_subset by simp
    finally show ?case .
  qed
qed

end (* Group *)


subsection ‹Solvability of an extension›

text ‹∗‹An extension of a solvable group by a solvable group is solvable.›  For a surjective
  homomorphism ‹η›: if the kernel and the image ‹G'› are both solvable, so is ‹G›.  The derived
  series of ‹G› maps onto that of ‹G'› (‹image_derivedSeries›), which reaches ‹{𝟭'}›; so
  ‹source.derivedSeries k ⊆ Ker›, and the kernel's own solvability then drives the remaining terms
  to ‹{𝟭}› via the shift lemma.›
theorem (in group_epimorphism) solvable_extension:
  assumes solvKer: "Group.solvable Ker (⋅) 𝟭"
    and solvImg: "target.solvable"
  shows "source.solvable"
proof -
  ― ‹The derived series of @{term G} maps onto that of the image, which vanishes at some step.›
  from solvImg obtain k where k: "target.derivedSeries k = {𝟭'}"
    unfolding target.solvable_def by blast
  ― ‹Everything in @{term "source.derivedSeries k"} maps to @{term "𝟭'"}, hence lies in the kernel.›
  have subKer: "source.derivedSeries k ⊆ Ker"
    using image_derivedSeries[OF surjective] k source.derivedSeries_subset by blast
  ― ‹The kernel is a subgroup; its solvability drives the shifted series to @{term "{𝟭}"}.›
  from solvKer obtain m where m: "Group.derivedSeries Ker (⋅) 𝟭 m = {𝟭}"
    using kernel.sub.solvable_def by auto
  have "source.derivedSeries (k + m) ⊆ Group.derivedSeries Ker (⋅) 𝟭 m"
    by (simp add: kernel.Subgroup_axioms source.derivedSeries_shift_subgroup subKer)
  then show ?thesis unfolding source.solvable_def
    using m source.derivedSeries_unit_closed by auto
qed

end