Theory Group_Operations

theory Group_Operations
  imports Group_Theory "HOL-Computational_Algebra.Primes"
begin

section ‹Group Actions›

text ‹This theory formalises group actions with respect to the locale-based group
  infrastructure of @{text Group_Theory}, following the same development as
  @{text GroupAction.thy} (which uses the record-based groups of HOL-Algebra).

  A group action of a group $(G, \cdot, 1)$ on a set $S$ is given by a group
  homomorphism $\varphi : G \to \operatorname{Sym}(S)$, where $\operatorname{Sym}(S)$
  is the symmetric group on $S$ (i.e.\ the group of bijections $S \to S$).›


subsection ‹Definition and Basic Properties›

locale Group_Action =
  grp: Group G "(⋅)" 𝟭 + transformations S
  for G and composition (infixl ‹⋅› 70) and unit (‹𝟭›) and φ and S +
  assumes hom_closed: "g ∈ G ⟹ φ g ∈ Sym"
    and hom_compose: "⟦ g ∈ G; h ∈ G ⟧ ⟹ φ (g ⋅ h) = compose S (φ g) (φ h)"
    and hom_unit: "φ 𝟭 = identity S"

begin

sublocale coset_notation .

text ‹The action of @{term 𝟭} has no effect.›

lemma one_is_id [simp]:
  assumes "s ∈ S"
  shows "φ 𝟭 s = s"
  using assms hom_unit by simp

text ‹The action maps @{term S} to itself.›

lemma action_closed [intro, simp]:
  assumes "g ∈ G" "s ∈ S"
  shows "φ g s ∈ S"
  using assms hom_closed Units_bij_betwI by (meson bij_betwE)

text ‹The image of any group element is a bijection on @{term S}.›

lemma images_are_bij:
  assumes "g ∈ G"
  shows "bij_betw (φ g) S S"
  using assms hom_closed by auto

text ‹The action respects group multiplication.›

lemma action_mult:
  assumes "g ∈ G" "h ∈ G" "s ∈ S"
  shows "φ g (φ h s) = φ (g ⋅ h) s"
  using assms hom_compose by (simp add: compose_eq)

text ‹The action of @{term "grp.inverse g"} reverts the action of @{term g}.›

lemma group_inv_rel:
  assumes "g ∈ G" "t ∈ S" "φ g t = s"
  shows "φ (grp.inverse g) s = t"
  using action_mult assms by force

lemma action_inverse:
  assumes "g ∈ G" "s ∈ S"
  shows "φ (grp.inverse g) (φ g s) = s"
  using assms action_closed group_inv_rel by blast


subsection ‹Stabilizer›

text ‹The stabilizer of a point @{term "s ∈ S"} is the set of group elements
  that fix @{term s} under the action.›

definition stabilizer
  where "stabilizer s = {g ∈ G. φ g s = s}"


text ‹The stabilizer of any point in @{term S} is a subgroup of @{term G}.›

theorem stabilizer_subgroup:
  assumes "s ∈ S"
  shows "Subgroup (stabilizer s) G (⋅) 𝟭"
proof (rule grp.subgroupI)
  fix g h
  assume "g ∈ stabilizer s" "h ∈ stabilizer s"
  then show "g ⋅ h ∈ stabilizer s"
    using action_mult assms stabilizer_def by force
qed (auto simp: assms group_inv_rel stabilizer_def)

subsection ‹Fixed Points›

text ‹The fixed points of a group action are those elements of @{term S} that
  are fixed by every group element.  Equivalently, a point is fixed if and only
  if its stabilizer is the whole group.›

definition fixed_points
  where "fixed_points = {s ∈ S. G ⊆ stabilizer s}"

lemma fixed_points_subset: "fixed_points ⊆ S"
  unfolding fixed_points_def by auto

lemma fixed_point_char:
  assumes "s ∈ S"
  shows "s ∈ fixed_points ⟷ (∀g ∈ G. φ g s = s)"
  unfolding fixed_points_def stabilizer_def using assms by auto

lemma fixed_pointI:
  assumes "s ∈ S" "⋀g. g ∈ G ⟹ φ g s = s"
  shows "s ∈ fixed_points"
  using assms fixed_point_char by auto

lemma fixed_pointD:
  assumes "s ∈ fixed_points" "g ∈ G"
  shows "φ g s = s"
  using assms unfolding fixed_points_def stabilizer_def by auto

text ‹A point is fixed if and only if its stabilizer is the whole group.›

lemma fixed_point_stabilizer:
  assumes "s ∈ S"
  shows "s ∈ fixed_points ⟷ stabilizer s = G"
  using assms fixed_points_def stabilizer_def by auto


subsection ‹Orbits›

text ‹The orbit of a point @{term "s ∈ S"} under the group action is the set
  of all images of @{term s} under group elements.›

definition orbit
  where "orbit s ≡ {φ g s | g. g ∈ G}"

lemma orbit_eq: "orbit s = (λg. φ g s) ` G"
  by (auto simp: orbit_def)

lemma orbit_subset:
  assumes "s ∈ S"
  shows "orbit s ⊆ S"
  unfolding orbit_def using assms by auto

lemma orbit_self:
  assumes "s ∈ S"
  shows "s ∈ orbit s"
  unfolding orbit_def using assms grp.unit_closed by force

lemma orbit_mem_iff:
  assumes "s ∈ S"
  shows "t ∈ orbit s ⟷ (∃g ∈ G. φ g s = t)"
  unfolding orbit_def by auto

lemma orbit_memI:
  assumes "g ∈ G"
  shows "φ g s ∈ orbit s"
  unfolding orbit_def using assms by auto

lemma orbit_memE:
  assumes "t ∈ orbit s"
  obtains g where "g ∈ G" "φ g s = t"
  using assms unfolding orbit_def by auto

lemma orbit_nonempty: "orbit s ≠ {}"
  using orbit_memI by auto

text ‹A point is fixed precisely when its orbit is the singleton containing it.›

lemma fixed_point_iff_orbit_singleton:
  assumes "s ∈ S"
  shows "s ∈ fixed_points ⟷ orbit s = {s}"
proof
  assume fixed: "s ∈ fixed_points"
  show "orbit s = {s}"
  proof (rule set_eqI)
    fix t
    show "t ∈ orbit s ⟷ t ∈ {s}"
    proof
      assume "t ∈ orbit s"
      then obtain g where "g ∈ G" "φ g s = t" by (rule orbit_memE)
      then show "t ∈ {s}" using fixed fixed_pointD by simp
    next
      assume "t ∈ {s}"
      then show "t ∈ orbit s" using assms orbit_self by simp
    qed
  qed
next
  assume orbit: "orbit s = {s}"
  show "s ∈ fixed_points"
  proof (rule fixed_pointI[OF assms])
    fix g assume "g ∈ G"
    then have "φ g s ∈ orbit s" by (rule orbit_memI)
    then show "φ g s = s" by (simp add: orbit)
  qed
qed

lemma card_orbit_gt0I: "finite G ⟹ card (orbit s) > 0"
  by (metis card_gt_0_iff finite_imageI orbit_eq orbit_nonempty)

subsection ‹The Orbit-Stabilizer Theorem›

text ‹Two group elements give the same image under the action if and only if
  they lie in the same right coset of the stabilizer.›

lemma same_orbit_iff_same_coset:
  assumes "s ∈ S" "g ∈ G" "h ∈ G"
  shows "φ g s = φ h s ⟷ grp.inverse g ⋅ h ∈ stabilizer s"
proof
  assume "φ g s = φ h s"
  then show "grp.inverse g ⋅ h ∈ stabilizer s"
    using assms Group_Action.action_mult Group_Action_axioms action_inverse
      by (fastforce simp: invertible_inverse_closed stabilizer_def)
next
  assume mem: "grp.inverse g ⋅ h ∈ stabilizer s"
  then have "φ g (φ (grp.inverse g) (φ h s)) = φ g s"
    using assms by (simp add: action_mult stabilizer_def)
  then show "φ g s = φ h s"
    using assms by (simp add: action_mult grp.invertible_right_inverse2)
qed

text ‹The orbit-stabilizer theorem.  The map @{term "λg. φ g s"} from
  @{term G} to @{term "orbit s"} is surjective, and its fibers are exactly
  the left cosets of the stabilizer.  Hence the number of distinct images
  equals the index of the stabilizer, and Lagrange's theorem gives the
  cardinality form.›

text ‹Every left coset of the stabilizer has the same cardinality as the
  stabilizer itself.›

lemma coset_fiber:
  assumes s: "s ∈ S" and g: "g ∈ G"
  shows "{h ∈ G. φ h s = φ g s} = g ⋅| stabilizer s"
proof (rule set_eqI)
  fix h
  show "(h ∈ {h ∈ G. φ h s = φ g s}) = (h ∈ g ⋅| stabilizer s)"
  proof
    assume h: "h ∈ {h ∈ G. φ h s = φ g s}"
    then have hG: "h ∈ G" and eq: "φ h s = φ g s" by auto
    from same_orbit_iff_same_coset [OF s g hG] eq
    have "grp.inverse g ⋅ h ∈ stabilizer s" by simp
    then show "h ∈ g ⋅| stabilizer s"
      by (simp add: g grp.invertible_right_inverse2 hG rev_image_eqI Left_Coset_def)
  next
    assume h: "h ∈ g ⋅| stabilizer s"
    then obtain t where t: "t ∈ stabilizer s" and ht: "h = g ⋅ t"
      unfolding Left_Coset_def by auto
    from t have tG: "t ∈ G" and ts: "φ t s = s"
      unfolding stabilizer_def by auto
    have hG: "h ∈ G" using ht g tG by auto
    then show "h ∈ {h ∈ G. φ h s = φ g s}"
      using action_mult g ht s tG ts by fastforce
  qed
qed

text ‹The orbit-stabilizer theorem (bijection form).  The map that sends each
  orbit element to its fiber under @{term "λg. φ g s"} is a bijection from
  @{term "orbit s"} to the set of left cosets of the stabilizer.›

theorem orbit_stabilizer_bij:
  assumes "s ∈ S"
  shows "bij_betw (λt. {g ∈ G. φ g s = t}) (orbit s) ((λg. g ⋅| stabilizer s) ` G)"
  using coset_fiber assms
  by (auto simp: bij_betw_def inj_on_def orbit_def)

text ‹The orbit-stabilizer theorem (cardinality form).›

theorem orbit_stabilizer_card:
  assumes s: "s ∈ S" and fin: "finite G"
  shows "card G = card (orbit s) * card (stabilizer s)"
proof -
  let ?f = "λg. φ g s"
  have surj: "?f ` G = orbit s"
    unfolding orbit_def by auto
  have fibers: "⋀g. g ∈ G ⟹ {h ∈ G. ?f h = ?f g} = g ⋅| stabilizer s"
    using coset_fiber [OF s] by auto
  have fiber_card: "card {h ∈ G. ?f h = ?f g} = card (stabilizer s)"
    if g: "g ∈ G" for g
  proof -
    have §: "bij_betw ((⋅) g) (stabilizer s) (g ⋅| stabilizer s)"
      using that by (auto simp: bij_betw_def inj_on_def stabilizer_def)
    have "card {h ∈ G. ?f h = ?f g} = card (g ⋅| stabilizer s)"
      using fibers [OF that] by simp
    also have "… = card (stabilizer s)"
      using § by (simp add: bij_betw_same_card)
    finally show ?thesis
      by presburger
  qed
  have decomp: "G = (⋃t ∈ orbit s. {g ∈ G. ?f g = t})"
    using surj by auto
  have disj: "⋀t1 t2. ⟦ t1 ∈ orbit s; t2 ∈ orbit s; t1 ≠ t2 ⟧
    ⟹ {g ∈ G. ?f g = t1} ∩ {g ∈ G. ?f g = t2} = {}"
    by auto
  have fin_orbit: "finite (orbit s)"
    using fin surj by (metis finite_imageI)
  have "card G = card (⋃t ∈ orbit s. {g ∈ G. ?f g = t})"
    using decomp by simp
  also have "… = (∑t ∈ orbit s. card {g ∈ G. ?f g = t})"
    using fin fin_orbit disj by (intro card_UN_disjoint) auto
  also have "… = (∑t ∈ orbit s. card (stabilizer s))"
    using fiber_card
    by (intro sum.cong; force simp: orbit_def)
  also have "… = card (orbit s) * card (stabilizer s)"
    by simp
  finally show ?thesis .
qed


subsection ‹Connection to Transformation Groups›

text ‹The image @{term "φ ` G"} is a subgroup of the symmetric group on @{term S},
  and therefore forms a transformation group.  This connects the orbit defined
  here with the orbit equivalence relation of @{locale transformation_group}.›

lemma image_is_subgroup: "Subgroup (φ ` G) Sym (compose S) (identity S)"
proof (rule symmetric.subgroupI)
  show "φ ` G ⊆ Sym"
    using hom_closed by auto
next
  show "identity S ∈ φ ` G"
    using hom_unit grp.unit_closed by (metis image_eqI)
next
  fix g h
  assume "g ∈ φ ` G" "h ∈ φ ` G"
  then obtain a b where "a ∈ G" "g = φ a" "b ∈ G" "h = φ b" by auto
  then show "compose S g h ∈ φ ` G"
    using hom_compose by (metis grp.composition_closed image_eqI)
next
  fix g
  assume "g ∈ φ ` G"
  then obtain a where a: "a ∈ G" "g = φ a" by auto
  show "⋀g. g ∈ φ ` G ⟹ symmetric.invertible g"
    using hom_closed by blast
  have inv_eq: "inverse (φ a) = φ (grp.inverse a)"
  proof (intro inverse_equality)
    show "compose S (φ a) (φ (grp.inverse a)) = identity S"
         "compose S (φ (grp.inverse a)) (φ a) = identity S"
      using ‹a ∈ G› hom_compose [symmetric] hom_unit by auto
  qed (use ‹a ∈ G› hom_closed Units_bijective in blast)+
  have "symmetric.inverse g ∈ S →⇩E S"
    by (metis a hom_closed mem_UnitsD symmetric.invertible symmetric.invertible_inverse_closed)
  then have "inverse (φ a) = symmetric.inverse g"
    using ‹a ∈ G› ‹g = φ a› hom_closed
    by (metis (no_types, lifting) inverse_equality mem_UnitsD symmetric.invertible
        symmetric.invertible_left_inverse symmetric.invertible_right_inverse)
  then show "symmetric.inverse g ∈ φ ` G"
    by (metis ‹a ∈ G› grp.invertible grp.invertible_inverse_closed image_iff inv_eq)
qed

sublocale tg: transformation_group "φ ` G" S
  using image_is_subgroup transformation_group_def by blast

lemma orbit_eq_Class:
  assumes "s ∈ S"
  shows "orbit s = tg.orbit.Class s"
  using assms tg.orbit_equality by (auto simp: orbit_def)


subsection ‹The permutation representation›

text ‹
  A group action is, by definition, a homomorphism into the symmetric group on @{term S}.
  We make this explicit, identify its kernel with the set of elements acting trivially on
  every point, and deduce that a ∗‹faithful› action embeds the group as a subgroup of the
  symmetric group: the permutation representation.  This is what turns an action on a
  finite set into a concrete subgroup of permutations (e.g.\ a Galois group acting on the
  roots of a polynomial becomes a subgroup of @{term "Sym"} of the root set).
›

text ‹The action, restricted to @{term G} for extensionality, is a group homomorphism into the
  symmetric group.›
interpretation action_hom:
  group_homomorphism "restrict φ G" G "(⋅)" 𝟭 Sym "compose S" "identity S"
proof 
  show "restrict φ G ∈ G →⇩E Sym" using hom_closed by auto
next
  fix x y assume "x ∈ G" "y ∈ G"
  then show "restrict φ G (x ⋅ y) = compose S (restrict φ G x) (restrict φ G y)"
    by (simp add: hom_compose)
next
  show "restrict φ G 𝟭 = identity S" by (simp add: hom_unit)
qed

text ‹On @{term S}, the image of a group element is the identity exactly when it fixes every
  point.›
lemma phi_eq_identity_iff:
  assumes "g ∈ G"
  shows "φ g = identity S ⟷ (∀s ∈ S. φ g s = s)"
  using assms by auto

text ‹The kernel of the permutation representation is the set of group elements that fix every
  point of @{term S}, i.e.\ the intersection of all the stabilizers.›
lemma action_kernel_eq:
  "group_homomorphism.Ker (restrict φ G) G (identity S) = {g ∈ G. ∀s ∈ S. φ g s = s}"
proof -
  show ?thesis
    using action_hom.Ker_image by (auto simp: phi_eq_identity_iff)
qed

text ‹An action is ∗‹faithful› if only the unit acts trivially on all of @{term S}.›
definition faithful
  where "faithful ⟷ (∀g ∈ G. (∀s ∈ S. φ g s = s) ⟶ g = 𝟭)"

lemma faithful_iff_kernel_trivial:
  "faithful ⟷ group_homomorphism.Ker (restrict φ G) G (identity S) = {𝟭}"
proof -
  have ker: "action_hom.Ker = {g ∈ G. ∀s ∈ S. φ g s = s}" by (rule action_kernel_eq)
  have one_in: "𝟭 ∈ action_hom.Ker" unfolding ker by simp
  show ?thesis
  proof
    assume faithful
    then have "action_hom.Ker ⊆ {𝟭}" unfolding ker faithful_def by blast
    with one_in show "action_hom.Ker = {𝟭}" by blast
  next
    assume "action_hom.Ker = {𝟭}"
    then show faithful unfolding faithful_def using ker by blast
  qed
qed

text ‹A faithful action is injective.›
lemma faithful_inj:
  assumes faithful
  shows "inj_on (restrict φ G) G"
  using action_hom.injective_iff_kernel_unit assms faithful_iff_kernel_trivial
  by force

text ‹The permutation representation of a faithful action is a group isomorphism onto its
  image, exhibiting @{term G} as a subgroup of the symmetric group on @{term S}.›
theorem faithful_action_embeds:
  assumes faithful
  shows "group_isomorphism (restrict φ G) G (⋅) 𝟭 (φ ` G) (compose S) (identity S)"
proof
  show "bij_betw (restrict φ G) G (φ ` G)"
    using assms bij_betw_def faithful_inj by auto
qed (auto simp: hom_closed hom_unit hom_compose)


subsection ‹Orbit Partition›

text ‹The orbits of a group action partition @{term S}.  Using the connection to
  @{locale transformation_group}, these facts follow from the general theory of
  equivalence relations.›

text ‹If @{term t} is in the orbit of @{term s}, then @{term s} is in the orbit of @{term t}.›

lemma orbit_symmetric:
  assumes "s ∈ S" "t ∈ orbit s"
  shows "s ∈ orbit t"
proof -
  from assms have "t ∈ tg.orbit.Class s"
    by (simp add: orbit_eq_Class)
  then have "(t, s) ∈ tg.Orbit_Relation"
    using assms(1) by auto
  then have "(s, t) ∈ tg.Orbit_Relation"
    by (rule tg.orbit.symmetric)
  then show "s ∈ orbit t"
    using orbit_eq_Class by blast
qed

text ‹If @{term t} is in the orbit of @{term s}, the two orbits are equal.›

lemma orbit_subset_mem:
  assumes "s ∈ S" "t ∈ orbit s"
  shows "orbit t ⊆ orbit s"
  using action_mult assms orbit_mem_iff by fastforce

lemma orbit_eq_mem:
  assumes "s ∈ S" "t ∈ orbit s"
  shows "orbit t = orbit s"
  by (meson antisym assms orbit_subset_mem orbit_subset orbit_symmetric subsetD)

text ‹Two orbits are either equal or disjoint.›

lemma orbit_disjoint:
  assumes "s ∈ S" "t ∈ S" "orbit s ≠ orbit t"
  shows "orbit s ∩ orbit t = {}"
  by (metis Int_emptyI assms orbit_eq_mem)

text ‹The set of all orbits.›

definition orbits :: "'b set set"
  where "orbits = orbit ` S"

lemma orbits_coverI:
  assumes "s ∈ S"
  shows "orbit s ∈ orbits"
  using assms unfolding orbits_def by auto

lemma orbits_coverE:
  assumes "X ∈ orbits"
  obtains s where "s ∈ S" "X = orbit s"
  using assms unfolding orbits_def by auto

text ‹The orbits cover @{term S}.›

lemma orbits_cover: "⋃ orbits = S"
  by (simp add: orbit_eq_Class orbits_def)

text ‹The orbits are pairwise disjoint.›

lemma orbits_disjoint: "disjoint orbits"
  by (simp add: disjnt_def orbit_disjoint orbits_def pairwise_imageI)

text ‹The nontrivial orbits are the orbits containing more than one point.›

definition nontrivial_orbits :: "'b set set"
  where "nontrivial_orbits = {X ∈ orbits. ¬ is_singleton X}"

lemma nontrivial_orbits_subset: "nontrivial_orbits ⊆ orbits"
  by (auto simp: nontrivial_orbits_def)

text ‹The nontrivial orbits cover exactly the points that are not fixed.›

lemma nontrivial_orbits_cover:
  "⋃ nontrivial_orbits = S - fixed_points"
proof (rule set_eqI)
  fix x
  show "x ∈ ⋃ nontrivial_orbits ⟷ x ∈ S - fixed_points"
  proof
    assume "x ∈ ⋃ nontrivial_orbits"
    then obtain X where X: "X ∈ nontrivial_orbits" "x ∈ X" by auto
    then obtain s where s: "s ∈ S" "X = orbit s"
      using nontrivial_orbits_def orbits_coverE by auto
    have xS: "x ∈ S" using X s orbit_subset by auto
    have "orbit x = X" using orbit_eq_mem[OF s(1)] X(2) s(2) by simp
    moreover have "¬ is_singleton X" using X by (simp add: nontrivial_orbits_def)
    ultimately have "x ∉ fixed_points"
      using fixed_point_iff_orbit_singleton[OF xS] by (auto simp: is_singleton_def)
    with xS show "x ∈ S - fixed_points" by simp
  next
    assume x: "x ∈ S - fixed_points"
    have xS: "x ∈ S" using x by simp
    have "orbit x ≠ {x}"
      using fixed_point_iff_orbit_singleton[of x] x by simp
    then have "¬ is_singleton (orbit x)"
      using orbit_self[OF xS] by (auto simp: is_singleton_def)
    then have "orbit x ∈ nontrivial_orbits"
      using x orbits_coverI by (simp add: nontrivial_orbits_def)
    then show "x ∈ ⋃ nontrivial_orbits" using x orbit_self by auto
  qed
qed

text ‹Cardinality of @{term S} as a sum over orbits.›

lemma card_S_sum_orbits:
  assumes "finite S"
  shows "card S = (∑X ∈ orbits. card X)"
proof -
  have "card (⋃ orbits) = (∑X ∈ orbits. card X)"
  proof (rule card_Union_disjoint)
    show "disjoint orbits" by (rule orbits_disjoint)
    show "⋀A. A ∈ orbits ⟹ finite A"
      by (metis Union_upper assms orbits_cover rev_finite_subset)
  qed
  then show ?thesis by (simp add: orbits_cover)
qed

text ‹Splitting the orbit partition into fixed points and nontrivial orbits gives the
  fixed-point form of the class equation.›

lemma fixed_point_class_equation:
  assumes fin: "finite S"
  shows "card S = card fixed_points + (∑X ∈ nontrivial_orbits. card X)"
proof -
  have card_nontrivial:
      "card (⋃ nontrivial_orbits) = (∑X ∈ nontrivial_orbits. card X)"
  proof (rule card_Union_disjoint)
    show "disjoint nontrivial_orbits"
      using orbits_disjoint nontrivial_orbits_subset
      by (auto simp: disjoint_def)
    show "⋀X. X ∈ nontrivial_orbits ⟹ finite X"
    proof -
      fix X assume "X ∈ nontrivial_orbits"
      then obtain s where "s ∈ S" "X = orbit s"
        using nontrivial_orbits_def orbits_coverE by auto
      then show "finite X"
        using orbit_subset[OF ‹s ∈ S›] fin by (meson finite_subset)
    qed
  qed
  have fin_fixed: "finite fixed_points"
    using fixed_points_subset fin by (rule finite_subset)
  have fin_nonfixed: "finite (S - fixed_points)" using fin by simp
  have split: "fixed_points ∪ (S - fixed_points) = S"
    using fixed_points_subset by auto
  have "card S = card fixed_points + card (S - fixed_points)"
    using card_Un_disjoint[OF fin_fixed fin_nonfixed] split by simp
  also have "… = card fixed_points + card (⋃ nontrivial_orbits)"
    by (simp add: nontrivial_orbits_cover)
  also have "… = card fixed_points + (∑X ∈ nontrivial_orbits. card X)"
    by (simp add: card_nontrivial)
  finally show ?thesis .
qed

text ‹If every nontrivial orbit has cardinality divisible by @{term k}, then the same is true
  of the set of non-fixed points.  This is the divisibility form of the fixed-point congruence.›

lemma dvd_card_nonfixed_points:
  assumes fin: "finite S"
    and dvd: "⋀s. ⟦s ∈ S; s ∉ fixed_points⟧ ⟹ k dvd card (orbit s)"
  shows "k dvd card (S - fixed_points)"
proof -
  have "k dvd card (⋃ nontrivial_orbits)"
  proof (intro dvd_partition strip)
    show "finite (⋃ nontrivial_orbits)"
      using fin nontrivial_orbits_cover by simp
    show "k dvd card X" if X: "X ∈ nontrivial_orbits" for X
    proof -
      obtain s where s: "s ∈ S" "X = orbit s"
        using X nontrivial_orbits_def orbits_coverE by auto
      have "s ∉ fixed_points"
        using X s fixed_point_iff_orbit_singleton[OF s(1)]
        by (auto simp: nontrivial_orbits_def)
      then show ?thesis using dvd[OF s(1)] s(2) by simp
    qed
  qed (use orbits_disjoint nontrivial_orbits_subset in ‹auto simp: disjoint_def›)
  then show ?thesis by (simp add: nontrivial_orbits_cover)
qed

text ‹If @{term k} divides the cardinality of every orbit, then @{term k} divides
  @{term "card S"}.›

lemma dvd_orbits_dvd_S:
  assumes "finite S" "⋀X. X ∈ orbits ⟹ k dvd card X"
  shows "k dvd card S"
proof -
  have "k dvd card (⋃ orbits)"
    using orbits_disjoint unfolding disjoint_def
    by (metis assms dvd_partition orbits_cover)
  then show ?thesis by (simp add: orbits_cover)
qed


end

section ‹Sylow's Theorem›

context Monoid
begin

definition power :: "'a ⇒ nat ⇒ 'a"
  where "power a n ≡ (((⋅) a)^^ n) 𝟭"

definition element_order :: "'a ⇒ nat"
  where "element_order a ≡ (LEAST n. n > 0 ∧ power a n = 𝟭)"

lemma power_0 [simp]: "power a 0 = 𝟭"
  by (simp add: power_def)

lemma power_Suc [simp]: "power a (Suc n) = a ⋅ power a n"
  by (simp add: power_def)

lemma power_1 [simp]: "a ∈ M ⟹ power a 1 = a"
  by simp

lemma power_closed [intro, simp]: "a ∈ M ⟹ power a n ∈ M"
  by (induction n) auto

lemma power_add: "a ∈ M ⟹ power a (m + n) = power a m ⋅ power a n"
  by (induction m) (simp_all add: associative)

lemma power_mult: "a ∈ M ⟹ power a (m * n) = power (power a m) n"
  by (induction n) (simp_all add: power_add)

lemma power_unit [simp]: "power 𝟭 n = 𝟭"
  by (induction n) simp_all

lemma power_Suc_right: "a ∈ M ⟹ power a (Suc n) = power a n ⋅ a"
proof (induction n)
  case 0
  then show ?case by simp
next
  case (Suc n) then show ?case
    using Suc_eq_plus1 local.power_add power_1 by presburger
qed

lemma power_commutes: "a ∈ M ⟹ a ⋅ power a n = power a n ⋅ a"
  by (metis power_Suc power_Suc_right)

lemma power_commutes_power:
  "a ∈ M ⟹ power a m ⋅ power a n = power a n ⋅ power a m"
  by (simp add: power_add[symmetric] add.commute)

lemma element_order_unit [simp]: "element_order 𝟭 = 1"
  unfolding element_order_def by (rule Least_equality) auto

end

context Group begin

lemma power_inverse:
  assumes "g ∈ G"
  shows "power (inverse g) n = inverse (power g n)"
proof (induction n)
  case 0
  then show ?case by simp
next
  case (Suc n)
  have "inverse g ⋅ inverse (power g n) = inverse (power g n) ⋅ inverse g"
    using power_commutes[of "inverse g" n] assms Suc by simp
  then have "power (inverse g) (Suc n) = inverse (power g n) ⋅ inverse g"
    using Suc by simp
  also have "… = inverse (power g (Suc n))"
    using inverse_composition_commute[of g "power g n"] assms by simp
  finally show ?case .
qed

lemma finite_power_order_exists:
  assumes "finite G" "g ∈ G"
  shows "∃n>0. power g n = 𝟭"
proof -
  have False if "inj_on (power g) {..card G}"
  proof -
    have "card (power g ` {..card G}) = Suc (card G)"
      by (simp add: card_image that) 
    then show False
      using card_mono assms by (metis Suc_n_not_le_n imageE power_closed subsetI)
  qed
  then obtain i j where "i ≤ card G" "j ≤ card G" "i < j" and ij_eq: "power g i = power g j"
    by (metis (mono_tags, opaque_lifting) inj_on_def linorder_cases atMost_iff)
  then have "j = i + (j - i)" by simp
  then have eq: "power g j = power g i ⋅ power g (j - i)"
    using power_add assms(2) by metis
  have "power g (j - i) = 𝟭"
    by (metis Monoid.invertible_left_cancel Monoid_axioms assms(2) eq ij_eq invertible
        power_closed right_unit unit_closed)
  with ‹i < j› show ?thesis by (intro exI[of _ "j - i"]) auto
qed

lemma element_order_pos:
  assumes "finite G" "g ∈ G"
  shows "element_order g > 0"
proof -
  obtain n where "n > 0" "power g n = 𝟭"
    using finite_power_order_exists[OF assms] by auto
  then show ?thesis
    unfolding element_order_def using LeastI[of "λn. n > 0 ∧ power g n = 𝟭" n] by auto
qed

lemma power_element_order:
  assumes "finite G" "g ∈ G"
  shows "power g (element_order g) = 𝟭"
proof -
  obtain n where "n > 0" "power g n = 𝟭"
    using finite_power_order_exists[OF assms] by auto
  then show ?thesis
    unfolding element_order_def using LeastI[of "λn. n > 0 ∧ power g n = 𝟭" n] 
    by auto
qed

lemma element_order_minimal:
  assumes "finite G" "g ∈ G" "n > 0" "power g n = 𝟭"
  shows "element_order g ≤ n"
  unfolding element_order_def by (rule Least_le) (use assms in auto)

lemma element_order_dvd:
  assumes "finite G" "g ∈ G" "power g n = 𝟭"
  shows "element_order g dvd n"
proof (rule ccontr)
  assume ndvd: "¬ element_order g dvd n"
  have ord_pos: "element_order g > 0"
    using element_order_pos[OF assms(1,2)] .
  have mod_pos: "n mod element_order g > 0"
    using ndvd ord_pos by (metis dvd_eq_mod_eq_0 gr0I)
  have "power g n = power g (element_order g * (n div element_order g) + n mod element_order g)"
    by simp
  also have "… = power g (element_order g * (n div element_order g)) ⋅ power g (n mod element_order g)"
    using assms(2) power_add by blast
  also have "power g (element_order g * (n div element_order g)) = power (power g (element_order g)) (n div element_order g)"
    using assms(2) power_mult by blast
  also have "… = power 𝟭 (n div element_order g)"
    using power_element_order[OF assms(1,2)] by simp
  also have "… = 𝟭" by simp
  finally have "power g (n mod element_order g) = 𝟭"
    using assms by simp
  moreover have "n mod element_order g < element_order g"
    using ord_pos by simp
  ultimately show False
    using element_order_minimal[OF assms(1,2) mod_pos] by linarith
qed

lemma power_mod_order:
  assumes "finite G" "g ∈ G"
  shows "power g n = power g (n mod element_order g)"
proof -
  have "n = element_order g * (n div element_order g) + n mod element_order g"
    by simp
  then have "power g n = power g (element_order g * (n div element_order g)) ⋅ power g (n mod element_order g)"
    using assms(2) power_add by metis
  also have "power g (element_order g * (n div element_order g)) = power (power g (element_order g)) (n div element_order g)"
    using assms(2) power_mult by blast
  also have "… = 𝟭"
    using power_element_order[OF assms] by simp
  finally show ?thesis using assms(2) by simp
qed

lemma power_eq_order_False:
  assumes "finite G" "g ∈ G"
    and "i < j" "j < element_order g"
    and "power g i = power g j"
  shows False
proof -
  from ‹i < j› have "j = i + (j - i)" by simp
  then have "power g j = power g i ⋅ power g (j - i)"
    using power_add ‹g ∈ G› by metis
  with assms(5) have "power g i = power g i ⋅ power g (j - i)" by simp
  then have "power g (j - i) = 𝟭"
    using ‹g ∈ G›
    by (metis invertible invertible_left_inverse invertible_left_inverse2 power_closed)
  moreover from assms have "0 < j - i" "j - i < element_order g" by auto
  ultimately show False
    using assms element_order_dvd nat_dvd_not_less by blast
qed

lemma power_inj_on_order:
  assumes "finite G" "g ∈ G"
  shows "inj_on (power g) {..<element_order g}"
  unfolding inj_on_def
  by (metis assms lessThan_iff linorder_neqE_nat power_eq_order_False)

end


subsection ‹Cyclic subgroups›

text ‹The cyclic subgroup generated by an element @{term g}: the set of its powers.
  For @{term g} of finite order this is @{term "power g ` {..<element_order g}"}.›

definition (in Group) cyclic_subgroup :: "'a ⇒ 'a set"
  where "cyclic_subgroup g = power g ` {..<element_order g}"

context Group
begin

lemma cyclic_subgroup_eq_range:
  assumes fin: "finite G" and gG: "g ∈ G"
  shows "cyclic_subgroup g = range (power g)"
proof (rule set_eqI)
  fix x
  show "x ∈ cyclic_subgroup g ⟷ x ∈ range (power g)"
  proof
    assume "x ∈ range (power g)"
    then obtain n where "x = power g n" by auto
    then have "x = power g (n mod element_order g)"
      using power_mod_order[OF fin gG] by simp
    moreover have "n mod element_order g < element_order g" 
      using element_order_pos[OF fin gG] by simp
    ultimately show "x ∈ cyclic_subgroup g" unfolding cyclic_subgroup_def by auto
  qed (auto simp: cyclic_subgroup_def)
qed

lemma cyclic_subgroup_subset:
  assumes "g ∈ G" shows "cyclic_subgroup g ⊆ G"
  unfolding cyclic_subgroup_def using assms by auto

lemma power_mem_cyclic_subgroup:
  assumes fin: "finite G" and gG: "g ∈ G"
  shows "power g i ∈ cyclic_subgroup g"
  using cyclic_subgroup_eq_range[OF fin gG] by blast

text ‹The cyclic subgroup is indeed a subgroup.›
theorem cyclic_subgroup_is_subgroup:
  assumes fin: "finite G" and gG: "g ∈ G"
  shows "Subgroup (cyclic_subgroup g) G (⋅) 𝟭"
proof -
  have ord_pos: "element_order g > 0" using element_order_pos[OF fin gG] .
  note C_alt = cyclic_subgroup_eq_range[OF fin gG]
  have unit_C: "𝟭 ∈ cyclic_subgroup g" unfolding C_alt
    by (metis local.power_0 rangeI)
  have comp_C: "⋀a b. a ∈ cyclic_subgroup g ⟹ b ∈ cyclic_subgroup g ⟹ a ⋅ b ∈ cyclic_subgroup g"
  proof -
    fix a b assume "a ∈ cyclic_subgroup g" "b ∈ cyclic_subgroup g"
    then obtain i j where "a = power g i" "b = power g j" unfolding C_alt by auto
    then have "a ⋅ b = power g (i + j)" using gG power_add by auto
    then show "a ⋅ b ∈ cyclic_subgroup g" unfolding C_alt by blast
  qed
  have inv_g: "inverse g = power g (element_order g - 1)"
  proof (rule inverse_equality)
    show "g ⋅ power g (element_order g - 1) = 𝟭"
      using power_element_order[OF fin gG] ord_pos
      by (metis Suc_diff_1 local.power_Suc)
    then show "power g (element_order g - 1) ⋅ g = 𝟭"
      using power_element_order[OF fin gG] ord_pos gG local.power_commutes by auto
    show "g ∈ G" by fact
    show "power g (element_order g - 1) ∈ G" using gG by simp
  qed
  have inv_C: "⋀a. a ∈ cyclic_subgroup g ⟹ inverse a ∈ cyclic_subgroup g"
  proof -
    fix a assume "a ∈ cyclic_subgroup g"
    then obtain i where a: "a = power g i" unfolding C_alt by auto
    have "inverse a = power (inverse g) i" using a power_inverse[OF gG] by simp
    also have "… = power (power g (element_order g - 1)) i" using inv_g by simp
    also have "… = power g ((element_order g - 1) * i)" using gG power_mult by simp
    finally have "inverse a = power g ((element_order g - 1) * i)" .
    then show "inverse a ∈ cyclic_subgroup g" unfolding C_alt by blast
  qed
  show ?thesis
    using subgroupI[of "cyclic_subgroup g"] cyclic_subgroup_subset[OF gG] unit_C comp_C inv_C
    by auto
qed

text ‹Its cardinality is the order of the generator.›
theorem card_cyclic_subgroup:
  assumes fin: "finite G" and gG: "g ∈ G"
  shows "card (cyclic_subgroup g) = element_order g"
proof -
  have "card (cyclic_subgroup g) = card (power g ` {..<element_order g})"
    unfolding cyclic_subgroup_def by simp
  also have "… = card {..<element_order g}"
    using card_image power_inj_on_order[OF fin gG] by blast
  also have "… = element_order g" by simp
  finally show ?thesis .
qed

end (* Group *)

lemma (in Group) element_order_dvd_card:
  assumes fin: "finite G" and gG: "g ∈ G"
  shows "element_order g dvd (card G)"
proof -
  interpret CG: subgroup_of_group "cyclic_subgroup g" G "(⋅)" 𝟭
    by (simp add: Group_axioms cyclic_subgroup_is_subgroup[OF fin gG] subgroup_of_group_def)
  from CG.lagrange[OF fin]
  have "card G = element_order g * CG.index"
    using card_cyclic_subgroup[OF fin gG] by simp
  then show ?thesis by auto
qed

lemma (in Group) power_order_eq_1 [simp]: "g∈G ⟹ finite G ⟹ power g (card G) = 𝟭"
  by (simp add: element_order_dvd_card power_mod_order)


lemma (in Monoid_homomorphism) commutes_with_power:
  assumes "g ∈ M"
  shows "η (source.power g n) = target.power (η g) n"
  by (induction n) (simp_all add: commutes_with_unit commutes_with_composition assms)

lemma (in group_homomorphism) element_order_image_dvd:
  assumes "finite G" "finite G'" "g ∈ G"
  shows "target.element_order (η g) dvd source.element_order g"
  by (metis assms commutes_with_power commutes_with_unit map_closed
      source.power_element_order target.element_order_dvd)

lemma (in group_isomorphism) element_order_preserved:
  assumes "finite G" "finite G'" "g ∈ G"
  shows "target.element_order (η g) = source.element_order g"
proof (rule dvd_antisym)
  show "target.element_order (η g) dvd source.element_order g"
    using element_order_image_dvd assms by blast
  show "source.element_order g dvd target.element_order (η g)"
  proof -
    have eta_g: "η g ∈ G'" using assms map_closed by blast
    have "target.power (η g) (target.element_order (η g)) = 𝟭'"
      using target.power_element_order[OF assms(2) eta_g] .
    then have img_eq: "η (source.power g (target.element_order (η g))) = η 𝟭"
      using commutes_with_power assms commutes_with_unit by simp
    have inj: "inj_on η G" using bij_betw_def bijective by blast
    have "source.power g (target.element_order (η g)) = 𝟭"
      using inj_onD[OF inj img_eq _ source.unit_closed] assms by simp
    then show ?thesis
      using source.element_order_dvd[OF assms(1,3)] by blast
  qed
qed

text ‹The same fact stated with the raw ‹Monoid.element_order› applied to the explicit
  operations and units, rather than the locale-qualified ‹source.element_order› /
  ‹target.element_order›.  This is the form a caller working with concrete groups (e.g.\ the
  symmetric group under ‹(∘)›/‹id›) can unify against directly --- the prefixed versions are
  definitionally equal but do not match by name across interpretations.›
lemma (in group_isomorphism) element_order_preserved':
  assumes "finite G" "finite G'" "g ∈ G"
  shows "Monoid.element_order (⋅') (𝟭') (η g) = Monoid.element_order (⋅) 𝟭 g"
  using element_order_preserved[OF assms] .

lemma (in Group) element_order_power_prime:
  assumes fin: "finite G" and gG: "g ∈ G" and prime: "prime p" and dvd: "p dvd element_order g"
  shows "element_order (power g (element_order g div p)) = p"
proof -
  define k where "k = element_order g div p"
  have ord_eq: "element_order g = p * k"
    using dvd by (simp add: k_def)
  have k_pos: "k > 0"
    using element_order_pos[OF fin gG] ord_eq prime by (metis gr0I mult_is_0)
  have gk: "power g k ∈ G" using gG by simp
  have "power (power g k) p = power g (element_order g)"
    by (simp add: gG local.power_mult mult.commute ord_eq)
  then have dvd_p: "element_order (power g k) dvd p"
    using element_order_dvd[OF fin gk]
    by (simp add: fin gG power_element_order)
  have "element_order (power g k) ≠ 1"
    using power_element_order[of "power g k"] fin gG gk k_pos
    by (metis dvd_mult_cancel2 element_order_dvd not_prime_1 ord_eq power_1 prime)
  with dvd_p prime show ?thesis
    unfolding k_def by (metis prime_nat_iff)
qed

end