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" ("lcosetsı _" [81] 80) where "lcosets⇘G⇙ H = (⋃a∈carrier G. {a <#⇘G⇙ 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⇘G⇙ 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 subset_inj_on) 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