Theory Commutator

section ‹Commutators and the Derived Subgroup›

theory Commutator
  imports Sylow_Theorems
begin

text ‹
  The commutator of two elements, the commutator subgroup of two subsets, and the
  derived (commutator) subgroup of a group.  These underlie the derived series and
  the notion of a solvable group.  (Custom notation is deferred; we use plain
  constant names while developing the theory.)
›

context Group
begin

text ‹The commutator of two elements.›
definition commutator_elt :: "'a ⇒ 'a ⇒ 'a"
  where "commutator_elt a b = a ⋅ b ⋅ inverse a ⋅ inverse b"

text ‹Membership rule for commutators.  Declared @{attribute simp} only: as an
  @{attribute intro} rule it back-chains on ∗‹every› carrier-membership goal
  (‹?x ∈ G› via ‹?x = commutator_elt ?a ?b›), which interacts badly with large
  introduction-rule sets and can loop.›
lemma commutator_elt_closed [simp]:
  "⟦ a ∈ G; b ∈ G ⟧ ⟹ commutator_elt a b ∈ G"
  unfolding commutator_elt_def by simp

text ‹The commutator subgroup of two subsets of the carrier.›
definition commutator_subgroup :: "'a set ⇒ 'a set ⇒ 'a set"
  where "commutator_subgroup H K = ⟨{ commutator_elt h k | h k. h ∈ H ∧ k ∈ K }⟩"

text ‹The derived subgroup of the whole group.›
definition derived :: "'a set"
  where "derived = commutator_subgroup G G"

lemma commutator_subgroup_is_subgroup:
  "Subgroup (commutator_subgroup H K) G (⋅) 𝟭"
  unfolding commutator_subgroup_def by (rule Gen_is_subgroup)

lemma commutator_subgroup_subset:
  "commutator_subgroup H K ⊆ G"
  unfolding commutator_subgroup_def by (rule Gen_subset_carrier)

lemma derived_is_subgroup: "Subgroup derived G (⋅) 𝟭"
  unfolding derived_def by (rule commutator_subgroup_is_subgroup)

lemma derived_subset: "derived ⊆ G"
  unfolding derived_def by (rule commutator_subgroup_subset)

text ‹Generators of the commutator subgroup are commutators.›
lemma commutator_gen_mem:
  "⟦ h ∈ H; k ∈ K; H ⊆ G; K ⊆ G ⟧ ⟹ commutator_elt h k ∈ commutator_subgroup H K"
    unfolding commutator_subgroup_def using Gen_incl by force

text ‹Conjugation distributes over a commutator.›
lemma conjugation_commutator:
  assumes "g ∈ G" "a ∈ G" "b ∈ G"
  shows "conjugation g (commutator_elt a b) = commutator_elt (conjugation g a) (conjugation g b)"
  using assms by (simp add: conjugation_hom commutator_elt_def flip: conjugation_inverse)

text ‹The derived subgroup is normal.›
lemma derived_normal: "normal_subgroup derived G (⋅) 𝟭"
proof -
  interpret D: Subgroup derived G "(⋅)" 𝟭 by (rule derived_is_subgroup)
  interpret DG: subgroup_of_group derived G "(⋅)" 𝟭
    by (simp add: D.Subgroup_axioms Group_axioms subgroup_of_group_def)
  show ?thesis
  proof
    fix g k assume g: "g ∈ G" and k: "k ∈ derived"
    have ig: "inverse g ∈ G" using g by simp
    have conj_in: "conjugation (inverse g) x ∈ derived"
      if "x ∈ generate ({ commutator_elt a b | a b. a ∈ G ∧ b ∈ G } ∩ G)" for x
      using that
    proof induction
      case unit then show ?case
        using conjugation_def by auto
    next
      case (incl x) 
      then obtain a b where xab: "x = commutator_elt a b" and ab: "a ∈ G" "b ∈ G" by auto
      have "conjugation (inverse g) x =
              commutator_elt (conjugation (inverse g) a) (conjugation (inverse g) b)"
        using ig ab xab by (simp add: conjugation_commutator)
      moreover have "conjugation (inverse g) a ∈ G" "conjugation (inverse g) b ∈ G"
        using ig ab by (auto simp: conjugation_closed)
      ultimately show ?case
        by (metis commutator_gen_mem derived_def set_eq_subset)
    next
      case (comp x y)
      have xy: "x ∈ G" "y ∈ G" using comp.hyps generate_subset_carrier by auto
      with conjugation_hom[OF xy] comp.IH D.sub_composition_closed
      show ?case by metis
    next
      case (inv x)
      have xG: "x ∈ G" using inv.hyps generate_subset_carrier by auto
      have "conjugation (inverse g) (inverse x) = inverse (conjugation (inverse g) x)"
        using conjugation_inverse[OF xG] .
      then show ?case using inv.IH D.submonoid_inverse_closed D.sub.invertible by simp
    qed
    have "inverse g ⋅ k ⋅ g = conjugation (inverse g) k"
      using g k derived_subset
      by (auto simp: conjugation_def associative invertible_inverse_inverse subsetD)
    moreover have "k ∈ generate ({ commutator_elt a b | a b. a ∈ G ∧ b ∈ G } ∩ G)"
      using k unfolding derived_def commutator_subgroup_def Gen_def .
    ultimately show "inverse g ⋅ k ⋅ g ∈ derived"
      using conj_in by simp
  qed
qed

text ‹The commutator subgroup is monotone in both arguments.›
lemma commutator_subgroup_mono:
  assumes "A ⊆ A'" "B ⊆ B'"
  shows "commutator_subgroup A B ⊆ commutator_subgroup A' B'"
  unfolding commutator_subgroup_def Gen_def
  using assms by (intro generate_mono) blast

text ‹A commutator computed inside a subgroup (with the restricted operation) equals the
  ambient commutator.  A locality property of @{const commutator_elt}.›
lemma commutator_elt_subgroup_eq:
  assumes H: "Subgroup H G (⋅) 𝟭" and ab: "a ∈ H" "b ∈ H"
  shows "Group.commutator_elt H (⋅) 𝟭 a b = commutator_elt a b"
proof -
  interpret S: Subgroup H G "(⋅)" 𝟭 by (rule H)
  show ?thesis
    by (simp add: assms S.sub.commutator_elt_def commutator_elt_def)
  also have "… = commutator_elt a b" by (simp add: commutator_elt_def)
qed

text ‹The commutator subgroup computed inside a subgroup is contained in the ambient one.›
lemma commutator_subgroup_subgroup_subset:
  assumes H: "Subgroup H G (⋅) 𝟭" and AB: "A ⊆ H" "B ⊆ H"
  shows "Group.commutator_subgroup H (⋅) 𝟭 A B ⊆ commutator_subgroup A B"
proof -
  interpret S: Subgroup H G "(⋅)" 𝟭 by (rule H)
  have AG: "A ⊆ G" "B ⊆ G" using AB S.subset by auto
  have genset: "({ Group.commutator_elt H (⋅) 𝟭 h k | h k. h ∈ A ∧ k ∈ B } ∩ H)
                  ⊆ { commutator_elt h k | h k. h ∈ A ∧ k ∈ B }"
    using assms commutator_elt_subgroup_eq by blast
  have absorb: "{ commutator_elt h k | h k. h ∈ A ∧ k ∈ B } ∩ G
                  = { commutator_elt h k | h k. h ∈ A ∧ k ∈ B }"
    using AG by (force simp: commutator_elt_closed)
  have "Group.commutator_subgroup H (⋅) 𝟭 A B
          = Group.generate H (⋅) 𝟭 ({ Group.commutator_elt H (⋅) 𝟭 h k | h k. h ∈ A ∧ k ∈ B } ∩ H)"
    by (simp add: S.sub.commutator_subgroup_def S.sub.Gen_def)
  also have "… ⊆ generate ({ Group.commutator_elt H (⋅) 𝟭 h k | h k. h ∈ A ∧ k ∈ B } ∩ H)"
    by (rule generate_subgroup_subset[OF H])
  also have "… ⊆ generate { commutator_elt h k | h k. h ∈ A ∧ k ∈ B }"
    using genset by (rule generate_mono)
  also have "… = commutator_subgroup A B"
    by (simp add: commutator_subgroup_def Gen_def absorb)
  finally show ?thesis .
qed

text ‹Generation is ∗‹absolute› for a subgroup: for @{term "S ⊆ H"}, the subgroup generated by
  @{term S} inside @{term G} coincides with the one generated inside @{term H} (the reverse
  inclusion to @{thm [source] generate_subgroup_subset}).  The @{term H}-generated set is a
  subgroup of @{term G} containing @{term S}, so the minimal such (@{const generate}) is contained
  in it.›
lemma generate_subgroup_superset:
  assumes H: "Subgroup H G (⋅) 𝟭" and S: "S ⊆ H"
  shows "generate S ⊆ Group.generate H (⋅) 𝟭 S"
proof (rule generate_minimal)
  interpret S': Subgroup H G "(⋅)" 𝟭 by (rule H)
  have "Subgroup (Group.generate H (⋅) 𝟭 S) H (⋅) 𝟭" by (rule S'.sub.generate_is_subgroup)
  then show "Subgroup (Group.generate H (⋅) 𝟭 S) G (⋅) 𝟭"
    using H by (rule subgroup_transitive)
  have "S ⊆ Group.generate H (⋅) 𝟭 S" using S S'.sub.generate_incl by auto
  then show "S ∩ G ⊆ Group.generate H (⋅) 𝟭 S" by blast
qed

text ‹The commutator subgroup of subsets of @{term H} computed in @{term G} is contained in the one
  computed in @{term H} (the reverse of @{thm [source] commutator_subgroup_subgroup_subset}; the two
  are in fact equal).›
lemma commutator_subgroup_subset_subgroup:
  assumes H: "Subgroup H G (⋅) 𝟭" and AB: "A ⊆ H" "B ⊆ H"
  shows "commutator_subgroup A B ⊆ Group.commutator_subgroup H (⋅) 𝟭 A B"
proof -
  interpret S: Subgroup H G "(⋅)" 𝟭 by (rule H)
  have AG: "A ⊆ G" "B ⊆ G" using AB S.subset by auto
  ― ‹The commutator generators computed in @{term H} coincide with the ambient ones and lie in @{term H}.›
  have absorb: "{ commutator_elt h k | h k. h ∈ A ∧ k ∈ B } ∩ G
                = { commutator_elt h k | h k. h ∈ A ∧ k ∈ B }"
    using AG by (force simp: commutator_elt_closed)
  have "commutator_subgroup A B = generate ({ commutator_elt h k | h k. h ∈ A ∧ k ∈ B })"
    by (simp add: commutator_subgroup_def Gen_def absorb)
  also have "… ⊆ generate ({ Group.commutator_elt H (⋅) 𝟭 h k | h k. h ∈ A ∧ k ∈ B } ∩ H)"
    using assms by (intro generate_mono) (force simp: commutator_elt_def S.sub.commutator_elt_def)
  also have "… ⊆ Group.generate H (⋅) 𝟭 ({ Group.commutator_elt H (⋅) 𝟭 h k | h k. h ∈ A ∧ k ∈ B } ∩ H)"
    by (rule generate_subgroup_superset[OF H]) auto
  also have "… = Group.commutator_subgroup H (⋅) 𝟭 A B"
    by (simp add: S.sub.commutator_subgroup_def S.sub.Gen_def)
  finally show ?thesis .
qed

subsection ‹The Derived Series and Solvable Groups›

text ‹
  The derived series of a group is obtained by iterating the derived-subgroup
  construction.  A group is solvable when its derived series reaches the trivial
  subgroup.  As a first milestone we show that every abelian group is solvable.
›

text ‹The derived series, as a sequence of subsets of the carrier.›
primrec derivedSeries :: "nat ⇒ 'a set"
  where
    "derivedSeries 0 = G"
  | "derivedSeries (Suc n) = commutator_subgroup (derivedSeries n) (derivedSeries n)"

text ‹A group is solvable if its derived series reaches the trivial subgroup.›
definition solvable :: bool
  where "solvable ≡ (∃n. derivedSeries n = {𝟭})"

text ‹Each term of the derived series is a subgroup.›
lemma derivedSeries_subgroup: "Subgroup (derivedSeries n) G (⋅) 𝟭"
  by (cases n) (auto simp: commutator_subgroup_is_subgroup group_self_subgroup)

lemma derivedSeries_subset: "derivedSeries n ⊆ G" and derivedSeries_unit_closed: "𝟭 ∈ derivedSeries n"
proof -
  interpret S: Subgroup "derivedSeries n" G "(⋅)" 𝟭 by (rule derivedSeries_subgroup)
  show "derivedSeries n ⊆ G" by (rule S.subset)
  show "𝟭 ∈ derivedSeries n" by (rule S.sub_unit_closed)
qed

text ‹The commutator subgroup of a subgroup @{term H} (with itself) is contained in @{term H}: the
  commutator generators lie in @{term H} (closed under the operation and inverse), and @{term H}, being
  a subgroup, contains the subgroup they generate.›
lemma commutator_subgroup_self_subset:
  assumes H: "Subgroup H G (⋅) 𝟭"
  shows "commutator_subgroup H H ⊆ H"
proof -
  interpret S: Subgroup H G "(⋅)" 𝟭 by (rule H)
  show ?thesis
    using S.sub.commutator_subgroup_subset assms commutator_subgroup_subset_subgroup
    by blast
qed

text ‹The derived series is decreasing: @{term "derivedSeries (Suc n) ⊆ derivedSeries n"}.›
lemma derivedSeries_Suc_subset: "derivedSeries (Suc n) ⊆ derivedSeries n"
  using commutator_subgroup_self_subset[OF derivedSeries_subgroup] by simp

lemma derivedSeries_antimono: "m ≤ n ⟹ derivedSeries n ⊆ derivedSeries m"
  by (induction n) (use derivedSeries_Suc_subset not_less_eq_eq in fastforce)+

text ‹In an abelian group every commutator is the unit.›
lemma commutator_elt_abelian:
  assumes "commutative_monoid G (⋅) 𝟭" and "a ∈ G" "b ∈ G"
  shows "commutator_elt a b = 𝟭"
proof -
  interpret comm: commutative_monoid G "(⋅)" 𝟭 by (rule assms(1))
  show ?thesis
    using assms(2,3) comm.commutative commutator_elt_def commute_iff_inverse by auto
qed

text ‹In an abelian group the derived subgroup is trivial.›
lemma derived_trivial_if_abelian:
  assumes "commutative_monoid G (⋅) 𝟭"
  shows "derived = {𝟭}"
proof -
  interpret D: Subgroup derived G "(⋅)" 𝟭 by (rule derived_is_subgroup)
  have "derived ⊆ {𝟭}"
    unfolding derived_def commutator_subgroup_def
    using commutator_elt_abelian[OF assms]  
    by (intro Gen_minimal[OF trivial_subgroup]) auto
  then show ?thesis using D.sub_unit_closed by auto
qed

text ‹Milestone: every abelian group is solvable.›
theorem abelian_imp_solvable:
  assumes "commutative_monoid G (⋅) 𝟭"
  shows solvable
  unfolding solvable_def
  by (metis assms derivedSeries.simps derived_def derived_trivial_if_abelian)

end (* Group *)

end