Double cosets

This file defines double cosets for two subgroups H K of a group G and the quotient of G by the double coset relation, i.e. H \ G / K. We also prove that G can be written as a disjoint union of the double cosets and that if one of H or K is the trivial group (i.e. ⊥ ) then this is the usual left or right quotient of a group by a subgroup.

Main definitions

• rel: The double coset relation defined by two subgroups H K of G.
• Doset.quotient: The quotient of G by the double coset relation, i.e, H \ G / K.

def Doset.doset {α : Type u_2} [Mul α] (a : α) (s : Set α) (t : Set α) : Set α

The double coset as an element of Set α corresponding to s a t

Equations

• Doset.doset a s t = s * {a} * t

theorem Doset.doset_eq_image2 {α : Type u_2} [Mul α] (a : α) (s : Set α) (t : Set α) : Doset.doset a s t = Set.image2 (fun (x x_1 : α) => x * a * x_1) s t

theorem Doset.mem_doset {α : Type u_2} [Mul α] {s : Set α} {t : Set α} {a : α} {b : α} : b ∈ Doset.doset a s t ↔ ∃ x ∈ s, ∃ y ∈ t, b = x * a * y

theorem Doset.mem_doset_self {G : Type u_1} [Group G] (H : Subgroup G) (K : Subgroup G) (a : G) : a ∈ Doset.doset a ↑H ↑K

theorem Doset.doset_eq_of_mem {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} {a : G} {b : G} (hb : b ∈ Doset.doset a ↑H ↑K) : Doset.doset b ↑H ↑K = Doset.doset a ↑H ↑K

theorem Doset.mem_doset_of_not_disjoint {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} {a : G} {b : G} (h : ¬Disjoint (Doset.doset a ↑H ↑K) (Doset.doset b ↑H ↑K)) : b ∈ Doset.doset a ↑H ↑K

theorem Doset.eq_of_not_disjoint {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} {a : G} {b : G} (h : ¬Disjoint (Doset.doset a ↑H ↑K) (Doset.doset b ↑H ↑K)) : Doset.doset a ↑H ↑K = Doset.doset b ↑H ↑K

def Doset.setoid {G : Type u_1} [Group G] (H : Set G) (K : Set G) : Setoid G

The setoid defined by the double_coset relation

Equations

• Doset.setoid H K = Setoid.ker fun (x : G) => Doset.doset x H K

def Doset.Quotient {G : Type u_1} [Group G] (H : Set G) (K : Set G) : Type u_1

Quotient of G by the double coset relation, i.e. H \ G / K

Equations

• Doset.Quotient H K = Quotient (Doset.setoid H K)

theorem Doset.rel_iff {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} {x : G} {y : G} : Setoid.Rel (Doset.setoid ↑H ↑K) x y ↔ ∃ a ∈ H, ∃ b ∈ K, y = a * x * b

theorem Doset.bot_rel_eq_leftRel {G : Type u_1} [Group G] (H : Subgroup G) : Setoid.Rel (Doset.setoid ↑⊥ ↑H) = Setoid.Rel (QuotientGroup.leftRel H)

theorem Doset.rel_bot_eq_right_group_rel {G : Type u_1} [Group G] (H : Subgroup G) : Setoid.Rel (Doset.setoid ↑H ↑⊥) = Setoid.Rel (QuotientGroup.rightRel H)

def Doset.quotToDoset {G : Type u_1} [Group G] (H : Subgroup G) (K : Subgroup G) (q : Doset.Quotient ↑H ↑K) : Set G

Create a doset out of an element of H \ G / K

Equations

• Doset.quotToDoset H K q = Doset.doset (Quotient.out' q) ↑H ↑K

@[inline, reducible]

abbrev Doset.mk {G : Type u_1} [Group G] (H : Subgroup G) (K : Subgroup G) (a : G) : Doset.Quotient ↑H ↑K

Map from G to H \ G / K

Equations

• Doset.mk H K a = Quotient.mk'' a

instance Doset.instInhabitedQuotientCoeSubgroupInstSetLikeSubgroup {G : Type u_1} [Group G] (H : Subgroup G) (K : Subgroup G) : Inhabited (Doset.Quotient ↑H ↑K)

Equations

• Doset.instInhabitedQuotientCoeSubgroupInstSetLikeSubgroup H K = { default := Doset.mk H K 1 }

theorem Doset.eq {G : Type u_1} [Group G] (H : Subgroup G) (K : Subgroup G) (a : G) (b : G) : Doset.mk H K a = Doset.mk H K b ↔ ∃ h ∈ H, ∃ k ∈ K, b = h * a * k

theorem Doset.out_eq' {G : Type u_1} [Group G] (H : Subgroup G) (K : Subgroup G) (q : Doset.Quotient ↑H ↑K) : Doset.mk H K (Quotient.out' q) = q

theorem Doset.mk_out'_eq_mul {G : Type u_1} [Group G] (H : Subgroup G) (K : Subgroup G) (g : G) : ∃ (h : G) (k : G), h ∈ H ∧ k ∈ K ∧ Quotient.out' (Doset.mk H K g) = h * g * k

theorem Doset.mk_eq_of_doset_eq {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} {a : G} {b : G} (h : Doset.doset a ↑H ↑K = Doset.doset b ↑H ↑K) : Doset.mk H K a = Doset.mk H K b

theorem Doset.disjoint_out' {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} {a : Doset.Quotient ↑H.toSubmonoid ↑K} {b : Doset.Quotient ↑H.toSubmonoid ↑K} : a ≠ b → Disjoint (Doset.doset (Quotient.out' a) ↑H ↑K) (Doset.doset (Quotient.out' b) ↑H ↑K)

theorem Doset.union_quotToDoset {G : Type u_1} [Group G] (H : Subgroup G) (K : Subgroup G) : ⋃ (q : Doset.Quotient ↑H ↑K), Doset.quotToDoset H K q = Set.univ

theorem Doset.doset_union_rightCoset {G : Type u_1} [Group G] (H : Subgroup G) (K : Subgroup G) (a : G) : ⋃ (k : ↥K), MulOpposite.op (a * ↑k) • ↑H = Doset.doset a ↑H ↑K

theorem Doset.doset_union_leftCoset {G : Type u_1} [Group G] (H : Subgroup G) (K : Subgroup G) (a : G) : ⋃ (h : ↥H), (↑h * a) • ↑K = Doset.doset a ↑H ↑K

theorem Doset.left_bot_eq_left_quot {G : Type u_1} [Group G] (H : Subgroup G) : Doset.Quotient ↑⊥.toSubmonoid ↑H = (G ⧸ H)

theorem Doset.right_bot_eq_right_quot {G : Type u_1} [Group G] (H : Subgroup G) : Doset.Quotient ↑H.toSubmonoid ↑⊥ = Quotient (QuotientGroup.rightRel H)