Theory Group_Product

section ‹The external direct product of two groups›

theory Group_Product
  imports Solvable_Transfer
begin

text ‹The external direct product of two groups: carrier the Cartesian product of the carriers, with
  componentwise operation and unit.  This is the group-theoretic prerequisite for combining two
  solvable Galois groups (the compositum of two splitting fields embeds into the product of their
  Galois groups); its headline consequence is that a ∗‹product of solvable groups is solvable›.›

locale group_product =
  G: Group G "(⋅)" 𝟭 + G': Group G' "(⋅')" "𝟭'"
  for G and composition (infixl ‹⋅› 70) and unit (‹𝟭›)
    and G' and composition' (infixl ‹⋅''› 70) and unit' (‹𝟭''›)
begin

definition pcarrier :: "('a × 'b) set" where "pcarrier = G × G'"

definition pcomp :: "'a × 'b ⇒ 'a × 'b ⇒ 'a × 'b" (infixl ‹⊗⇩×› 70)
  where "x ⊗⇩× y = (fst x ⋅ fst y, snd x ⋅' snd y)"

definition punit :: "'a × 'b" (‹𝟭⇩×›) where "𝟭⇩× = (𝟭, 𝟭')"

lemma pcomp_closed [intro, simp]:
  "x ∈ pcarrier ⟹ y ∈ pcarrier ⟹ x ⊗⇩× y ∈ pcarrier"
  by (auto simp: pcarrier_def pcomp_def)

lemma punit_closed [intro, simp]: "𝟭⇩× ∈ pcarrier"
  by (auto simp: pcarrier_def punit_def)

text ‹The direct product is a group.›
theorem Group_product: "Group pcarrier (⊗⇩×) 𝟭⇩×"
proof (rule GroupI)
  fix x y z assume "x ∈ pcarrier" "y ∈ pcarrier" "z ∈ pcarrier"
  then show "(x ⊗⇩× y) ⊗⇩× z = x ⊗⇩× (y ⊗⇩× z)"
    by (auto simp: pcarrier_def pcomp_def G.associative G'.associative)
next
  fix u assume u: "u ∈ pcarrier"
  then show "𝟭⇩× ⊗⇩× u = u" "u ⊗⇩× 𝟭⇩× = u"
    by (auto simp: pcarrier_def pcomp_def punit_def)
  have fu: "fst u ∈ G" and su: "snd u ∈ G'" 
    using u by (auto simp: pcarrier_def)
  obtain a where a: "a ∈ G" "fst u ⋅ a = 𝟭" "a ⋅ fst u = 𝟭"
    using G.invertible[OF fu] by (auto simp: G.invertible_def)
  obtain b where b: "b ∈ G'" "snd u ⋅' b = 𝟭'" "b ⋅' snd u = 𝟭'"
    using G'.invertible[OF su] by (auto simp: G'.invertible_def)
  show "∃v ∈ pcarrier. u ⊗⇩× v = 𝟭⇩× ∧ v ⊗⇩× u = 𝟭⇩×"
    using a b pcomp_def punit_def pcarrier_def by auto
qed auto

sublocale prod: Group pcarrier "(⊗⇩×)" "𝟭⇩×" 
  by (rule Group_product)

subsection ‹Projections are homomorphisms; the derived series is componentwise-bounded›

text ‹The (extensional) first and second projections are group homomorphisms onto @{term G} and
  @{term G'}.  We use @{term "restrict fst pcarrier"} so the maps are extensional, as the
  homomorphism locale requires; on @{term pcarrier} they agree with @{term fst} / @{term snd}.›
definition p1 :: "'a × 'b ⇒ 'a"
  where "p1 = restrict fst pcarrier"

definition p2 :: "'a × 'b ⇒ 'b" 
  where "p2 = restrict snd pcarrier"

lemma p1_eq: "x ∈ pcarrier ⟹ p1 x = fst x" 
  by (simp add: p1_def)

lemma p2_eq: "x ∈ pcarrier ⟹ p2 x = snd x" 
  by (simp add: p2_def)

lemma p1_hom: "group_homomorphism p1 pcarrier (⊗⇩×) 𝟭⇩× G (⋅) 𝟭"
proof 
  show "p1 ∈ pcarrier →⇩E G" 
    by (auto simp: p1_def pcarrier_def)
  show "⋀x y. x ∈ pcarrier ⟹ y ∈ pcarrier ⟹ p1 (x ⊗⇩× y) = p1 x ⋅ p1 y"
    using p1_eq pcomp_closed pcomp_def by auto
  show "p1 𝟭⇩× = 𝟭"
    using p1_eq punit_closed punit_def by auto
qed

lemma p2_hom: "group_homomorphism p2 pcarrier (⊗⇩×) 𝟭⇩× G' (⋅') 𝟭'"
proof 
  show "p2 ∈ pcarrier →⇩E G'" 
    by (auto simp: p2_def pcarrier_def)
  show "⋀x y. x ∈ pcarrier ⟹ y ∈ pcarrier ⟹ p2 (x ⊗⇩× y) = p2 x ⋅' p2 y"
    using p2_eq pcomp_closed pcomp_def by auto
  show "p2 𝟭⇩× = 𝟭'"
    using p2_eq punit_closed punit_def by auto
qed

text ‹An element of the product's derived series projects into each factor's derived series.›
lemma derivedSeries_p1: "p1 ` prod.derivedSeries n ⊆ G.derivedSeries n"
proof (induction n)
  case 0
  show ?case
    by (meson group_homomorphism.image_derivedSeries_subset p1_hom)
next
  case (Suc n)
  interpret F: group_homomorphism p1 pcarrier "(⊗⇩×)" "𝟭⇩×" G "(⋅)" 𝟭 by (rule p1_hom)
  have "p1 ` prod.derivedSeries (Suc n)
          ⊆ G.commutator_subgroup (p1 ` prod.derivedSeries n) (p1 ` prod.derivedSeries n)"
    using F.image_commutator_subgroup_sub[OF prod.derivedSeries_subset prod.derivedSeries_subset]
    by simp
  also have "… ⊆ G.commutator_subgroup (G.derivedSeries n) (G.derivedSeries n)"
    using G.commutator_subgroup_mono[OF Suc.IH Suc.IH] .
  also have "… = G.derivedSeries (Suc n)" by simp
  finally show ?case .
qed

lemma derivedSeries_p2: "p2 ` prod.derivedSeries n ⊆ G'.derivedSeries n"
proof (induction n)
  case 0 show ?case
    by (meson group_homomorphism.image_derivedSeries_subset p2_hom)
next
  case (Suc n)
  interpret S: group_homomorphism p2 pcarrier "(⊗⇩×)" "𝟭⇩×" G' "(⋅')" "𝟭'" by (rule p2_hom)
  have "p2 ` prod.derivedSeries (Suc n)
          ⊆ G'.commutator_subgroup (p2 ` prod.derivedSeries n) (p2 ` prod.derivedSeries n)"
    using S.image_commutator_subgroup_sub[OF prod.derivedSeries_subset prod.derivedSeries_subset] by simp
  also have "… ⊆ G'.commutator_subgroup (G'.derivedSeries n) (G'.derivedSeries n)"
    using G'.commutator_subgroup_mono[OF Suc.IH Suc.IH] .
  also have "… = G'.derivedSeries (Suc n)" by simp
  finally show ?case .
qed

subsection ‹Product of solvable groups is solvable›

text ‹∗‹The direct product of two solvable groups is solvable.›  If both factors' derived series reach
  the trivial subgroup (at steps @{term m}, @{term k}), then at step @{term "max m k"} the product's
  derived series projects to @{term "{𝟭}"} in each factor (the derived series is monotone decreasing),
  hence consists of the single element @{term "𝟭⇩×"}.›
theorem solvable_product:
  assumes solvG: "G.solvable" and solvG': "G'.solvable"
  shows "prod.solvable"
proof -
  obtain m where m: "G.derivedSeries m = {𝟭}" using solvG unfolding G.solvable_def by blast
  obtain k where k: "G'.derivedSeries k = {𝟭'}" using solvG' unfolding G'.solvable_def by blast
  define N where "N = max m k"
  have dGN: "G.derivedSeries N = {𝟭}"
    using m G.derivedSeries_antimono[of m N] G.derivedSeries_unit_closed by (auto simp: N_def)
  have dG'N: "G'.derivedSeries N = {𝟭'}"
    using k G'.derivedSeries_antimono[of k N] G'.derivedSeries_unit_closed by (auto simp: N_def)
  ― ‹At step @{term N} the product's derived series projects to a point in each factor.›
  have "prod.derivedSeries N ⊆ {𝟭⇩×}"
  proof
    fix x assume x: "x ∈ prod.derivedSeries N"
    have xp: "x ∈ pcarrier" using x prod.derivedSeries_subset by blast
    then have "p1 x = 𝟭" "p2 x = 𝟭'" using derivedSeries_p1 dGN derivedSeries_p2 dG'N
      using x by blast+
    then show "x ∈ {𝟭⇩×}"
      using p1_eq p2_eq punit_def xp by auto
  qed
  moreover have "𝟭⇩× ∈ prod.derivedSeries N" by (rule prod.derivedSeries_unit_closed)
  ultimately have "prod.derivedSeries N = {𝟭⇩×}" by auto
  then show ?thesis unfolding prod.solvable_def by blast
qed

end

end