Quelle  Left_Coset.thy   Sprache: Isabelle

theory Left_Coset
imports Coset

(*This instance of Coset.thy but for left cosets is due to Jonas Rädle and has been imported
  from the AFP entry Orbit_Stabiliser. *)

begin

definition
  LCOSETS  :: "[_, 'a set] \ ('a set)set"
    (‹(‹open_block notation=‹prefix lcosets››lcosets🍋 _)› [81] 80)
  where "lcosets\<^bsub>G\<^esub> H = (\a\carrier G. {a <#\<^bsub>G\<^esub> H})"

definition
  LFactGroup :: "[('a,'b) monoid_scheme, 'a set] \ ('a set) monoid" (infixl ‹LMod› 65)
    🍋 ‹Actually defined for groups rather than monoids›
   where "LFactGroup G H = \carrier = lcosets\<^bsub>G\<^esub> H, mult = set_mult G, one = H\"

lemma (in group) lcos_self: "[| x \ carrier G; subgroup H G |] ==> x \ x <# H"
  by (simp add: group_l_invI subgroup.lcos_module_rev subgroup.one_closed)

text ‹Elements of a left coset are in the carrier›
lemma (in subgroup) elemlcos_carrier:
  assumes "group G" "a \ carrier G" "a' \ a <# H"
  shows "a' \ carrier G"
  by (meson assms group.l_coset_carrier subgroup_axioms)

text ‹Step one for lemma ‹rcos_module››
lemma (in subgroup) lcos_module_imp:
  assumes "group G"
  assumes xcarr: "x \ carrier G"
      and x'cos: "x' ∈ x <# H"
  shows "(inv x \ x') \ H"
proof -
  interpret group G by fact
  obtain h
    where hH: "h \ H" and x': "x' = x ⊗ h" and hcarr: "h ∈ carrier G"
    using assms by (auto simp: l_coset_def)
  have "(inv x) \ x' = (inv x) \ (x \ h)"
    by (simp add: x')
  have "\ = (x \ inv x) \ h"
    by (metis hcarr inv_closed inv_inv l_inv m_assoc xcarr)
  also have "\ = h"
    by (simp add: hcarr xcarr)
  finally have "(inv x) \ x' = h"
    using x' by metis
  then show "(inv x) \ x' \ H"
    using hH by force
qed

text ‹Left cosets are subsets of the carrier.› 
lemma (in subgroup) lcosets_carrier:
  assumes "group G"
  assumes XH: "X \ lcosets H"
  shows "X \ carrier G"
proof -
  interpret group G by fact
  show "X \ carrier G"
    using XH l_coset_subset_G subset by (auto simp: LCOSETS_def)
qed

lemma (in group) lcosets_part_G:
  assumes "subgroup H G"
  shows "\(lcosets H) = carrier G"
proof -
  interpret subgroup H G by fact
  show ?thesis
  proof
    show "\ (lcosets H) \ carrier G"
      by (force simp add: LCOSETS_def l_coset_def)
    show "carrier G \ \ (lcosets H)"
      by (auto simp add: LCOSETS_def intro: lcos_self assms)
  qed
qed

lemma (in group) lcosets_subset_PowG:
     "subgroup H G \ lcosets H \ Pow(carrier G)"
  using lcosets_part_G subset_Pow_Union by blast

lemma (in group) lcos_disjoint:
  assumes "subgroup H G"
  assumes p: "a \ lcosets H" "b \ lcosets H" "a\b"
  shows "a \ b = {}"
proof -
  interpret subgroup H G by fact
  show ?thesis
    using p l_repr_independence subgroup_axioms unfolding LCOSETS_def disjoint_iff
    by blast
qed

text‹The next two lemmas support the proof of ‹card_cosets_equal›.›
lemma (in group) inj_on_f':
    "\H \ carrier G; a \ carrier G\ \ inj_on (\y. y \ inv a) (a <# H)"
  by (simp add: inj_on_g l_coset_subset_G)

lemma (in group) inj_on_f'':
    "\H \ carrier G; a \ carrier G\ \ inj_on (\y. inv a \ y) (a <# H)"
  by (meson inj_on_cmult inv_closed l_coset_subset_G inj_on_subset)

lemma (in group) inj_on_g':
    "\H \ carrier G; a \ carrier G\ \ inj_on (\y. a \ y) H"
  using inj_on_cmult inj_on_subset by blast

lemma (in group) l_card_cosets_equal:
  assumes "c \ lcosets H" and H: "H \ carrier G" and fin: "finite(carrier G)"
  shows "card H = card c"
proof -
  obtain x where x: "x \ carrier G" and c: "c = x <# H"
    using assms by (auto simp add: LCOSETS_def)
  have "inj_on ((\) x) H"
    by (simp add: H group.inj_on_g' x)
  moreover
  have "(\) x ` H \ x <# H"
    by (force simp add: m_assoc subsetD l_coset_def)
  moreover
  have "inj_on ((\) (inv x)) (x <# H)"
    by (simp add: H group.inj_on_f'' x)
  moreover
  have "\h. h \ H \ inv x \ (x \ h) \ H"
    by (metis H in_mono inv_solve_left m_closed x)
  then have "(\) (inv x) ` (x <# H) \ H"
    by (auto simp: l_coset_def)
  ultimately show ?thesis
    by (metis H fin c card_bij_eq finite_imageD finite_subset)
qed

theorem (in group) l_lagrange:
  assumes "finite(carrier G)" "subgroup H G"
  shows "card(lcosets H) * card(H) = order(G)"
proof -
  have "card H * card (lcosets H) = card (\ (lcosets H))"
    using card_partition
    by (metis (no_types, lifting) assms finite_UnionD l_card_cosets_equal lcos_disjoint lcosets_part_G subgroup.subset)
  then show ?thesis
    by (simp add: assms(2) lcosets_part_G mult.commute order_def)
qed

end