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

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

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

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

Equations

• DoubleCoset.doubleCoset a s t = s * {a} * t

@[deprecated DoubleCoset.doubleCoset (since := "2025-07-12")]

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

Alias of DoubleCoset.doubleCoset.

---

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

Equations

• @Doset.doset = @DoubleCoset.doubleCoset

theorem DoubleCoset.doubleCoset_eq_image2 {α : Type u_2} [Mul α] (a : α) (s t : Set α) : doubleCoset a s t = Set.image2 (fun (x1 x2 : α) => x1 * a * x2) s t

@[deprecated DoubleCoset.doubleCoset_eq_image2 (since := "2025-07-12")]

theorem Doset.doset_eq_image2 {α : Type u_2} [Mul α] (a : α) (s t : Set α) : DoubleCoset.doubleCoset a s t = Set.image2 (fun (x1 x2 : α) => x1 * a * x2) s t

Alias of DoubleCoset.doubleCoset_eq_image2.

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

@[deprecated DoubleCoset.mem_doubleCoset (since := "2025-07-12")]

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

Alias of DoubleCoset.mem_doubleCoset.

theorem DoubleCoset.mem_doubleCoset_self {G : Type u_1} [Group G] (H K : Subgroup G) (a : G) : a ∈ doubleCoset a ↑H ↑K

@[deprecated DoubleCoset.mem_doubleCoset_self (since := "2025-07-12")]

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

Alias of DoubleCoset.mem_doubleCoset_self.

theorem DoubleCoset.doubleCoset_eq_of_mem {G : Type u_1} [Group G] {H K : Subgroup G} {a b : G} (hb : b ∈ doubleCoset a ↑H ↑K) : doubleCoset b ↑H ↑K = doubleCoset a ↑H ↑K

@[deprecated DoubleCoset.doubleCoset_eq_of_mem (since := "2025-07-12")]

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

Alias of DoubleCoset.doubleCoset_eq_of_mem.

theorem DoubleCoset.mem_doubleCoset_of_not_disjoint {G : Type u_1} [Group G] {H K : Subgroup G} {a b : G} (h : ¬Disjoint (doubleCoset a ↑H ↑K) (doubleCoset b ↑H ↑K)) : b ∈ doubleCoset a ↑H ↑K

@[deprecated DoubleCoset.mem_doubleCoset_of_not_disjoint (since := "2025-07-12")]

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

Alias of DoubleCoset.mem_doubleCoset_of_not_disjoint.

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

@[deprecated DoubleCoset.eq_of_not_disjoint (since := "2025-07-12")]

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

Alias of DoubleCoset.eq_of_not_disjoint.

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

The setoid defined by the double_coset relation

Equations

• DoubleCoset.setoid H K = Setoid.ker fun (x : G) => DoubleCoset.doubleCoset x H K

@[deprecated DoubleCoset.setoid (since := "2025-07-12")]

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

Alias of DoubleCoset.setoid.

---

The setoid defined by the double_coset relation

Equations

• @Doset.setoid = @DoubleCoset.setoid

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

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

Equations

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

@[deprecated DoubleCoset.Quotient (since := "2025-07-12")]

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

Alias of DoubleCoset.Quotient.

---

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

Equations

• @Doset.Quotient = @DoubleCoset.Quotient

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

@[deprecated DoubleCoset.rel_iff (since := "2025-07-12")]

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

Alias of DoubleCoset.rel_iff.

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

@[deprecated DoubleCoset.bot_rel_eq_leftRel (since := "2025-07-12")]

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

Alias of DoubleCoset.bot_rel_eq_leftRel.

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

@[deprecated DoubleCoset.rel_bot_eq_right_group_rel (since := "2025-07-12")]

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

Alias of DoubleCoset.rel_bot_eq_right_group_rel.

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

Create a double coset out of an element of H \ G / K

Equations

• DoubleCoset.quotToDoubleCoset H K q = DoubleCoset.doubleCoset (Quotient.out q) ↑H ↑K

@[deprecated DoubleCoset.quotToDoubleCoset (since := "2025-07-12")]

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

Alias of DoubleCoset.quotToDoubleCoset.

---

Create a double coset out of an element of H \ G / K

Equations

• @Doset.quotToDoset = @DoubleCoset.quotToDoubleCoset

@[reducible, inline]

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

Map from G to H \ G / K

Equations

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

@[deprecated DoubleCoset.mk (since := "2025-07-12")]

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

Alias of DoubleCoset.mk.

---

Map from G to H \ G / K

Equations

• @Doset.mk = @DoubleCoset.mk

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

Equations

• DoubleCoset.instInhabitedQuotientCoeSubgroup H K = { default := DoubleCoset.mk H K 1 }

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

@[deprecated DoubleCoset.eq (since := "2025-07-12")]

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

Alias of DoubleCoset.eq.

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

@[deprecated DoubleCoset.out_eq' (since := "2025-07-12")]

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

Alias of DoubleCoset.out_eq'.

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

@[deprecated DoubleCoset.mk_out_eq_mul (since := "2025-07-12")]

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

Alias of DoubleCoset.mk_out_eq_mul.

theorem DoubleCoset.mk_eq_of_doubleCoset_eq {G : Type u_1} [Group G] {H K : Subgroup G} {a b : G} (h : doubleCoset a ↑H ↑K = doubleCoset b ↑H ↑K) : mk H K a = mk H K b

@[deprecated DoubleCoset.mk_eq_of_doubleCoset_eq (since := "2025-07-12")]

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

Alias of DoubleCoset.mk_eq_of_doubleCoset_eq.

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

@[deprecated DoubleCoset.disjoint_out (since := "2025-07-12")]

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

Alias of DoubleCoset.disjoint_out.

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

@[deprecated DoubleCoset.union_quotToDoubleCoset (since := "2025-07-12")]

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

Alias of DoubleCoset.union_quotToDoubleCoset.

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

@[deprecated DoubleCoset.doubleCoset_union_rightCoset (since := "2025-07-12")]

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

Alias of DoubleCoset.doubleCoset_union_rightCoset.

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

@[deprecated DoubleCoset.doubleCoset_union_leftCoset (since := "2025-07-12")]

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

Alias of DoubleCoset.doubleCoset_union_leftCoset.

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

@[deprecated DoubleCoset.left_bot_eq_left_quot (since := "2025-07-12")]

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

Alias of DoubleCoset.left_bot_eq_left_quot.

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

@[deprecated DoubleCoset.right_bot_eq_right_quot (since := "2025-07-12")]

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

Alias of DoubleCoset.right_bot_eq_right_quot.