Theory Symmetric_Generation

section ‹Generating the Symmetric Group›

theory Symmetric_Generation
  imports Symmetric_Group Sylow_Theorems
begin

text ‹@{term "Sn n"} is finite: it is a set of permutations of a finite set.  Stated here at the top
  level --- it was previously inside the anonymous context below that fixes a @{term p}-cycle
  @{term g}, so the exported fact carried that context's four irrelevant assumptions.›
lemma finite_Sn: "finite (Sn n)"
  unfolding Sn_def using finite_permutations[of "{0..<n}"] by simp


text ‹
  The symmetric group @{term "Sn n"} is generated by a single transposition
  together with a full @{term n}-cycle, and (for prime @{term p}) by ∗‹any› transposition
  together with ∗‹any› @{term p}-cycle.  These generation results are the combinatorial
  ingredient that, combined with ‹Sn_not_solvable›, shows that the Galois group
  of a quintic with exactly two non-real roots is the whole of @{term "Sn 5"}.›

subsection ‹A general lemma on generated subgroups›

text ‹Powers of an element of a generated subgroup stay inside it.›
lemma (in Group) generate_funpow:
  assumes "g ∈ generate S"
  shows "power g k ∈ generate S"
  by (induction k) (auto simp add: assms generate.intros)

subsection ‹Conjugation is an automorphism of the generated subgroup›

text ‹Conjugation by a group element @{term g} fixes the unit and commutes with generation:
  the image of @{term "generate S"} under @{term "conjugation g"} is the subgroup generated by
  the image of @{term S}.  This lets a generation result be transported along conjugacy, which
  is what upgrades the standard-cycle generation theorem to an ∗‹arbitrary› cycle.›

lemma (in Group) conjugation_one: "g ∈ G ⟹ conjugation g 𝟭 = 𝟭"
  by (simp add: conjugation_def invertible_right_inverse)

lemma (in Group) conjugation_inv_cancel:
  assumes g: "g ∈ G" and x: "x ∈ G"
  shows "conjugation (inverse g) (conjugation g x) = x"
  using g x by (simp add: conjugation_def associative invertible_left_inverse2 invertible_right_inverse2)

lemma (in Group) conjugation_generate_sub:
  assumes g: "g ∈ G"
  shows "conjugation g ` generate S ⊆ generate (conjugation g ` (S ∩ G))"
proof
  fix y assume "y ∈ conjugation g ` generate S"
  then obtain x where x: "x ∈ generate S" and yx: "y = conjugation g x" by auto
  from x have "conjugation g x ∈ generate (conjugation g ` (S ∩ G))"
  proof induction
    case unit
    then show ?case using conjugation_one[OF g] generate.unit by simp
  next
    case (incl x) then show ?case
      by (simp add: generate.incl conjugation_closed g)
  next
    case (comp x y) 
    then show ?case
      using conjugation_hom generate.comp generate_subset_carrier by (smt (cvc5, best) in_mono)
  next
    case (inv x)
    then show ?case
      by (metis IntD2 conjugation_inverse g generate.inv generate_subset_carrier inf.orderE)
  qed
  then show "y ∈ generate (conjugation g ` (S ∩ G))" using yx by simp
qed

lemma (in Group) conjugation_generate_eq:
  assumes g: "g ∈ G"
  shows "conjugation g ` generate S = generate (conjugation g ` (S ∩ G))"
proof
  show "conjugation g ` generate S ⊆ generate (conjugation g ` (S ∩ G))"
    by (rule conjugation_generate_sub[OF g])
next
  have ginv: "inverse g ∈ G" using g by blast
  let ?T = "conjugation g ` (S ∩ G)"
  have sub2: "conjugation (inverse g) ` generate ?T ⊆ generate (conjugation (inverse g) ` (?T ∩ G))"
    by (rule conjugation_generate_sub[OF ginv])
  have "conjugation (inverse g) ` (?T ∩ G) ⊆ S ∩ G"
    by (auto simp: conjugation_inv_cancel g)
  then have step: "generate (conjugation (inverse g) ` (?T ∩ G)) ⊆ generate (S ∩ G)"
    by (rule generate_mono)
  show "generate ?T ⊆ conjugation g ` generate S"
  proof
    fix y assume y: "y ∈ generate ?T"
    have yG: "y ∈ G" using y generate_subset_carrier by blast
    have "conjugation g (conjugation (inverse g) y) ∈ conjugation g ` generate (S ∩ G)" 
      using sub2 y step by auto
    moreover have "conjugation g (conjugation (inverse g) y) = y"
      using ginv yG conjugation_inv_cancel[OF ginv yG] g by simp
    ultimately show "y ∈ conjugation g ` generate S"
      using generate_mono[of "S ∩ G" S] by auto
  qed
qed

subsection ‹Transpositions generate the symmetric group›

text ‹The set of transpositions of points of @{term "{0..<n}"}.›
definition transpositions :: "nat ⇒ (nat ⇒ nat) set"
  where "transpositions n = {Transposition.transpose a b | a b. a ∈ {0..<n} ∧ b ∈ {0..<n}}"

lemma transpositions_subset_Sn: "transpositions n ⊆ Sn n"
  by (auto simp: transpositions_def Sn_def permutes_swap_id)

subsection ‹The standard ‹n›-cycle›

text ‹The cyclic shift sending ‹i› to ‹Suc i mod n› on @{term "{0..<n}"}, fixing everything
  outside.  We work with this explicit form rather than @{const cycle_of_list} because its
  powers have the transparent closed form @{term "(i + k) mod n"}.›

definition ncycle :: "nat ⇒ nat ⇒ nat"
  where "ncycle n i = (if i < n then Suc i mod n else i)"

lemma ncycle_lt: "i < n ⟹ ncycle n i < n" by (auto simp: ncycle_def)

lemma ncycle_inv_right: "i < n ⟹ ncycle n ((i + (n-1)) mod n) = i"
  by (simp add: mod_if ncycle_def)

lemma ncycle_inv_left: "i < n ⟹ (ncycle n i + (n-1)) mod n = i"
  using mod_if ncycle_def by force

lemma ncycle_permutes: "ncycle n permutes {0..<n}"
proof (rule bij_imp_permutes)
  show "bij_betw (ncycle n) {0..<n} {0..<n}"
  proof (rule bij_betw_byWitness)
    show "∀i∈{0..<n}. ncycle n (if i < n then (i + (n-1)) mod n else i) = i"
      using ncycle_inv_right by auto
  qed (use ncycle_lt ncycle_inv_left in auto)
qed (auto simp: ncycle_def)

lemma ncycle_in_Sn: "ncycle n ∈ Sn n" by (simp add: Sn_def ncycle_permutes)

lemma ncycle_bij: "bij (ncycle n)"
  by (rule permutes_bij[OF ncycle_permutes])

text ‹The closed form for the iterates of the @{term n}-cycle.›
lemma ncycle_funpow: "i < n ⟹ (ncycle n ^^ k) i = (i + k) mod n"
  by (induction k; simp add: mod_Suc_eq ncycle_def)


context
  fixes n::nat
begin

interpretation S: Group "Sn n" "(∘)" id
  by (rule Group_Sn)

text ‹Every permutation of @{term "{0..<n}"} is a product of transpositions, so the
  transpositions generate @{term "Sn n"}.  This follows directly from the tailored induction
  rule @{thm [source] permutes_induct}.›
lemma Sn_generated_by_transpositions:
  "Group.generate (Sn n) (∘) id (transpositions n) = Sn n"
proof
  show "S.generate (transpositions n) ⊆ Sn n"
    using S.generate_subset_carrier by simp
next
  show "Sn n ⊆ S.generate (transpositions n)"
  proof
    fix p assume "p ∈ Sn n"
    then have "p permutes {0..<n}" "finite {0..<n}" by (simp_all add: Sn_def)
    then show "p ∈ S.generate (transpositions n)"
    proof (induction p rule: permutes_induct)
      case id
      show ?case
        using S.generate.unit by blast
    next
      case (swap a b p) 
      then obtain "Transposition.transpose a b ∈ transpositions n" 
                  "Transposition.transpose a b ∈ Sn n"
        using transpositions_def transpositions_subset_Sn by fastforce
      then show ?case
        by (metis Int_iff S.generate.comp S.generate.incl swap.IH)
    qed
  qed
qed


subsection ‹Conjugating a transposition›

text ‹Conjugating a transposition by a bijection transposes the images of the two points.›
lemma transpose_conjug:
  assumes "bij q"
  shows "q ∘ Transposition.transpose a b ∘ inv q = Transposition.transpose (q a) (q b)"
proof -
  have "Transposition.transpose (q a) (q b) ∘ q  = q ∘ Transposition.transpose a b"
    using assms by (simp add: bij_def transpose_comp_eq)
  then show ?thesis
    by (metis assms bij_betw_inv_into bij_is_inj o_inv_o_cancel)
qed

subsection ‹The symmetric group is generated by a transposition and a cycle›

text ‹The group power in @{term "Sn n"} (composition) is just function iteration.›
lemma Sn_power_funpow: "Monoid.power (∘) id (g :: nat ⇒ nat) k = g ^^ k"
  by (metis S.power_def comp_funpow comp_id)

text ‹In @{term "Sn n"} the group inverse is the functional inverse.›
lemma Sn_inverse_eq:
  assumes "p ∈ Sn n"
  shows "Monoid.inverse (Sn n) (∘) id p = inv p"
  using S.invertible_left_inverse2 Sn_iff assms permutes_inv permutes_inv_o(1) by fastforce

lemma t01_in_Sn: "1 < n ⟹ Transposition.transpose 0 1 ∈ Sn n"
  by (simp add: Sn_def permutes_swap_id)

text ‹Conjugating @{term "transpose 0 1"} by the @{term k}-th power of the @{term n}-cycle
  yields the adjacent transposition @{term "transpose (k mod n) (Suc k mod n)"}.›
lemma adjacent_transpose_conjug:
  assumes "k < n" "1 < n"
  shows "(ncycle n ^^ k) ∘ Transposition.transpose 0 1 ∘ inv (ncycle n ^^ k)
         = Transposition.transpose (k mod n) (Suc k mod n)"
proof -
  have "(ncycle n ^^ k) ∘ Transposition.transpose 0 1 ∘ inv (ncycle n ^^ k)
        = Transposition.transpose ((ncycle n ^^ k) 0) ((ncycle n ^^ k) 1)"
    using ncycle_bij bij_fn transpose_conjug by metis
  then show ?thesis
    by (metis One_nat_def Suc_lessD add_0 assms(2) ncycle_funpow plus_1_eq_Suc) 
qed

text ‹Hence each adjacent transposition lies in the subgroup generated by
  @{term "transpose 0 1"} and the @{term n}-cycle.›
lemma adjacent_in_generate:
  assumes "k < n" "1 < n"
  defines "S ≡ {Transposition.transpose 0 1, ncycle n}"
  shows "Transposition.transpose (k mod n) (Suc k mod n) ∈ Group.generate (Sn n) (∘) id S"
proof -
  have t01: "Transposition.transpose 0 1 ∈ S.generate S"
    using Group.generate_incl S.Group_axioms S_def assms(2) t01_in_Sn by fastforce
  have nc: "ncycle n ∈ S.generate S"
    using ncycle_in_Sn by (intro S.generate.incl) (simp add: S_def)
  have powk: "S.power (ncycle n) k ∈ S.generate S" using nc by (rule S.generate_funpow)
  have powkSn: "S.power (ncycle n) k ∈ Sn n" using powk S.generate_subset_carrier by blast
  have conj: "S.power (ncycle n) k ∘ Transposition.transpose 0 1 ∘ S.inverse (S.power (ncycle n) k) ∈ S.generate S"
    using powk t01 by (meson S.generate.simps)
  have "S.inverse (S.power (ncycle n) k) = inv (ncycle n ^^ k)"
    using Sn_power_funpow powkSn Sn_inverse_eq by simp
  with conj Sn_power_funpow adjacent_transpose_conjug[OF assms(1,2)]
  show ?thesis by simp
qed

text ‹Building from adjacent transpositions, every transposition ‹transpose i j› with
  ‹i < j < n› lies in the subgroup.›
lemma transpose_extend:
  assumes "a ≠ b" "b ≠ c" "a ≠ c"
  shows "Transposition.transpose a c = Transposition.transpose a b ∘ Transposition.transpose b c ∘ Transposition.transpose a b"
  using assms by (simp add: transpose_comp_triple)

lemma all_transpose_in_generate_aux:
  assumes "1 < n"
  defines "S ≡ {Transposition.transpose 0 1, ncycle n}"
  shows "∀i. i + Suc d < n ⟶ Transposition.transpose i (i + Suc d) ∈ Group.generate (Sn n) (∘) id S"
proof (induction d)
  case 0
  show ?case
    unfolding S_def
    using adjacent_in_generate[OF _ assms(1)]
    by (metis One_nat_def Suc_eq_plus1 Suc_lessD mod_less)
next
  case (Suc d)
  show ?case
  proof (intro allI impI)
    fix i assume i: "i + Suc (Suc d) < n"
    let ?b = "i + Suc d" and ?c = "i + Suc (Suc d)"
    have §: "i + Suc d < n" using i by simp
    then have ib: "Transposition.transpose i ?b ∈ S.generate S"
      using Suc.IH unfolding S_def by blast
    have "?b mod n = ?b" "Suc ?b mod n = Suc ?b" using i by auto
    then have §: "Transposition.transpose ?b (Suc ?b) ∈ S.generate S"
      using adjacent_in_generate[OF _ assms(1)] unfolding S_def by (metis §)
    have "Transposition.transpose i ?c
            = Transposition.transpose i ?b ∘ Transposition.transpose ?b ?c ∘ Transposition.transpose i ?b"
      by (rule transpose_extend) auto
    with ib § show "Transposition.transpose i ?c ∈ S.generate S" 
      by (auto intro: S.generate.comp simp: o_assoc)
  qed
qed

lemma transpose_in_generate:
  assumes "a < n" "b < n" "1 < n"
  shows "Transposition.transpose a b ∈ Group.generate (Sn n) (∘) id {Transposition.transpose 0 1, ncycle n}"
proof (cases "a=b")
  case True
  then show ?thesis
    by (simp add: S.generate.unit)
next
  case False
  then show ?thesis
    using assms add_Suc_right less_natE all_transpose_in_generate_aux
    by (metis (no_types, lifting) linorder_not_le order_less_le transpose_commute) 
qed

text ‹The canonical generation theorem: a transposition of two adjacent points together with
  the standard @{term n}-cycle generate the whole symmetric group.›
theorem Sn_generated_canonical:
  assumes "1 < n"
  shows "Group.generate (Sn n) (∘) id {Transposition.transpose 0 1, ncycle n} = Sn n"
proof
  show "S.generate {Transposition.transpose 0 1, ncycle n} ⊆ Sn n"
    using S.generate_subset_carrier by simp
next
  have sub: "S.generate (transpositions n) ⊆ S.generate {Transposition.transpose 0 1, ncycle n}"
    using transpose_in_generate[OF _ _ assms] 
      by (intro S.generate_minimal S.generate_is_subgroup) (auto simp: transpositions_def)
  then show "Sn n ⊆ S.generate {Transposition.transpose 0 1, ncycle n}"
    using Sn_generated_by_transpositions by simp
qed


subsection ‹A transposition and a ‹p›-cycle generate ‹S⇩p› for prime ‹p››

text ‹For prime @{term p}, the standard @{term p}-cycle together with ∗‹any› transposition
  generates @{term "Sn p"}.  The primality is essential: it guarantees that the conjugates of
  the transposition by powers of the cycle have supports forming a single orbit covering all
  points, from which every transposition can be recovered.›

text ‹Conjugating @{term "transpose a b"} by the @{term k}-th power of the @{term n}-cycle
  shifts both points by @{term k} (modulo @{term n}); the result stays in the subgroup
  generated by the cycle and the transposition.›
lemma ncycle_conj_transpose_in_generate:
  assumes "a < n" "b < n" "1 < n"
  defines "S ≡ {ncycle n, Transposition.transpose a b}"
  shows "Transposition.transpose ((a + k) mod n) ((b + k) mod n) ∈ Group.generate (Sn n) (∘) id S"
proof -
  have tabSn: "Transposition.transpose a b ∈ Sn n"
    using assms by (auto simp: Sn_def permutes_swap_id)
  have tab: "Transposition.transpose a b ∈ S.generate S"
    using tabSn by (intro S.generate.incl) (simp add: S_def)
  have nc: "ncycle n ∈ S.generate S"
    using ncycle_in_Sn by (intro S.generate.incl) (simp add: S_def)
  have invk: "S.inverse (S.power (ncycle n) k) ∈ S.generate S"
    using nc by (intro S.generate.inv S.generate_funpow)
  have conj: "S.power (ncycle n) k ∘ Transposition.transpose a b ∘ S.inverse (S.power (ncycle n) k) ∈ S.generate S"
    by (simp add: S.generate.comp S.generate_funpow invk nc tab)
  have inveq: "S.inverse (S.power (ncycle n) k) = inv (ncycle n ^^ k)"
    using S.power_closed Sn_inverse_eq Sn_power_funpow ncycle_in_Sn by force
  have "ncycle n ^^ k ∘ Transposition.transpose a b ∘ inv (ncycle n ^^ k)
        = Transposition.transpose ((ncycle n ^^ k) a) ((ncycle n ^^ k) b)"
    using ncycle_bij by (intro transpose_conjug bij_fn)
  with ncycle_funpow [of _ n k] assms
  have "ncycle n ^^ k ∘ Transposition.transpose a b ∘ inv (ncycle n ^^ k)
        = Transposition.transpose ((a + k) mod n) ((b + k) mod n)"   by presburger
  with conj Sn_power_funpow inveq show ?thesis by simp
qed

text ‹If a subgroup contains two transpositions sharing a point, it contains their ``sum''.›
lemma transpose_chain:
  assumes H: "Subgroup H (Sn n) (∘) id"
    and "Transposition.transpose x y ∈ H"
    and "Transposition.transpose y z ∈ H"
    and "x ≠ z" "y ≠ z"
  shows "Transposition.transpose x z ∈ H"
proof -
  interpret H: Subgroup H "Sn n" "(∘)" id by (rule H)
  show ?thesis
    using assms by (metis H.sub_composition_closed transpose_comp_triple)
qed

end (* n::nat *)

context
  fixes p::nat
  assumes p: "prime p"

begin

interpretation G: Group "Sn p" "(∘)" id 
  by (rule Group_Sn)

lemma p_gt1: "1 < p" 
  using p by (simp add: prime_nat_iff)

text ‹Number-theoretic facts about the stride @{term d} (the gap of the transposition).›
lemma coprime_prime_stride:
  assumes "0 < d" "d < p"
  shows "coprime p d"
  by (simp add: assms nat_dvd_not_less p prime_imp_coprime)

lemma kd_mod_zero_iff:
  assumes "0 < d" "d < p"
  shows "(k * d) mod p = 0 ⟷ p dvd k"
  by (simp add: coprime_dvd_mult_left_iff coprime_prime_stride assms mod_eq_0_iff_dvd)

lemma stride_endpoints_distinct:
  assumes "0 < d" "d < p"
  shows "(k * d) mod p ≠ (Suc k * d) mod p"
    by (metis assms add_implies_diff le_add2 mod_eq_dvd_iff_nat mult_Suc nat_dvd_not_less)

text ‹Each ``stride edge'' ‹transpose (k * d mod p) (Suc k * d mod p)› lies in the subgroup
  generated by the cycle and @{term "transpose 0 d"}.›
lemma stride_edge:
  assumes d1: "0 < d" and d2: "d < p"
  defines "S ≡ {ncycle p, Transposition.transpose 0 d}"
  shows "Transposition.transpose ((k * d) mod p) ((Suc k * d) mod p) ∈ Group.generate (Sn p) (∘) id S"
    using S_def Symmetric_Generation.ncycle_conj_transpose_in_generate d2
    by (metis add_0 mult_Suc p prime_gt_0_nat prime_nat_iff)

text ‹Chaining the stride edges, every ‹transpose 0 (k * d mod p)› (for ‹k› not a
  multiple of @{term p}) lies in the subgroup.›
lemma stride_walk:
  fixes d :: nat
  assumes d1: "0 < d" and d2: "d < p"
  defines "S ≡ {ncycle p, Transposition.transpose 0 d}"
  shows "¬ p dvd k ⟹ Transposition.transpose 0 ((k * d) mod p) ∈ Group.generate (Sn p) (∘) id S"
proof (induction k)
  case 0
  then show ?case by simp
next
  case (Suc k)
  have edge: "Transposition.transpose ((k * d) mod p) ((Suc k * d) mod p) ∈ G.generate S"
    using stride_edge[OF d1 d2] unfolding S_def by blast
  have suc_ne0: "(Suc k * d) mod p ≠ 0"
    using Suc.prems d1 d2 kd_mod_zero_iff by blast
  show ?case
  proof (cases "p dvd k")
    case True
    then show ?thesis by (metis edge dvd_imp_mod_0 dvd_mult2)
  next
    case False
    have ih: "Transposition.transpose 0 ((k * d) mod p) ∈ G.generate S"
      using Suc.IH[OF False] unfolding S_def by blast
    have kne0: "(k * d) mod p ≠ 0"
      using False d1 d2 kd_mod_zero_iff by blast
    have ne: "(k * d) mod p ≠ (Suc k * d) mod p"
      using d1 d2 stride_endpoints_distinct by blast
    show ?thesis 
      using transpose_chain[OF G.generate_is_subgroup ih edge] kne0 suc_ne0 ne
      unfolding S_def by argo
  qed
qed

lemma pymod: "(p * y + 1) mod p = (1::nat) mod p"
  by (metis mod_mult_self3 mult.commute)

text ‹Since @{term d} is coprime to the prime @{term p}, some multiple of @{term d} is
  congruent to @{term 1}, so @{term "transpose 0 1"} is reached.›
lemma stride_reaches_one:
  fixes d :: nat
  assumes d1: "0 < d" and d2: "d < p"
  shows "∃k. (k * d) mod p = 1 ∧ ¬ p dvd k"
proof -
  have cop: "coprime d p" using coprime_prime_stride[OF d1 d2] by (simp add: coprime_commute)
  obtain x y where xy: "d * x = p * y + 1" using coprime_bezout_strong[OF cop] p_gt1 by auto
  have one: "(x * d) mod p = 1"
    by (metis mod_less mult.commute p_gt1 pymod xy)
  with one show ?thesis by auto
qed

lemma t01_in_stride_generate:
  assumes "0 < d" "d < p"
  shows "Transposition.transpose 0 1 ∈ Group.generate (Sn p) (∘) id {ncycle p, Transposition.transpose 0 d}"
  by (metis assms stride_reaches_one stride_walk)

text ‹The cycle and a stride-@{term d} transposition generate @{term "Sn p"}.›
theorem Sn_generated_cycle_transpose_0d:
  fixes d :: nat
  assumes d1: "0 < d" and d2: "d < p"
  shows "Group.generate (Sn p) (∘) id {ncycle p, Transposition.transpose 0 d} = Sn p"
proof
  have nc: "ncycle p ∈ G.generate {ncycle p, Transposition.transpose 0 d}"
    using ncycle_in_Sn by (intro G.generate.incl) simp
  have sub: "G.generate {Transposition.transpose 0 1, ncycle p} ⊆ G.generate {ncycle p, Transposition.transpose 0 d}"
    using t01_in_stride_generate[OF d1 d2] nc 
    by (intro G.generate_minimal G.generate_is_subgroup) auto
  then show "Sn p ⊆ G.generate {ncycle p, Transposition.transpose 0 d}"
    using Sn_generated_canonical[OF p_gt1] by simp
qed (use G.generate_subset_carrier in simp)

lemma sum_pa_bounds:
  fixes a b :: nat
  assumes "a < p" "b < p" "a ≠ b"
  shows "0 < (b + (p - a)) mod p"
proof (rule ccontr)
  have *: "0 < b + (p - a)" "b + (p - a) < 2 * p" "b + (p - a) ≠ p" using assms
    by auto
  assume "¬ 0 < (b + (p - a)) mod p"
  then obtain k where "b + (p - a) = p * k" by (auto simp: dvd_def)
  with * show False by auto
qed

text ‹The main result of this section: for prime @{term p}, the standard @{term p}-cycle and
  ∗‹any› transposition generate @{term "Sn p"}.›
theorem Sn_generated_ncycle_transpose:
  fixes a b :: nat
  assumes a: "a < p" and b: "b < p" and ab: "a ≠ b"
  shows "Group.generate (Sn p) (∘) id {ncycle p, Transposition.transpose a b} = Sn p"
proof
  define d where "d ≡ (b + (p - a)) mod p"
  obtain d: "0 < d" "d < p" unfolding d_def using p_gt1
    using a ab b sum_pa_bounds by (metis mod_less_divisor not_gr0 not_less0)
  ― ‹Conjugating @{term "transpose a b"} by @{term "ncycle p ^^ (p - a)"} maps @{term a} to
    @{term 0}, exhibiting @{term "transpose 0 d"} inside the subgroup.›
  have t0d: "Transposition.transpose 0 d ∈ G.generate {ncycle p, Transposition.transpose a b}"
    using ncycle_conj_transpose_in_generate[OF a b p_gt1, of "p - a"] a d_def by auto
  have nc: "ncycle p ∈ G.generate {ncycle p, Transposition.transpose a b}"
    using ncycle_in_Sn by (intro G.generate.incl) simp
  have sub: "G.generate {ncycle p, Transposition.transpose 0 d} ⊆ G.generate {ncycle p, Transposition.transpose a b}"
    using t0d nc by (intro G.generate_minimal G.generate_is_subgroup) auto
  then show "Sn p ⊆ G.generate {ncycle p, Transposition.transpose a b}"
    using Sn_generated_cycle_transpose_0d[OF d] by simp
qed (use G.generate_subset_carrier in simp)


subsection ‹An arbitrary cycle and transposition generate ‹S⇩p››

text ‹In @{term "Sn n"} the group conjugation specialises to the familiar
  @{term "g ∘ x ∘ inv g"}.›
lemma Sn_conjugation_eq:
  assumes g: "g ∈ Sn n" and x: "x ∈ Sn n"
  shows "Group.conjugation (Sn n) (∘) id g x = g ∘ x ∘ inv g"
  by (simp add: Group.conjugation_def Group_Sn Sn_inverse_eq g x)

text ‹Transporting @{thm [source] Sn_generated_ncycle_transpose} along conjugacy: for prime
  @{term p}, ∗‹any› conjugate @{term "q ∘ ncycle p ∘ inv q"} of the standard @{term p}-cycle,
  together with the conjugate @{term "q ∘ transpose a b ∘ inv q"} of a transposition, generates
  @{term "Sn p"}.›
lemma Sn_generated_conj_cycle_transpose:
  fixes q :: "nat ⇒ nat" and a b :: nat
  assumes q: "q ∈ Sn p" and a: "a < p" and b: "b < p" and ab: "a ≠ b"
  shows "Group.generate (Sn p) (∘) id
           {q ∘ ncycle p ∘ inv q, q ∘ Transposition.transpose a b ∘ inv q} = Sn p"
proof -
  interpret G: Group "Sn p" "(∘)" id by (rule Group_Sn)
  have qp: "q permutes {0..<p}" using q by (simp add: Sn_def)
  define S where "S = {ncycle p, Transposition.transpose a b}"
  have genS: "G.generate S = Sn p"
    unfolding S_def by (rule Sn_generated_ncycle_transpose[OF a b ab])
  have SsubSn: "S ⊆ Sn p"
    unfolding S_def using ncycle_in_Sn a b by (auto simp: Sn_def permutes_swap_id)
  have "G.generate {q ∘ ncycle p ∘ inv q, q ∘ Transposition.transpose a b ∘ inv q}
      = G.conjugation q ` G.generate S"
    using G.conjugation_generate_eq[OF q] G.conjugation_def S_def Sn_inverse_eq SsubSn q by force
  also have "… = Sn p" using G.conjugation_bij[OF q] by (simp add: genS bij_betw_imp_surj_on)
  finally show ?thesis .
qed


subsection ‹An order-‹p› element of ‹S⇩p› is a ‹p›-cycle›

text ‹The combinatorial counterpart of the previous result: every element of @{term "Sn p"}
  of order @{term p} (for @{term p} prime) is conjugate to the standard cycle, hence is itself
  a @{term p}-cycle.  Together with @{thm [source] Sn_generated_conj_cycle_transpose} this lets
  Cauchy's theorem (which only yields ∗‹some› order-@{term p} element) feed the generation
  argument for the quintic.›

text ‹Iterating @{term g} is periodic with period dividing @{term n} once @{term "g ^^ n = id"}.›
lemma funpow_mod_period:
  assumes "(g ^^ n) = id"
  shows "(g ^^ (k mod n)) = (g ^^ k)"
  by (metis (no_types, lifting) ext assms funpow_mod_eq id_apply)

text ‹If @{term g} has order @{term p} (prime) and moves @{term x}, then no smaller positive
  power fixes @{term x}: the only powers fixing @{term x} are the multiples of @{term p}.›
lemma cycle_period_prime:
  assumes p: "prime p" and gp: "(g ^^ p) = id" and gx: "g x ≠ x"
    and d: "(g ^^ d) x = x"
  shows "d mod p = 0"
proof (rule ccontr)
  assume "d mod p ≠ 0"
  have dmod: "(g ^^ (d mod p)) x = x"
    using funpow_mod_period[OF gp, of d] d by simp
  obtain k where k: "(k * (d mod p)) mod p = 1"
    using ‹d mod p ≠ 0› p stride_reaches_one
    by (meson mod_less_divisor not_gr_zero prime_gt_0_nat)
  then have "(g ^^ ((k * (d mod p)) mod p)) x = x"
    using funpow_mod_period[OF gp] by (metis dmod funpow_mod_eq mod_mult_self2_is_0 mod_self)
  with gx show False using k by simp
qed

text ‹The conjugator: the map sending @{term i} to @{term "(g ^^ i) x"} on @{term "{0..<p}"}
  and fixing the rest.›
definition qmap :: "(nat ⇒ nat) ⇒ nat ⇒ nat ⇒ nat"
  where "qmap g x i = (if i < p then (g ^^ i) x else i)"

context
  fixes g :: "nat ⇒ nat" and x :: nat
  assumes gSn: "g ∈ Sn p" and gp: "(g ^^ p) = id"
    and gx: "g x ≠ x" and xp: "x < p"
begin

lemma g_funpow_lt: "i < p ⟹ (g ^^ i) x < p"
  using gSn permutes_in_funpow_image xp by (fastforce simp: Sn_def permutes_funpow)

lemma qmap_inj_aux:
  assumes ij: "i < p" "j < p" "i ≤ j" and eq: "(g ^^ i) x = (g ^^ j) x"
  shows "i = j"
proof -
  have bij_i: "bij (g ^^ i)" using Sn_def gSn permutes_bij by fastforce
  have "(g ^^ i) x = (g ^^ i) ((g ^^ (j - i)) x)"
    by (metis Sn_iff bij_betw_def eq funpow_diff gSn ij(3) permutes_bij)
  then have "(j - i) mod p = 0" 
    using cycle_period_prime[OF p gp gx] by (simp add: bij_i bij_is_inj inj_eq)
  then show "i = j" using ij by auto
qed

lemma qmap_inj_on: "inj_on (qmap g x) {0..<p}"
proof (rule inj_onI)
  fix i j assume "i ∈ {0..<p}" "j ∈ {0..<p}" "qmap g x i = qmap g x j"
  then have "i < p" "j < p" "(g ^^ i) x = (g ^^ j) x"
    by (auto simp: qmap_def)
  then show "i = j"
    by (metis nat_le_linear qmap_inj_aux)
qed

lemma qmap_image: "qmap g x ` {0..<p} = {0..<p}"
proof (rule endo_inj_surj)
  show "finite {0..<p}" by simp
  show "qmap g x ` {0..<p} ⊆ {0..<p}" using g_funpow_lt by (auto simp: qmap_def)
  show "inj_on (qmap g x) {0..<p}" by (rule qmap_inj_on)
qed

lemma qmap_permutes: "qmap g x permutes {0..<p}"
  using qmap_inj_on qmap_image
  by (intro bij_imp_permutes) (auto simp: bij_betw_def qmap_def)

lemma qmap_in_Sn: "qmap g x ∈ Sn p"
  using qmap_permutes by (simp add: Sn_def)

lemma g_qmap_eq:
  assumes "i < p"
  shows "g (qmap g x i) = qmap g x (ncycle p i)"
  using funpow_mod_period[OF gp, of "Suc i"] assms by (simp add: qmap_def ncycle_def)

lemma g_comp_qmap: "g ∘ qmap g x = qmap g x ∘ ncycle p"
  using g_qmap_eq gSn by (auto simp: Sn_def permutes_def ncycle_def qmap_def)

lemma g_conj_ncycle: "g = qmap g x ∘ ncycle p ∘ inv (qmap g x)"
  by (metis comp_assoc comp_id g_comp_qmap permutes_inv_o(1) qmap_permutes)

end

theorem order_p_elt_conj_ncycle:
  fixes g :: "nat ⇒ nat"
  assumes gSn: "g ∈ Sn p" and gp: "(g ^^ p) = id" and gne: "g ≠ id"
  shows "∃q ∈ Sn p. g = q ∘ ncycle p ∘ inv q"
proof -
  obtain x where x: "g x ≠ x" using gne by (auto simp: fun_eq_iff)
  with gSn have xp: "x < p"
    by (auto simp: Sn_def permutes_def)
  show ?thesis
    using gSn g_conj_ncycle gp qmap_in_Sn x xp by blast
qed

text ‹The same conclusion phrased through the group's @{const Monoid.element_order}: an element
  of @{term "Sn p"} of order @{term p} is a conjugate of the standard cycle.›
theorem order_p_elt_conj_ncycle_order:
  fixes g :: "nat ⇒ nat"
  assumes gSn: "g ∈ Sn p"
    and ord: "Monoid.element_order (∘) id g = p"
  shows "∃q ∈ Sn p. g = q ∘ ncycle p ∘ inv q"
proof -
  have gp: "(g ^^ p) = id"
    using G.power_element_order Sn_power_funpow finite_Sn gSn ord by force
  have gne: "g ≠ id"
    using ord p by force
  show ?thesis by (rule order_p_elt_conj_ncycle[OF gSn gp gne])
qed

end (* p::nat *)

end