(*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>(\<open>open_block notation=\<open>prefix lcosets\<close>\<close>lcosets\<index> _)\<close> [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) \<comment> \<open>Actually defined for groups rather than monoids\<close> 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\<open>Elements of a left coset are in the carrier\<close> 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\<open>Step one for lemma \<open>rcos_module\<close>\<close> lemma (in subgroup) lcos_module_imp: assumes"group G" assumes xcarr: "x \ carrier G" and x'cos: "x'\<in> 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) alsohave"\ = h" by (simp add: hcarr xcarr) finallyhave"(inv x) \ x' = h" using x' by metis thenshow"(inv x) \ x' \ H" using hH by force qed
text\<open>Left cosets are subsets of the carrier.\<close> 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\<open>The next two lemmas support the proof of \<open>card_cosets_equal\<close>.\<close> 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) thenhave"(\) (inv x) ` (x <# H) \ H" by (auto simp: l_coset_def) ultimatelyshow ?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) thenshow ?thesis by (simp add: assms(2) lcosets_part_G mult.commute order_def) qed
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
