Theory Normal_Series

theory Normal_Series
  imports Group_Theory
begin

section ‹Finite normal series›

text ‹
  The canonical one-step series has the trivial subgroup at index zero and the
  full carrier thereafter.  Values beyond its declared length are immaterial.
›
definition one_step_normal_series_term ::
    "'a set ⇒ 'a ⇒ nat ⇒ 'a set"
  where
    "one_step_normal_series_term G unit i = (if i = 0 then {unit} else G)"

text ‹
  A finite normal series is a finite chain of subgroups beginning at the
  trivial subgroup and ending at the ambient group, with each term normal in
  the next one.  The chain is indexed by the natural numbers from @{term 0}
  through @{term n}; repeated terms are permitted, so strictness can be added
  separately when defining composition series.

  The definition is deliberately stated with carrier sets and the existing
  @{locale normal_subgroup} locale.  In particular, it does not introduce a
  second representation of quotient groups or subgroup chains.
›

locale normal_series =
  G: Group G "(⋅)" 𝟭
  for G and composition (infixl ‹⋅› 70) and unit (‹𝟭›) +
  fixes H :: "nat ⇒ 'a set" and n :: nat
  assumes bottom: "H 0 = {𝟭}"
    and top: "H n = G"
    and term_subgroup: "⋀i. i ≤ n ⟹ Subgroup (H i) G (⋅) 𝟭"
    and normal_step:
      "⋀i. i < n ⟹ normal_subgroup (H i) (H (Suc i)) (⋅) 𝟭"
begin

text ‹
  The factor at index @{term i} is packaged as the carrier, operation, and unit
  of the quotient of @{term "H (Suc i)"} by @{term "H i"}.  The definition is
  total in the index; the series assumptions provide the group interpretation
  whenever @{term "i < n"}.
›

definition series_factor ::
    "nat ⇒ ('a set set × ('a set ⇒ 'a set ⇒ 'a set) × 'a set)"
  where
    "series_factor i =
      (normal_subgroup.Factor_Group (H i) (H (Suc i)) (⋅) 𝟭,
       Monoid_congruence.quotient_composition
         (H (Suc i)) (⋅)
         (normal_subgroup.Congruence (H i) (H (Suc i)) (⋅) 𝟭),
       Equivalence.Class (H (Suc i))
         (normal_subgroup.Congruence (H i) (H (Suc i)) (⋅) 𝟭) 𝟭)"

text ‹The finite factor sequence is ordered by increasing index.›

definition series_factors ::
    "('a set set × ('a set ⇒ 'a set ⇒ 'a set) × 'a set) list"
  where
    "series_factors = List.map series_factor [0..<n]"

lemma length_series_factors:
  "length series_factors = n"
  unfolding series_factors_def by simp

lemma series_factors_prefix:
  assumes k: "k ≤ n"
  shows "take k series_factors = List.map series_factor [0..<k]"
  using k unfolding series_factors_def by (simp add: take_map)

lemma series_factors_nth:
  assumes i: "i < n"
  shows "series_factors ! i = series_factor i"
  using i unfolding series_factors_def by simp

lemma series_factor_group:
  assumes i: "i < n"
  shows "Group (fst (series_factor i))
      (fst (snd (series_factor i))) (snd (snd (series_factor i)))"
proof -
  interpret step: normal_subgroup "H i" "H (Suc i)" "(⋅)" 𝟭
    by (rule normal_step[OF i])
  show ?thesis
    unfolding series_factor_def
    using step.quotient.Group_axioms by simp
qed

text ‹The adjacent terms form a subgroup and are ordered by inclusion.›

lemma normal_step_subgroup:
  assumes i: "i < n"
  shows "Subgroup (H i) (H (Suc i)) (⋅) 𝟭"
proof -
  interpret step: normal_subgroup "H i" "H (Suc i)" "(⋅)" 𝟭
    by (rule normal_step[OF i])
  show ?thesis by (rule step.Subgroup_axioms)
qed

lemma normal_step_subset:
  assumes i: "i < n"
  shows "H i ⊆ H (Suc i)"
proof -
  interpret step: normal_subgroup "H i" "H (Suc i)" "(⋅)" 𝟭
    by (rule normal_step[OF i])
  show ?thesis by (rule step.subset)
qed

lemma series_term_subset:
  assumes i: "i ≤ n"
  shows "H i ⊆ G"
proof -
  interpret T: Subgroup "H i" G "(⋅)" 𝟭
    by (rule term_subgroup[OF i])
  show ?thesis by (rule T.subset)
qed

text ‹Inclusion propagates through the entire finite chain.›

lemma normal_series_mono:
  fixes i j :: nat
  assumes ij: "i ≤ j" and jn: "j ≤ n"
  shows "H i ⊆ H j"
  using ij
proof (induction rule: inc_induct)
  case base
  show "H j ⊆ H j" by simp
next
  case (step k)
  have k_lt_n: "k < n"
  proof (rule less_le_trans)
    show "k < j" by (rule step(2))
    show "j ≤ n" by fact
  qed
  have step_k: "H k ⊆ H (Suc k)"
    by (rule normal_step_subset[OF k_lt_n])
  have ih: "H (Suc k) ⊆ H j"
    by (rule step(3))
  show ?case by (rule subset_trans[OF step_k ih])
qed

lemma series_bottom_subset:
  assumes i: "i ≤ n"
  shows "H 0 ⊆ H i"
  by (rule normal_series_mono[OF zero_le i])

text ‹Every term in a prefix is a subgroup of the prefix's top term.›

lemma series_prefix_subgroup:
  assumes k: "k ≤ n" and i: "i ≤ k"
  shows "Subgroup (H i) (H k) (⋅) 𝟭"
proof -
  have i_n: "i ≤ n" by (rule le_trans[OF i k])
  have i_subset_k: "H i ⊆ H k" by (rule normal_series_mono[OF i k])
  show ?thesis
  proof (rule subgroup_restrict)
    show "Subgroup (H i) G (⋅) 𝟭" by (rule term_subgroup[OF i_n])
    show "Subgroup (H k) G (⋅) 𝟭" by (rule term_subgroup[OF k])
    show "H i ⊆ H k" by fact
  qed
qed

text ‹The terms up to any index form a normal series for that term.›

lemma prefix_normal_series:
  assumes k: "k ≤ n"
  shows "normal_series (H k) (⋅) 𝟭 H k"
proof -
  have Hk_subgroup: "Subgroup (H k) G (⋅) 𝟭"
    by (rule term_subgroup[OF k])
  have Hk_group: "Group (H k) (⋅) 𝟭"
    by (rule subgroup_imp_Group[OF Hk_subgroup])
  show ?thesis
  proof (intro normal_series.intro)
    show "Group (H k) (⋅) 𝟭" by fact
  next
    show "normal_series_axioms (H k) (⋅) 𝟭 H k"
    proof (intro normal_series_axioms.intro)
      show "H 0 = {𝟭}" by (rule bottom)
    next
      show "H k = H k" by simp
    next
      show "⋀i. i ≤ k ⟹ Subgroup (H i) (H k) (⋅) 𝟭"
      proof -
        fix i
        assume i: "i ≤ k"
        show "Subgroup (H i) (H k) (⋅) 𝟭"
          by (rule series_prefix_subgroup[OF k i])
      qed
    next
      show "⋀i. i < k ⟹ normal_subgroup (H i) (H (Suc i)) (⋅) 𝟭"
      proof -
        fix i
        assume i: "i < k"
        have i_n: "i < n" by (rule less_le_trans[OF i k])
        show "normal_subgroup (H i) (H (Suc i)) (⋅) 𝟭"
          by (rule normal_step[OF i_n])
      qed
    qed
  qed
qed

lemma zero_length_implies_trivial:
  assumes "n = 0"
  shows "G = {𝟭}"
proof -
  have "G = H 0"
    using top assms by simp
  also have "... = {𝟭}"
    by (rule bottom)
  finally show "G = {𝟭}" .
qed

end

context Group begin

text ‹
  Every group has the canonical one-step normal series from its trivial
  subgroup to its full carrier.  For the trivial group the two terms coincide,
  as repetitions are permitted in a normal series.
›
lemma one_step_normal_series:
  "normal_series G (⋅) 𝟭 (one_step_normal_series_term G 𝟭) 1"
proof (intro normal_series.intro)
  show "Group G (⋅) 𝟭" by (rule Group_axioms)
  show "normal_series_axioms G (⋅) 𝟭
      (one_step_normal_series_term G 𝟭) 1"
  proof (rule normal_series_axioms.intro)
    show "one_step_normal_series_term G 𝟭 0 = {𝟭}"
      by (simp add: one_step_normal_series_term_def)
    show "one_step_normal_series_term G 𝟭 1 = G"
      by (simp add: one_step_normal_series_term_def)
    show "⋀i. i ≤ 1 ⟹
        Subgroup (one_step_normal_series_term G 𝟭 i) G (⋅) 𝟭"
      by (auto simp: one_step_normal_series_term_def le_Suc_eq
            trivial_subgroup group_self_subgroup)
    show "⋀i. i < 1 ⟹
        normal_subgroup (one_step_normal_series_term G 𝟭 i)
          (one_step_normal_series_term G 𝟭 (Suc i)) (⋅) 𝟭"
      using trivial_normal_subgroup
      by (simp add: one_step_normal_series_term_def)
  qed
qed

end

end