Theory Action_To_Sn

section ‹Embedding a Faithful Finite Action into a Concrete Symmetric Group›

theory Action_To_Sn
  imports Symmetric_Group Group_Operations
begin

subsection ‹Relabelling Symmetric Groups along a Bijection›

text ‹Relabelling along a bijection @{term e} from @{term "{0..<n}"} to a finite set @{term X}
  transports the symmetric group on @{term X} to @{term "Sn n"}.›

definition pull :: "nat ⇒ (nat ⇒ 'a) ⇒ ('a ⇒ 'a) ⇒ (nat ⇒ nat)"
  where "pull n e a = (λi. if i < n then inv_into {0..<n} e (a (e i)) else i)"

context
  fixes n :: nat and e :: "nat ⇒ 'a" and X :: "'a set"
  assumes ebij: "bij_betw e {0..<n} X"
begin

lemma e_in_X: "i < n ⟹ e i ∈ X"
  using ebij by (auto simp: bij_betw_def)

lemma inv_e_lt: "x ∈ X ⟹ inv_into {0..<n} e x < n"
  using ebij by (metis atLeastLessThan_iff bij_betw_def inv_into_into)

lemma inv_e_e: "i < n ⟹ inv_into {0..<n} e (e i) = i"
  using ebij by (simp add: bij_betw_inv_into_left)

lemma e_inv_e: "x ∈ X ⟹ e (inv_into {0..<n} e x) = x"
  using ebij by (simp add: bij_betw_inv_into_right)

lemma pull_permutes:
  assumes a: "a ∈ transformations.Sym X"
  shows "pull n e a permutes {0..<n}"
proof (rule bij_imp_permutes)
  have abij: "bij_betw a X X" using a by (simp add: transformations.Units_bijective)
  show "bij_betw (pull n e a) {0..<n} {0..<n}"
  proof (rule bij_betwI)
    show "pull n e a ∈ {0..<n} → {0..<n}"
      using abij by (auto simp: pull_def e_in_X inv_e_lt bij_betwE)
    show "(λi. inv_into {0..<n} e (inv_into X a (e i))) ∈ {0..<n} → {0..<n}"
      using abij by (simp add: bij_betw_def e_in_X inv_e_lt inv_into_into)
  next
    fix i assume "i ∈ {0..<n}"
    then have iln: "i < n" by simp
    have eiX: "e i ∈ X" using iln by (rule e_in_X)
    have aeiX: "a (e i) ∈ X" using abij eiX by (auto simp: bij_betwE)
    have "(λi. inv_into {0..<n} e (inv_into X a (e i))) (pull n e a i)
            = inv_into {0..<n} e (inv_into X a (e (inv_into {0..<n} e (a (e i)))))"
      using iln by (simp add: pull_def)
    also have "inv_into X a (e (inv_into {0..<n} e (a (e i)))) = e i"
      using abij eiX by (simp add: aeiX bij_betw_inv_into_left e_inv_e)
    finally show "(λi. inv_into {0..<n} e (inv_into X a (e i))) (pull n e a i) = i"
      by (simp add: iln inv_e_e)
    have inv_in: "inv_into X a (e i) ∈ X"
      using abij eiX by (metis bij_betw_inv_into bij_betwE)
    have "pull n e a ((λi. inv_into {0..<n} e (inv_into X a (e i))) i)
            = inv_into {0..<n} e (a (e (inv_into {0..<n} e (inv_into X a (e i)))))"
      using iln inv_in by (simp add: pull_def inv_e_lt)
    also have "a (e (inv_into {0..<n} e (inv_into X a (e i)))) = e i"
      by (metis abij bij_betw_inv_into_right e_inv_e eiX inv_in)
    finally show "pull n e a ((λi. inv_into {0..<n} e (inv_into X a (e i))) i) = i"
      using iln inv_e_e by presburger
  qed
qed (simp add: pull_def)


lemma pull_compose:
  assumes a: "a ∈ transformations.Sym X" and b: "b ∈ transformations.Sym X"
  shows "pull n e (compose X a b) = pull n e a ∘ pull n e b"
proof (rule ext)
  fix i
  show "pull n e (compose X a b) i = (pull n e a ∘ pull n e b) i"
  proof (cases "i < n")
    case True
    then have beiX: "b (e i) ∈ X"
      by (meson b bij_betwE e_in_X transformations.Units_bij_betwI)
    then show ?thesis
      using True inv_e_lt beiX by (simp add: True compose_eq e_in_X pull_def e_inv_e)
  next
    case False
    then show ?thesis by (simp add: pull_def compose_def)
  qed
qed

lemma pull_unit: "pull n e (identity X) = id"
  using e_in_X by (auto simp: pull_def inv_e_e)

lemma pull_in_Sn: "a ∈ transformations.Sym X ⟹ pull n e a ∈ Sn n"
  by (simp add: Sn_def pull_permutes)

end

context Group_Action
begin

text ‹Transport a faithful finite action into the concrete symmetric group Sn (card S),
  via an enumeration e of S.›

lemma action_pull_hom:
  assumes ebij: "bij_betw e {0..<n} S"
  shows "group_homomorphism (restrict (λg. pull n e (φ g)) G) G (⋅) 𝟭 (Sn n) (∘) id"
proof -
  interpret T: Group "Sn n" "(∘)" id by (rule Group_Sn)
  have phiSym: "φ g ∈ transformations.Sym S" if "g ∈ G" for g
    using that by (rule hom_closed)
  show ?thesis
  proof 
    show "restrict (λg. pull n e (φ g)) G ∈ G →⇩E Sn n"
      using phiSym ebij by (simp add: pull_in_Sn)
  next
    fix g h assume g: "g ∈ G" and h: "h ∈ G"
    have "pull n e (φ (g ⋅ h)) = pull n e (φ g) ∘ pull n e (φ h)"
      by (simp add: ebij g h hom_compose pull_compose)
    then show "restrict (λg. pull n e (φ g)) G (g ⋅ h)
                = restrict (λg. pull n e (φ g)) G g ∘ restrict (λg. pull n e (φ g)) G h"
      using g h by (simp add: grp.composition_closed)
  next
    show "restrict (λg. pull n e (φ g)) G 𝟭 = id"
      using ebij grp.unit_closed by (simp add: hom_unit pull_unit)
  qed
qed

text ‹Under faithfulness the transported homomorphism has trivial kernel, hence is injective.›
lemma action_pull_inj:
  assumes ebij: "bij_betw e {0..<n} S" and faith: faithful
  shows "inj_on (restrict (λg. pull n e (φ g)) G) G"
proof (rule inj_onI)
  fix g h assume g: "g ∈ G" and h: "h ∈ G"
    and eq: "restrict (λg. pull n e (φ g)) G g = restrict (λg. pull n e (φ g)) G h"
  have pgh: "pull n e (φ g) = pull n e (φ h)" using eq g h by simp
  have agree: "φ g s = φ h s" if s: "s ∈ S" for s
  proof -
    define i where "i ≡ inv_into {0..<n} e s"
    have iln: "i < n" using ebij s unfolding i_def by (metis atLeastLessThan_iff bij_betw_def inv_into_into)
    have ei: "e i = s" using ebij s unfolding i_def by (simp add: bij_betw_inv_into_right)
    have "inv_into {0..<n} e (φ g s) = inv_into {0..<n} e (φ h s)"
      by (metis ei iln pgh pull_def)
    then show "φ g s = φ h s"
      by (metis action_closed bij_betw_inv_into_right ebij g h that)  
  qed
  have ginvg: "grp.inverse g ∈ G" using g by (simp add: grp.invertible_inverse_closed grp.invertible)
  have ghG: "grp.inverse g ⋅ h ∈ G" using ginvg h by (rule grp.composition_closed)
  have triv: "φ (grp.inverse g ⋅ h) s = s" if s: "s ∈ S" for s
    by (metis action_mult agree g ginvg group_inv_rel h that)
  have invgh: "grp.inverse g ⋅ h = 𝟭"
    using faith ghG triv unfolding faithful_def by blast
  show "g = h"
    using g grp.inverse_unique h invgh by auto 
qed

text ‹Hence a faithful finite action embeds @{term G} as a subgroup of @{term "Sn n"}: the
  transported map is a group isomorphism onto its image.›
theorem action_embeds_Sn:
  assumes ebij: "bij_betw e {0..<n} S" and faith: faithful
  shows "group_isomorphism (restrict (λg. pull n e (φ g)) G) G (⋅) 𝟭
           ((λg. pull n e (φ g)) ` G) (∘) id"
proof -
  interpret H: group_homomorphism "restrict (λg. pull n e (φ g)) G" G "(⋅)" 𝟭 "Sn n" "(∘)" id
    by (rule action_pull_hom[OF ebij])
  have img: "restrict (λg. pull n e (φ g)) G ` G = (λg. pull n e (φ g)) ` G" by auto
  interpret Img: Subgroup "(λg. pull n e (φ g)) ` G" "Sn n" "(∘)" id
    using H.image.Subgroup_axioms img by simp
  show ?thesis
  proof 
    have inj: "inj_on (restrict (λg. pull n e (φ g)) G) G" 
      by (rule action_pull_inj[OF ebij faith])
    with img show "bij_betw (restrict (λg. pull n e (φ g)) G) G ((λg. pull n e (φ g)) ` G)"
      by (simp add: bij_betw_def)
  qed (use H.commutes_with_unit H.commutes_with_composition in auto)
qed

end

end