Theory Left_Coset

```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)"
have "… = (x ⊗ inv x) ⊗ h"
by (metis hcarr inv_closed inv_inv l_inv m_assoc xcarr)
also have "… = h"
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)"

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
```