Theory Symmetric_Group

section ‹The Symmetric and Alternating Groups›

theory Symmetric_Group
  imports Group_Theory "HOL-Combinatorics.Permutations" "HOL-Combinatorics.Cycles"
begin

text ‹
  We realise the concrete symmetric group @{text "Sn"} as the group of permutations of
  @{term "{0..<n}"} under function composition, reusing the permutation and sign
  machinery of @{theory "HOL-Combinatorics.Permutations"}.

  Design note: the development's own @{term "transformations.Sym"} consists of
  ∗‹extensional› maps (undefined outside the carrier), which does not interoperate
  directly with the library predicate @{term "p permutes S"} (identity outside the
  carrier).  Building @{text "Sn"} natively on @{term "{p. p permutes S}"} avoids that
  impedance mismatch and lets us inherit @{const sign} and its homomorphism property
  for free.
›

subsection ‹The symmetric group as a @{locale Group}›

definition Sn :: "nat ⇒ (nat ⇒ nat) set"
  where "Sn n = {p. p permutes {0..<n}}"

lemma Sn_iff: "p ∈ Sn n ⟷ p permutes {0..<n}"
  by (simp add: Sn_def)

lemma Sn_permutation: "p ∈ Sn n ⟹ permutation p"
  by (auto simp: Sn_def permutation_permutes)

text ‹@{term "Sn n"} is a group under composition.›
theorem Group_Sn: "Group (Sn n) (∘) id"
proof (rule GroupI)
  fix u assume "u ∈ Sn n"
  then have perm: "u permutes {0..<n}" by (simp add: Sn_def)
  have "inv u ∈ Sn n" "u ∘ inv u = id" "inv u ∘ u = id"
    using perm by (simp_all add: Sn_def permutes_inv permutes_inv_o)
  then show "∃v ∈ Sn n. u ∘ v = id ∧ v ∘ u = id" by blast
qed (auto simp: Sn_def permutes_compose permutes_id o_assoc)


subsection ‹Relation to the development's abstract symmetric group›

text ‹
  The development's own symmetric group @{term "transformations.Sym S"} consists of the
  ∗‹extensional› bijections of @{term S} under @{term "compose S"}/@{term "identity S"}.  
  Our @{term "Sn n"} uses library @{const permutes} maps (identity outside).  The two are 
  reconciled by @{const restrict}: restricting a permutation to @{term S} yields an element
  of @{term "transformations.Sym S"}, and this correspondence is bijective.  This makes
  the concrete @{term "Sn n"} available to the development's @{text Group_Action} machinery.
›

lemma restrict_permutes_in_Sym:
  assumes "p permutes S"
  shows "restrict p S ∈ transformations.Sym S"
  using permutes_imp_bij [OF assms]
    by (simp add: bij_betw_imp_funcset transformations.Units_bij_betwD)

text ‹Conversely, an element of @{term "transformations.Sym S"} permutes @{term S} once it
  is extended by the identity outside @{term S}.›
lemma Sym_extend_permutes:
  assumes "α ∈ transformations.Sym S"
  shows "(λx. if x ∈ S then α x else x) permutes S"
proof (rule bij_imp_permutes)
  have "bij_betw α S S" using assms by (simp add: transformations.Units_bijective)
  then show "bij_betw (λx. if x ∈ S then α x else x) S S"
    by (smt (verit, best) bij_betw_cong)
qed simp


subsection ‹The sign homomorphism and the alternating group›

text ‹The two-element group of signs.›
lemma Group_signs: "Group {1, -1::int} (*) 1"
proof (rule GroupI)
  fix u :: int assume "u ∈ {1, -1}"
  then show "∃v ∈ {1, -1::int}. u * v = 1 ∧ v * u = 1" by force
qed auto

lemma sign_range: "p ∈ Sn n ⟹ sign p ∈ {1, -1::int}"
  by (auto simp: sign_def)

text ‹@{const sign} is a group homomorphism @{text "Sn → {1, -1}"}.  The multiplicativity
  is inherited directly from @{thm [source] sign_compose}.›
lemma sign_hom: "group_homomorphism (restrict sign (Sn n)) (Sn n) (∘) id {1,-1::int} (*) 1"
proof -
  interpret S: Group "Sn n" "(∘)" id by (rule Group_Sn)
  interpret T: Group "{1,-1::int}" "(*)" 1 by (rule Group_signs)
  show ?thesis
  proof qed (use sign_range in ‹auto simp: Sn_permutation sign_compose›)
qed

text ‹The alternating group is the kernel of the sign homomorphism.›
definition An :: "nat ⇒ (nat ⇒ nat) set"
  where "An n = group_homomorphism.Ker (restrict sign (Sn n)) (Sn n) (1::int)"

context
  fixes n::nat
begin

interpretation H: group_homomorphism "restrict sign (Sn n)" "Sn n" "(∘)" id "{1,-1::int}" "(*)" 1
  by (rule sign_hom)

lemma An_normal: "normal_subgroup (An n) (Sn n) (∘) id"
  using An_def H.kernel.normal_subgroup_axioms by presburger

lemma An_iff: "p ∈ An n ⟷ p ∈ Sn n ∧ sign p = 1"
  by (metis An_def H.Ker_image H.Ker_memI H.kernel.sub restrict_apply)

end

lemma An_subset_Sn: "An n ⊆ Sn n"
  by (auto simp: An_iff)


subsection ‹Three-cycles›

text ‹A three-cycle on distinct points of @{term "{0..<n}"} is a permutation, and it is
  even, hence lies in the alternating group.›

lemma three_cycle_permutes:
  assumes "distinct [a,b,c]" "a < n" "b < n" "c < n"
  shows "cycle_of_list [a,b,c] permutes {0..<(n::nat)}"
  using assms cycle_permutes [of "[a,b,c]"] permutes_subset assms by fastforce

lemma three_cycle_in_Sn:
  assumes "distinct [a,b,c]" "a < n" "b < n" "c < n"
  shows "cycle_of_list [a,b,c] ∈ Sn n"
  using assms three_cycle_permutes by (simp add: Sn_def)

lemma three_cycle_sign:
  assumes "distinct [a,b,c]"
  shows "sign (cycle_of_list [a,b,c]) = 1"
proof -
  have "sign (cycle_of_list [a,b,c])
      = sign (Transposition.transpose a b) * sign (Transposition.transpose b c)"
    by (simp add: permutation_swap_id sign_compose)
  also have "… = 1" using assms by (simp add: sign_swap_id)
  finally show ?thesis .
qed

lemma three_cycle_in_An:
  assumes "distinct [a,b,c]" "a < n" "b < n" "c < n"
  shows "cycle_of_list [a,b,c] ∈ An n"
  by (meson An_iff assms three_cycle_in_Sn three_cycle_sign)

end