Theory Zassenhaus_Lemma

(*
  The Zassenhaus (butterfly) lemma, developed directly over New-Algebra's
  set-based group and quotient infrastructure.
*)

theory Zassenhaus_Lemma
  imports Group_Theory
begin

section ‹The Zassenhaus Lemma›

text ‹
  Suppose that @{term H1} is normal in @{term H}, and @{term K1} is normal in
  @{term K}.  The two wings of the butterfly are obtained by multiplying each
  normal subgroup by @{term "H ∩ K"}; their denominators use the smaller
  intersections @{term "H ∩ K1"} and @{term "K ∩ H1"}.

  A locale records this symmetric configuration once.  In particular, no
  ambient record updates or HOL-Algebra structures occur in the statement.
›
locale zassenhaus =
  G: Group G "(⋅)" 𝟭 +
  H: subgroup_of_group H G "(⋅)" 𝟭 +
  K: subgroup_of_group K G "(⋅)" 𝟭 +
  H1: normal_subgroup H1 H "(⋅)" 𝟭 +
  K1: normal_subgroup K1 K "(⋅)" 𝟭
  for G H K H1 K1 and composition (infixl ‹⋅› 70) and unit (‹𝟭›)
begin

interpretation HK_sub: Subgroup "H ∩ K" G "(⋅)" 𝟭
  by (simp add: G.subgroup_intersection H.Subgroup_axioms K.Subgroup_axioms)

interpretation HK1_subG: Subgroup "H ∩ K1" G "(⋅)" 𝟭
  using G.subgroup_intersection H.Subgroup_axioms K.Subgroup_axioms K1.Subgroup_axioms 
  by (meson subgroup_transitive)

interpretation HK1_sub: Subgroup "H ∩ K1" H "(⋅)" 𝟭
  using H.Subgroup_axioms HK1_subG.Subgroup_axioms subgroup_restrict by fastforce

interpretation KH1_sub: Subgroup "K ∩ H1" K "(⋅)" 𝟭
proof -
  have "Subgroup (K ∩ H1) G (⋅) 𝟭"
    using G.subgroup_intersection H.Subgroup_axioms H1.Subgroup_axioms K.Subgroup_axioms
    by (meson subgroup_transitive)
  then show "Subgroup (K ∩ H1) K (⋅) 𝟭"
    using K.Subgroup_axioms subgroup_restrict by force
qed

interpretation HK1_normal: normal_subgroup "H ∩ K1" "H ∩ K" "(⋅)" 𝟭
proof -
  have I_sub: "Subgroup (H ∩ K) K (⋅) 𝟭"
    using HK_sub.Subgroup_axioms K.Subgroup_axioms subgroup_restrict by fastforce
  have "Subgroup ((H ∩ K) ∩ K1) K (⋅) 𝟭"
    by (rule K.sub.subgroup_intersection[OF I_sub K1.Subgroup_axioms])
  then have C_K: "Subgroup (H ∩ K1) K (⋅) 𝟭"
    using K1.subset by (smt (cvc5, best) dual_order.refl inf.bounded_iff subset_antisym)
  have C_sub: "Subgroup (H ∩ K1) (H ∩ K) (⋅) 𝟭"
    using C_K I_sub subgroup_restrict by fastforce
  interpret C: Subgroup "H ∩ K1" "H ∩ K" "(⋅)" 𝟭 by fact
  interpret I: Subgroup "H ∩ K" K "(⋅)" 𝟭 by fact
  have I_H_sub: "Subgroup (H ∩ K) H (⋅) 𝟭"
    using H.Subgroup_axioms HK_sub.Subgroup_axioms by (meson inf_sup_ord(1) subgroup_restrict)
  interpret I_H: Subgroup "H ∩ K" H "(⋅)" 𝟭 by fact
  show "normal_subgroup (H ∩ K1) (H ∩ K) (⋅) 𝟭"
  proof
    fix g c
    assume g: "g ∈ H ∩ K" and c: "c ∈ H ∩ K1"
    obtain inv_K: "Monoid.inverse (H ∩ K) (⋅) 𝟭 g = K.sub.inverse g"
       and inv_H: "Monoid.inverse (H ∩ K) (⋅) 𝟭 g = H.sub.inverse g"
      using I_H_sub I_sub g by (metis Subgroup.subgroup_inverse_equality)
    have g_H: "g ∈ H" and c_H: "c ∈ H" and g_K: "g ∈ K" and c_K1: "c ∈ K1"
      using g c by blast+
    have in_H: "H.sub.inverse g ⋅ c ⋅ g ∈ H"
      using Monoid.invertible_inverse_closed c_H g_H by blast
    have in_K1: "K.sub.inverse g ⋅ c ⋅ g ∈ K1"
      by (rule K1.normal[OF g_K c_K1])
    show "Monoid.inverse (H ∩ K) (⋅) 𝟭 g ⋅ c ⋅ g ∈ H ∩ K1"
      using in_H in_K1 inv_H inv_K by (metis IntI)
  qed
qed

interpretation KH1_normal: normal_subgroup "K ∩ H1" "H ∩ K" "(⋅)" 𝟭
proof -
  have I_sub: "Subgroup (H ∩ K) H (⋅) 𝟭"
    using H.Subgroup_axioms HK_sub.Subgroup_axioms subgroup_restrict by force
  have "Subgroup ((H ∩ K) ∩ H1) H (⋅) 𝟭"
    by (simp add: H.sub.subgroup_intersection H1.Subgroup_axioms I_sub)
  then have C_H: "Subgroup (K ∩ H1) H (⋅) 𝟭"
    using H1.subset by (smt (cvc5, best) dual_order.refl inf.bounded_iff subset_antisym)
  have C_sub: "Subgroup (K ∩ H1) (H ∩ K) (⋅) 𝟭"
    using C_H I_sub subgroup_restrict by fastforce
  interpret C: Subgroup "K ∩ H1" "H ∩ K" "(⋅)" 𝟭 by fact
  interpret I: Subgroup "H ∩ K" H "(⋅)" 𝟭 by fact
  have I_K_sub: "Subgroup (H ∩ K) K (⋅) 𝟭"
    using HK_sub.Subgroup_axioms K.Subgroup_axioms subgroup_restrict by fastforce
  interpret I_K: Subgroup "H ∩ K" K "(⋅)" 𝟭 by fact
  show "normal_subgroup (K ∩ H1) (H ∩ K) (⋅) 𝟭"
  proof
    fix g c
    assume g: "g ∈ H ∩ K" and c: "c ∈ K ∩ H1"
    have inv_H: "Monoid.inverse (H ∩ K) (⋅) 𝟭 g = H.sub.inverse g"
      using I.subgroup_inverse_equality g by presburger
    have inv_K: "Monoid.inverse (H ∩ K) (⋅) 𝟭 g = K.sub.inverse g"
      using I_K.subgroup_inverse_equality g by presburger
    have g_K: "g ∈ K" and c_K: "c ∈ K" and g_H: "g ∈ H" and c_H1: "c ∈ H1" and in_K: "K.sub.inverse g ⋅ c ⋅ g ∈ K"
      using g c by blast+
    have in_H1: "H.sub.inverse g ⋅ c ⋅ g ∈ H1"
      by (rule H1.normal[OF g_H c_H1])
    show "Monoid.inverse (H ∩ K) (⋅) 𝟭 g ⋅ c ⋅ g ∈ K ∩ H1"
      using in_H1 in_K inv_H inv_K by (metis IntI)
  qed
qed

interpretation middle_H: Subgroup "H ∩ K" H "(⋅)" 𝟭
  using H.Subgroup_axioms HK_sub.Subgroup_axioms subgroup_restrict by force

interpretation middle_K: Subgroup "H ∩ K" K "(⋅)" 𝟭
  using HK_sub.Subgroup_axioms K.Subgroup_axioms subgroup_restrict by force

interpretation middle_H_group: subgroup_of_group "H ∩ K" H "(⋅)" 𝟭
  by (simp add: H.sub.Group_axioms middle_H.Subgroup_axioms subgroup_of_group_def)

interpretation middle_K_group: subgroup_of_group "H ∩ K" K "(⋅)" 𝟭
  by (simp add: K.sub.Group_axioms middle_K.Subgroup_axioms subgroup_of_group_def)

interpretation HK1_group: subgroup_of_group "H ∩ K1" H "(⋅)" 𝟭
  by (simp add: H.sub.Group_axioms HK1_sub.Subgroup_axioms subgroup_of_groupI)

interpretation KH1_group: subgroup_of_group "K ∩ H1" K "(⋅)" 𝟭
  by (simp add: K.sub.Group_axioms KH1_sub.Subgroup_axioms subgroup_of_group_def)

text ‹The four subgroup products making up the two wings.›
definition left_top where
  "left_top ≡ (case_prod (⋅)) ` ((H ∩ K) × H1)"

definition left_bottom where
  "left_bottom ≡ (case_prod (⋅)) ` ((H ∩ K1) × H1)"

definition right_top where
  "right_top ≡ (case_prod (⋅)) ` ((H ∩ K) × K1)"

definition right_bottom where
  "right_bottom ≡ (case_prod (⋅)) ` ((K ∩ H1) × K1)"

interpretation left_top_product: normal_subgroup_product H1 "H ∩ K" H "(⋅)" 𝟭 ..

interpretation left_bottom_product: normal_subgroup_product H1 "H ∩ K1" H "(⋅)" 𝟭 ..

interpretation right_top_product: normal_subgroup_product K1 "H ∩ K" K "(⋅)" 𝟭 ..

interpretation right_bottom_product: normal_subgroup_product K1 "K ∩ H1" K "(⋅)" 𝟭 ..

lemma left_top_eq [simp]: "left_top = left_top_product.HK"
  by (simp add: left_top_def left_top_product.HK_def)

lemma left_bottom_eq [simp]: "left_bottom = left_bottom_product.HK"
  by (simp add: left_bottom_def left_bottom_product.HK_def)

lemma right_top_eq [simp]: "right_top = right_top_product.HK"
  by (simp add: right_top_def right_top_product.HK_def)

lemma right_bottom_eq [simp]: "right_bottom = right_bottom_product.HK"
  by (simp add: right_bottom_def right_bottom_product.HK_def)

lemma left_top_subgroup: "Subgroup left_top H (⋅) 𝟭"
  by (simp add: left_top_product.HK_subgroup)

lemma left_bottom_subgroup: "Subgroup left_bottom H (⋅) 𝟭"
  by (simp add: left_bottom_product.HK_subgroup)

lemma right_top_subgroup: "Subgroup right_top K (⋅) 𝟭"
  by (simp add: right_top_product.HK_subgroup)

lemma right_bottom_subgroup: "Subgroup right_bottom K (⋅) 𝟭"
  by (simp add: right_bottom_product.HK_subgroup)

lemma left_bottom_subset_top: "left_bottom ⊆ left_top"
  unfolding left_bottom_def left_top_def
  by blast

lemma right_bottom_subset_top: "right_bottom ⊆ right_top"
  unfolding right_bottom_def right_top_def
  by blast

lemma left_top_memE:
  assumes "x ∈ left_top"
  obtains b n where "b ∈ H ∩ K" "n ∈ H1" "x = b ⋅ n"
  using assms left_top_eq left_top_product.HK_memE by metis

lemma left_bottom_memI:
  "⟦c ∈ H ∩ K1; n ∈ H1⟧ ⟹ c ⋅ n ∈ left_bottom"
  unfolding left_bottom_eq by (rule left_bottom_product.HK_memI)

lemma left_bottom_memE:
  assumes "x ∈ left_bottom"
  obtains c n where "c ∈ H ∩ K1" "n ∈ H1" "x = c ⋅ n"
  using assms left_bottom_eq left_bottom_product.HK_memE by blast

text ‹The lower subgroup in the left wing is normal in the upper one.›
lemma left_bottom_normal: "normal_subgroup left_bottom left_top (⋅) 𝟭"
proof -
  have bottom_top: "Subgroup left_bottom left_top (⋅) 𝟭"
    by (rule subgroup_restrict[OF left_bottom_subgroup left_top_subgroup left_bottom_subset_top])
  interpret bottom: Subgroup left_bottom left_top "(⋅)" 𝟭 by fact
  interpret top_H: Subgroup left_top H "(⋅)" 𝟭 by (rule left_top_subgroup)
  show ?thesis
  proof
    fix x y
    assume x: "x ∈ left_top" and y: "y ∈ left_bottom"
    obtain b n where b_middle: "b ∈ H ∩ K" and n: "n ∈ H1" and x_eq: "x = b ⋅ n"
      using x by (rule left_top_memE)
    obtain c m where c: "c ∈ H ∩ K1" and m: "m ∈ H1" and y_eq: "y = c ⋅ m"
      using y by (rule left_bottom_memE)
    have bH: "b ∈ H" and cH: "c ∈ H" and nH: "n ∈ H" and mH: "m ∈ H"
      using b_middle c n m H1.sub by blast+
    have inv_middle: "H.sub.inverse b = Monoid.inverse (H ∩ K) (⋅) 𝟭 b"
      using b_middle middle_H.subgroup_inverse_equality by blast
    have conjugate_c: "H.sub.inverse b ⋅ c ⋅ b ∈ H ∩ K1"
      using HK1_normal.normal b_middle c inv_middle by presburger
    have conjugate_y: "H.sub.inverse b ⋅ y ⋅ b ∈ left_bottom"
      using H1.normal[OF bH m] H.sub.conjugate_composition H.sub.invertible bH cH conjugate_c 
            left_bottom_memI mH y_eq   by presburger
    have inv_n: "H.sub.inverse n ∈ H1"
      by (rule H1.submonoid_inverse_closed[OF H1.sub.invertible[OF n] n])
    have inv_n_bottom: "H.sub.inverse n ∈ left_bottom"
      using inv_n left_bottom_eq left_bottom_product.K_subset_HK by blast
    have n_bottom: "n ∈ left_bottom"
      using left_bottom_product.K_subset_HK n by auto
    have inv_x: "H.sub.inverse x = H.sub.inverse n ⋅ H.sub.inverse b"
      unfolding x_eq using H.sub.inverse_composition_commute bH nH by blast
    obtain inv_b_H: "H.sub.inverse b ∈ H" and inv_n_H: "H.sub.inverse n ∈ H"
      using H.sub.invertible_inverse_closed H1.sub bH inv_n by blast
    have y_top: "y ∈ left_top" using bottom.subset y by blast
    have yH: "y ∈ H" using top_H.subset y_top by blast
    have conjugate_expansion: "H.sub.inverse x ⋅ y ⋅ x = H.sub.inverse n ⋅ (H.sub.inverse b ⋅ y ⋅ b) ⋅ n"
      using H.sub.associative H.sub_composition_closed bH inv_b_H inv_n_H inv_x nH x_eq yH
      by metis
    then have "H.sub.inverse x ⋅ y ⋅ x ∈ left_bottom"
      using bottom.sub_composition_closed conjugate_y inv_n_bottom n_bottom by presburger
    then show "Monoid.inverse left_top (⋅) 𝟭 x ⋅ y ⋅ x ∈ left_bottom"
      using top_H.subgroup_inverse_equality x by metis
  qed
qed

text ‹
  The following two identities are the algebraic centre of the butterfly.  An
  element of the middle intersection that is written as a product in one wing
  forces its normal-subgroup factor into the opposite subgroup.
›
lemma middle_inter_left_bottom:
  "(H ∩ K) ∩ left_bottom =
   (case_prod (⋅)) ` ((H ∩ K1) × (K ∩ H1))"
proof (intro equalityI subsetI)
  fix x
  assume x: "x ∈ (H ∩ K) ∩ left_bottom"
  then obtain p where p_in: "p ∈ (H ∩ K1) × H1" and p_eq: "x = case_prod (⋅) p"
    unfolding left_bottom_def by blast
  obtain c h where p: "p = (c,h)" by (cases p)
  have c: "c ∈ H ∩ K1" and h: "h ∈ H1"
    using p_in unfolding p by blast+
  have x_eq: "x = c ⋅ h" using p_eq by (simp only: p prod.case)
  have cK: "c ∈ K" using c K1.sub by blast
  have xK: "x ∈ K" using x by blast
  have cG: "c ∈ G" and hG: "h ∈ G"
    using c h H.sub H1.sub by blast+
  then have "G.inverse c ⋅ x = h"
    using G.invertible_left_inverse2 x_eq by blast
  moreover have inv_c_x_K: "G.inverse c ⋅ x ∈ K"
    using cK xK by blast
  ultimately have hK: "h ∈ K" by meson
  show "x ∈ (case_prod (⋅)) ` ((H ∩ K1) × (K ∩ H1))"
    using c h hK x_eq by blast
next
  fix x
  assume "x ∈ (case_prod (⋅)) ` ((H ∩ K1) × (K ∩ H1))"
  then obtain p c h where p_in: "p ∈ (H ∩ K1) × (K ∩ H1)"
    and p_eq: "x = case_prod (⋅) p" and p: "p = (c,h)"  by blast
  have c: "c ∈ H ∩ K1" and h: "h ∈ K ∩ H1"
    using p_in unfolding p by blast+
  have x_eq: "x = c ⋅ h" using p_eq by (simp only: p prod.case)
  have "x ∈ H ∩ K"
    unfolding x_eq using c h by blast
  moreover have "x ∈ left_bottom"
    unfolding left_bottom_def using c h x_eq by blast
  ultimately show "x ∈ (H ∩ K) ∩ left_bottom" by blast
qed

interpretation symmetric: zassenhaus G K H K1 H1 "(⋅)" 𝟭 ..

lemma middle_inter_right_bottom:
  "(H ∩ K) ∩ right_bottom = (case_prod (⋅)) ` ((K ∩ H1) × (H ∩ K1))"
  using right_bottom_def symmetric.left_bottom_def symmetric.middle_inter_left_bottom
  by (metis Int_commute)

text ‹The normality argument for the right wing is exactly the symmetric instance.›
lemma right_bottom_normal: "normal_subgroup right_bottom right_top (⋅) 𝟭"
  using right_bottom_eq right_top_eq symmetric.left_bottom_eq symmetric.left_bottom_normal
    symmetric.left_top_eq by (metis inf.commute)

subsection ‹The quotient isomorphism›

interpretation left_quotient: normal_subgroup left_bottom left_top "(⋅)" 𝟭 
  by (rule left_bottom_normal)

interpretation right_quotient: normal_subgroup right_bottom right_top "(⋅)" 𝟭
  by (rule right_bottom_normal)

lemma middle_subset_left_top: "H ∩ K ⊆ left_top"
  using left_top_product.H_subset_HK unfolding left_top_eq .

lemma middle_subset_right_top: "H ∩ K ⊆ right_top"
  using right_top_product.H_subset_HK unfolding right_top_eq .

lemma middle_left_top_subgroup: "Subgroup (H ∩ K) left_top (⋅) 𝟭"
  by (rule subgroup_restrict[OF middle_H.Subgroup_axioms left_top_subgroup middle_subset_left_top])

lemma middle_right_top_subgroup: "Subgroup (H ∩ K) right_top (⋅) 𝟭"
  by (rule subgroup_restrict[OF middle_K.Subgroup_axioms right_top_subgroup middle_subset_right_top])

interpretation middle_left_top: subgroup_of_group "H ∩ K" left_top "(⋅)" 𝟭
  by (rule subgroup_of_groupI[OF middle_left_top_subgroup left_quotient.Group_axioms])

interpretation middle_right_top: subgroup_of_group "H ∩ K" right_top "(⋅)" 𝟭
  by (rule subgroup_of_groupI[OF middle_right_top_subgroup right_quotient.Group_axioms])

interpretation left_second:
  second_iso_theorem left_bottom "H ∩ K" left_top "(⋅)" 𝟭 ..

interpretation right_second:
  second_iso_theorem right_bottom "H ∩ K" right_top "(⋅)" 𝟭 ..

lemma left_second_product: "left_second.HK = left_top"
proof (intro equalityI subsetI)
  fix x
  assume "x ∈ left_second.HK"
  then obtain h k where h: "h ∈ H ∩ K" and k: "k ∈ left_bottom"
    and x_eq: "x = h ⋅ k" by (rule left_second.HK_memE)
  show "x ∈ left_top"
    unfolding x_eq using h k by blast
next
  fix x
  assume x: "x ∈ left_top"
  then obtain h n where h: "h ∈ H ∩ K" and n: "n ∈ H1" and x_eq: "x = h ⋅ n"
    by (rule left_top_memE)
  have unit_inter: "𝟭 ∈ H ∩ K1"
    using H.sub_unit_closed K1.sub_unit_closed by blast
  then have "n ∈ left_bottom"
    using H1.sub.left_unit left_bottom_memI n by metis
  then show "x ∈ left_second.HK"
    using h left_second.HK_memI x_eq by blast
qed

lemma right_second_product: "right_second.HK = right_top"
proof (intro equalityI subsetI)
  fix x
  assume "x ∈ right_second.HK"
  then obtain h k where h: "h ∈ H ∩ K" and k: "k ∈ right_bottom"
    and x_eq: "x = h ⋅ k" by (rule right_second.HK_memE)
  show "x ∈ right_top"
    unfolding x_eq using h k by blast
next
  fix x
  assume x: "x ∈ right_top"
  then obtain h n where h': "h ∈ K ∩ H" and n: "n ∈ K1" and x_eq: "x = h ⋅ n"
    using right_top_eq right_top_product.HK_memE by (metis Int_commute)
  have unit_inter: "𝟭 ∈ K ∩ H1"
    using K.sub_unit_closed H1.sub_unit_closed by blast
  then have "n ∈ right_bottom"
    using K1.sub.left_unit n right_bottom_eq right_bottom_product.HK_memI by metis
  then show "x ∈ right_second.HK" unfolding x_eq
    using h' right_second.HK_memI by blast
qed

lemma left_second_factor_group:
  "left_second.Fract_HK_K = left_quotient.Factor_Group"
  using left_quotient.Partition_def left_second.Fract_HK_K_def left_second_product by argo


lemma right_second_factor_group:
  "right_second.Fract_HK_K = right_quotient.Factor_Group"
  using right_quotient.Partition_def right_second.Fract_HK_K_def right_second_product by argo

lemma common_denominator:
  "(H ∩ K) ∩ left_bottom = (H ∩ K) ∩ right_bottom"
  unfolding middle_inter_left_bottom middle_inter_right_bottom
  using HK1_normal.subset KH1_normal.set_prod_commute by metis

interpretation left_common:
  normal_subgroup "(H ∩ K) ∩ left_bottom" "H ∩ K" "(⋅)" 𝟭
  using left_bottom_normal left_quotient.normal_subgroup_intersection middle_left_top_subgroup
  by blast

interpretation right_common:
  normal_subgroup "(H ∩ K) ∩ right_bottom" "H ∩ K" "(⋅)" 𝟭
  using common_denominator left_common.normal_subgroup_axioms by force

lemma left_wing_isomorphism:
  "(left_quotient.Factor_Group, left_quotient.quotient_composition,
      left_quotient.Class 𝟭) ≅⇩G
   (left_second.Fract_H_HIntK, left_common.quotient_composition,
      left_common.Class 𝟭)"
  using left_second.second_isomorphism
  unfolding left_second_factor_group .

lemma right_wing_isomorphism:
  "(right_quotient.Factor_Group, right_quotient.quotient_composition,
      right_quotient.Class 𝟭) ≅⇩G
   (right_second.Fract_H_HIntK, right_common.quotient_composition,
      right_common.Class 𝟭)"
  using right_second.second_isomorphism
  unfolding right_second_factor_group .

lemma common_factor_group:
  "(left_second.Fract_H_HIntK, left_common.quotient_composition,
      left_common.Class 𝟭) =
   (right_second.Fract_H_HIntK, right_common.quotient_composition,
      right_common.Class 𝟭)"
  using common_denominator left_second.Fract_H_HIntK_def right_second.Fract_H_HIntK_def
  by presburger

text ‹
  The Zassenhaus lemma: the quotients represented by the two wings of the
  butterfly are isomorphic.  The quotient operations and units are displayed
  explicitly, as is customary in New-Algebra's set-based API.
›
theorem butterfly_lemma:
  "(left_quotient.Factor_Group, left_quotient.quotient_composition,
      left_quotient.Class 𝟭) ≅⇩G
   (right_quotient.Factor_Group, right_quotient.quotient_composition,
      right_quotient.Class 𝟭)"
  using common_factor_group left_wing_isomorphism right_wing_isomorphism
  by (metis isomorphic_as_groups_symmetric isomorphic_as_groups_transitive)

end (* zassenhaus *)

end