Theory Schreier_Refinement

section ‹The Schreier refinement theorem›

theory Schreier_Refinement
  imports Normal_Chain Zassenhaus_Lemma
begin

subsection ‹Refining pairs of finite normal series›

text ‹
  The Zassenhaus lemma compares one refinement cell determined by a step from
  each of two normal series.  We name the two families of subgroup products
  independently of a particular cell.  Fixing one index produces a row of
  intermediate subgroups refining the corresponding step of the other series.
›

locale normal_series_pair =
  A: normal_series G "(⋅)" 𝟭 A m +
  B: normal_series G "(⋅)" 𝟭 B n
  for G and composition (infixl ‹⋅› 70) and unit (‹𝟭›)
    and A :: "nat ⇒ 'a set" and m
    and B :: "nat ⇒ 'a set" and n
begin

definition left_refinement_term :: "nat ⇒ nat ⇒ 'a set"
  where "left_refinement_term i j ≡ (case_prod (⋅)) ` ((A (Suc i) ∩ B j) × A i)"

definition right_refinement_term :: "nat ⇒ nat ⇒ 'a set"
  where "right_refinement_term j i ≡ (case_prod (⋅)) ` ((B (Suc j) ∩ A i) × B j)"

end

locale series_refinement_cell =
  normal_series_pair G "(⋅)" 𝟭 A m B n
  for G and composition (infixl ‹⋅› 70) and unit (‹𝟭›)
    and A :: "nat ⇒ 'a set" and m
    and B :: "nat ⇒ 'a set" and n
    and i j +
  assumes i_lt: "i < m" and j_lt: "j < n"
begin

lemma ambient_group:
  "Group G (⋅) 𝟭"
  by (rule A.G.Group_axioms)

lemma A_step_top_subgroup:
  "subgroup_of_group (A (Suc i)) G (⋅) 𝟭"
  by (simp add: A.term_subgroup Suc_leI ambient_group i_lt subgroup_of_group_def)

lemma B_step_top_subgroup:
  "subgroup_of_group (B (Suc j)) G (⋅) 𝟭"
  by (simp add: B.term_subgroup Suc_leI ambient_group j_lt subgroup_of_group_def)

interpretation cell: zassenhaus
    G "A (Suc i)" "B (Suc j)" "A i" "B j" "(⋅)" 𝟭
  by (simp add: zassenhaus.intro A.normal_step A_step_top_subgroup B.normal_step B_step_top_subgroup ambient_group i_lt
      j_lt)

lemma left_refinement_bottom_eq:
  "left_refinement_term i j = cell.left_bottom"
  using cell.left_bottom_def left_refinement_term_def by auto

lemma left_refinement_top_eq:
  "left_refinement_term i (Suc j) = cell.left_top"
  using cell.left_top_def left_refinement_term_def by auto

lemma right_refinement_bottom_eq:
  "right_refinement_term j i = cell.right_bottom"
  using cell.right_bottom_def right_refinement_term_def by auto

lemma right_refinement_top_eq:
  "right_refinement_term j (Suc i) = cell.right_top"
  using cell.right_top_def right_refinement_term_def by auto

lemma left_refinement_normal:
  "normal_subgroup (left_refinement_term i j) (left_refinement_term i (Suc j)) (⋅) 𝟭"
  using cell.left_bottom_normal left_refinement_bottom_eq left_refinement_top_eq by argo

lemma right_refinement_normal:
  "normal_subgroup (right_refinement_term j i) (right_refinement_term j (Suc i)) (⋅) 𝟭"
  using cell.right_bottom_normal right_refinement_bottom_eq right_refinement_top_eq by argo

text ‹
  Opposite sides of every refinement cell have the same native quotient-group
  isomorphism class.  This is the factor-level form of Zassenhaus needed by a
  later Schreier refinement theorem; the statement contains no HOL-Algebra
  records and no representatives of quotient isomorphisms.
›
theorem refinement_cell_factor_class_eq:
  "normal_factor_class (left_refinement_term i j) (left_refinement_term i (Suc j)) (⋅) 𝟭 =
   normal_factor_class (right_refinement_term j i) (right_refinement_term j (Suc i)) (⋅) 𝟭"
proof -
  have "normal_factor (left_refinement_term i j) (left_refinement_term i (Suc j)) (⋅) 𝟭 ≅⇩G
        normal_factor (right_refinement_term j i) (right_refinement_term j (Suc i)) (⋅) 𝟭"
    unfolding normal_factor_def left_refinement_bottom_eq left_refinement_top_eq
      right_refinement_bottom_eq right_refinement_top_eq
    by (rule cell.butterfly_lemma)
  then show ?thesis
    by (simp add: left_refinement_normal normal_factor_class_eq_iff right_refinement_normal)
qed

end

text ‹
  The factors of a refinement are read row by row.  The following elementary
  lemmas turn a rectangular list of entries into finite sums of singleton
  multisets; this makes transposition of the refinement matrix explicit in the
  final proof.
›

lemma mset_map_upt:
  "mset (List.map f [0..<n]) = (∑i<n. {#f i#})"
  by (induction n) (simp_all add: sum.lessThan_Suc)

lemma mset_concat_map_upt:
  "mset (concat (List.map (λi. List.map (f i) [0..<n]) [0..<m])) = (∑i<m. ∑j<n. {#f i j#})"
proof (induction m)
  case 0
  show ?case by simp
next
  case (Suc m)
  have row: "mset (List.map (f m) [0..<n]) = (∑j<n. {#f m j#})"
    by (rule mset_map_upt)
  have "mset (concat (List.map (λi. List.map (f i) [0..<n]) [0..<Suc m])) =
      mset (concat (List.map (λi. List.map (f i) [0..<n]) [0..<m])) + mset (List.map (f m) [0..<n])"
    by simp
  also have "... = (∑i<Suc m. ∑j<n. {#f i j#})"
    using Suc row by auto
  finally show ?case .
qed

lemma length_concat_map_upt:
  "length (concat (List.map (λi. List.map (f i) [0..<n]) [0..<m])) = m * n"
  by (induction m) (simp_all add: algebra_simps)

text ‹
  At the endpoints of a refinement row, one factor in a subgroup product is
  either trivial or the whole carrier.  For intermediate terms, intersecting
  the carrier with another ambient subgroup and multiplying by a normal
  subgroup again gives an ambient subgroup.  These generic facts keep the row
  proofs below independent of quotient representations.
›

lemma subgroup_product_with_trivial_left:
  assumes K: "Subgroup K G composition unit"
  shows "(case_prod composition) ` ({unit} × K) = K"
proof -
  interpret K: Subgroup K G composition unit by fact
  show ?thesis
    by force
qed

lemma subgroup_product_with_carrier_left:
  assumes K: "Subgroup K H composition unit"
  shows "(case_prod composition) ` (H × K) = H"
proof -
  obtain K_submonoid: "Submonoid K H composition unit" and H_monoid: "Monoid H composition unit"
    using assms by (meson Subgroup_def Submonoid.axioms(1))
  have unit_K: "unit ∈ K"
    by (rule Submonoid.sub_unit_closed[OF K_submonoid])
  show ?thesis
  proof (intro equalityI subsetI)
    show "⋀x. x ∈ (λ(x, y). composition x y) ` (H × K) ⟹ x ∈ H"
      using H_monoid K_submonoid Monoid.composition_closed Submonoid.sub by fastforce
    show "⋀x. x ∈ H ⟹ x ∈ (λ(x, y). composition x y) ` (H × K)"
      using H_monoid unit_K by (metis Monoid.right_unit SigmaI pair_imageI)
  qed
qed

lemma intersection_normal_product_subgroup:
  assumes G: "Group G composition unit"
    and N: "normal_subgroup K H composition unit"
    and H: "Subgroup H G composition unit"
    and L: "Subgroup L G composition unit"
  shows "Subgroup ((case_prod composition) ` ((H ∩ L) × K))
    G composition unit"
proof -
  interpret N: normal_subgroup K H composition unit by fact
  have intersection_group:
      "subgroup_of_group (H ∩ L) H composition unit"
    using G H L N.Group_axioms
    by (meson Group.subgroup_intersection inf_le1 subgroup_of_group_def subgroup_restrict)
  show ?thesis
    using H N intersection_group
    by (metis normal_subgroup_product.HK_def normal_subgroup_product.HK_subgroup
        normal_subgroup_product.intro subgroup_transitive)
qed

context normal_series_pair
begin

text ‹
  For every pair of valid step indices, the assumptions of
  @{locale series_refinement_cell} follow directly from the two series.  We
  construct the locale predicate without interpreting it, so clients can
  reuse the proved cell API without re-elaborating the Zassenhaus locale.
›
lemma series_refinement_cellI:
  assumes i: "i < m" and j: "j < n"
  shows "series_refinement_cell G (⋅) 𝟭 A m B n i j"
  by (simp add: i j normal_series_pair_axioms series_refinement_cell_axioms.intro
      series_refinement_cell_def)

subsection ‹Refinement rows›

text ‹
  The left row at index @{term i} runs from @{term "A i"} to
  @{term "A (Suc i)"}; the right row at index @{term j} runs from
  @{term "B j"} to @{term "B (Suc j)"}.  Thus concatenating rows in increasing
  outer index refines the original series.  The normal-chain theorems verify
  every intermediate subgroup and adjacent normality condition.
›

lemma left_refinement_start:
  assumes i: "i < m"
  shows "left_refinement_term i 0 = A i"
proof -
  interpret ASi: Subgroup "A (Suc i)" G "(⋅)" 𝟭
    by (rule A.term_subgroup) (use i in simp)
  have intersection: "A (Suc i) ∩ B 0 = {𝟭}"
    using B.bottom ASi.sub_unit_closed by auto
  show ?thesis
    unfolding left_refinement_term_def intersection
    using subgroup_product_with_trivial_left[OF A.term_subgroup] i by simp
qed

lemma left_refinement_end:
  assumes i: "i < m"
  shows "left_refinement_term i n = A (Suc i)"
proof -
  interpret ASi: Subgroup "A (Suc i)" G "(⋅)" 𝟭
    by (rule A.term_subgroup) (use i in simp)
  have intersection: "A (Suc i) ∩ B n = A (Suc i)"
    using B.top ASi.subset by auto
  show ?thesis
    unfolding left_refinement_term_def intersection
    by (rule subgroup_product_with_carrier_left[OF A.normal_step_subgroup[OF i]])
qed

lemma right_refinement_start:
  assumes j: "j < n"
  shows "right_refinement_term j 0 = B j"
proof -
  interpret BSj: Subgroup "B (Suc j)" G "(⋅)" 𝟭
    by (rule B.term_subgroup) (use j in simp)
  have intersection: "B (Suc j) ∩ A 0 = {𝟭}"
    using A.bottom BSj.sub_unit_closed by auto
  show ?thesis
    unfolding right_refinement_term_def intersection
    using subgroup_product_with_trivial_left[OF B.term_subgroup] j by simp
qed

lemma right_refinement_end:
  assumes j: "j < n"
  shows "right_refinement_term j m = B (Suc j)"
proof -
  interpret BSj: Subgroup "B (Suc j)" G "(⋅)" 𝟭
    by (rule B.term_subgroup) (use j in simp)
  have intersection: "B (Suc j) ∩ A m = B (Suc j)"
    using A.top BSj.subset by auto
  show ?thesis
    unfolding right_refinement_term_def intersection
    by (rule subgroup_product_with_carrier_left[OF B.normal_step_subgroup[OF j]])
qed

lemma left_refinement_step:
  assumes i: "i < m" and j: "j < n"
  shows "normal_subgroup (left_refinement_term i j) (left_refinement_term i (Suc j)) (⋅) 𝟭"
  using i j series_refinement_cellI by (meson series_refinement_cell.left_refinement_normal)

lemma left_refinement_term_subgroup:
  assumes i: "i < m" and j: "j ≤ n"
  shows "Subgroup (left_refinement_term i j) G (⋅) 𝟭"
  unfolding left_refinement_term_def
  by (simp add: A.G.Group_axioms A.normal_step A.term_subgroup B.term_subgroup Suc_leI i
      intersection_normal_product_subgroup j)

lemma right_refinement_step:
  assumes i: "i < m" and j: "j < n"
  shows "normal_subgroup (right_refinement_term j i) (right_refinement_term j (Suc i)) (⋅) 𝟭"
  using i j series_refinement_cellI by (meson series_refinement_cell.right_refinement_normal)

lemma right_refinement_term_subgroup:
  assumes i: "i ≤ m" and j: "j < n"
  shows "Subgroup (right_refinement_term j i) G (⋅) 𝟭"
  unfolding right_refinement_term_def
  by (simp add: A.G.Group_axioms A.term_subgroup B.normal_step B.term_subgroup Suc_leI i
      intersection_normal_product_subgroup j)

lemma left_refinement_row:
  assumes i: "i < m"
  shows "normal_chain G (⋅) 𝟭 (left_refinement_term i) n"
proof (intro normal_chain.intro A.G.Group_axioms)
  show "normal_chain_axioms G (⋅) 𝟭 (left_refinement_term i) n"
    by (simp add: i left_refinement_step left_refinement_term_subgroup normal_chain_axioms_def)
qed

lemma right_refinement_row:
  assumes j: "j < n"
  shows "normal_chain G (⋅) 𝟭 (right_refinement_term j) m"
proof (intro normal_chain.intro A.G.Group_axioms)
  show "normal_chain_axioms G (⋅) 𝟭 (right_refinement_term j) m"
    by (simp add: j normal_chain_axioms_def right_refinement_step right_refinement_term_subgroup)
qed

subsection ‹Factor-class refinements›

text ‹
  The two lists below flatten the left and right refinement rows in row-major
  order.  Each entry is the native isomorphism class of the corresponding
  normal-chain factor; repeated or trivial factors are retained.
›

definition left_refinement_factor_class :: "nat ⇒ nat ⇒ 'a set monoid_iso_class"
  where
    "left_refinement_factor_class i j ≡
      normal_factor_class (left_refinement_term i j) (left_refinement_term i (Suc j)) (⋅) 𝟭"

definition right_refinement_factor_class :: "nat ⇒ nat ⇒ 'a set monoid_iso_class"
  where
    "right_refinement_factor_class j i ≡
      normal_factor_class (right_refinement_term j i) (right_refinement_term j (Suc i)) (⋅) 𝟭"

definition left_refinement_factor_classes :: "'a set monoid_iso_class list"
  where
    "left_refinement_factor_classes ≡
      concat (List.map (λi. List.map (left_refinement_factor_class i) [0..<n]) [0..<m])"

definition right_refinement_factor_classes :: "'a set monoid_iso_class list"
  where
    "right_refinement_factor_classes ≡
      concat (List.map
        (λj. List.map (right_refinement_factor_class j) [0..<m]) [0..<n])"

lemma length_left_refinement_factor_classes:
  "length left_refinement_factor_classes = m * n"
  unfolding left_refinement_factor_classes_def by (rule length_concat_map_upt)

lemma length_right_refinement_factor_classes:
  "length right_refinement_factor_classes = n * m"
  unfolding right_refinement_factor_classes_def by (rule length_concat_map_upt)

lemma refinement_factor_class_eq:
  assumes i: "i < m" and j: "j < n"
  shows "left_refinement_factor_class i j = right_refinement_factor_class j i"
proof -
  have C: "series_refinement_cell G (⋅) 𝟭 A m B n i j"
    by (rule series_refinement_cellI[OF i j])
  show ?thesis
    unfolding left_refinement_factor_class_def right_refinement_factor_class_def
    by (rule series_refinement_cell.refinement_cell_factor_class_eq[OF C])
qed

text ‹
  The two row-major factor lists need not have the same order.  Their
  multisets agree: transposing the refinement matrix sends the factor at
  position @{term "(i, j)"} to the isomorphic factor at @{term "(j, i)"}.
  This is the native, factor-class form of the Schreier refinement theorem.
›
theorem schreier_refinement:
  "mset left_refinement_factor_classes = mset right_refinement_factor_classes"
proof -
  have transpose:
      "(∑i<m. ∑j<n. {#left_refinement_factor_class i j#}) =
       (∑j<n. ∑i<m. {#right_refinement_factor_class j i#})"
    using refinement_factor_class_eq sum.swap by auto
  show ?thesis
    unfolding left_refinement_factor_classes_def right_refinement_factor_classes_def mset_concat_map_upt
    using transpose by blast
qed

end

subsection ‹Reduced Schreier refinements›

text ‹
  A finite normal chain may repeat a term.  Its corresponding quotient is the
  one-element group and contributes no genuine factor.  The operation below
  removes precisely the canonical trivial isomorphism class while retaining
  multiplicity and forgetting order.
›
definition nontrivial_factor_multiset ::
    "'a monoid_iso_class list ⇒ 'a monoid_iso_class multiset"
  where
    "nontrivial_factor_multiset factors ≡ filter_mset (λC. C ≠ trivial_monoid_iso_class) (mset factors)"

lemma nontrivial_factor_multiset_cong:
  assumes "mset factors = mset factors'"
  shows "nontrivial_factor_multiset factors = nontrivial_factor_multiset factors'"
  using assms unfolding nontrivial_factor_multiset_def by simp

lemma nontrivial_factor_multiset_append [simp]:
  "nontrivial_factor_multiset (factors @ factors') =
    nontrivial_factor_multiset factors + nontrivial_factor_multiset factors'"
  unfolding nontrivial_factor_multiset_def by simp

lemma nontrivial_factor_multiset_Nil [simp]:
  "nontrivial_factor_multiset [] = {#}"
  unfolding nontrivial_factor_multiset_def by simp

lemma nontrivial_factor_multiset_singleton [simp]:
  "nontrivial_factor_multiset [C] =
    (if C = trivial_monoid_iso_class then {#} else {#C#})"
  unfolding nontrivial_factor_multiset_def by simp

lemma nontrivial_factor_multiset_concat_map_upt:
  "nontrivial_factor_multiset (concat (List.map f [0..<m])) =
    (∑i<m. nontrivial_factor_multiset (f i))"
  by (induction m) (simp_all add: sum.lessThan_Suc)

context normal_series_pair
begin

text ‹
  The trivial-class test has a concrete chain interpretation: it detects
  exactly an adjacent repetition.  These equivalences are the bridge used by
  the later Jordan--Hölder argument when a refinement row lies inside a simple
  factor.
›
lemma left_refinement_factor_class_eq_trivial_iff:
  assumes i: "i < m" and j: "j < n"
  shows "left_refinement_factor_class i j = trivial_monoid_iso_class
    ⟷ left_refinement_term i j = left_refinement_term i (Suc j)"
  by (simp add: i j left_refinement_factor_class_def left_refinement_step normal_factor_class_eq_trivial_iff)

lemma right_refinement_factor_class_eq_trivial_iff:
  assumes i: "i < m" and j: "j < n"
  shows "right_refinement_factor_class j i = trivial_monoid_iso_class
    ⟷ right_refinement_term j i = right_refinement_term j (Suc i)"
  by (simp add: i j normal_factor_class_eq_trivial_iff right_refinement_factor_class_def right_refinement_step)

definition left_reduced_refinement_factor_multiset :: "'a set monoid_iso_class multiset"
  where "left_reduced_refinement_factor_multiset ≡ nontrivial_factor_multiset left_refinement_factor_classes"

definition right_reduced_refinement_factor_multiset :: "'a set monoid_iso_class multiset"
  where "right_reduced_refinement_factor_multiset ≡ nontrivial_factor_multiset right_refinement_factor_classes"

text ‹
  Removing repetition factors from equivalent Schreier refinements preserves
  equality.  Unlike @{thm schreier_refinement}, this form is ready to compare
  directly with the factor multiset of a composition series.
›
theorem reduced_schreier_refinement:
  "left_reduced_refinement_factor_multiset = right_reduced_refinement_factor_multiset"
  by (simp add: left_reduced_refinement_factor_multiset_def nontrivial_factor_multiset_def
      right_reduced_refinement_factor_multiset_def schreier_refinement)

end

end