# mathlibdocumentation

group_theory.double_coset

# 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 writen 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.
• double_coset.quotient: The quotient of G by the double coset relation, i.e, H \ G / K.
def doset {α : Type u_2} [has_mul α] (a : α) (s t : set α) :
set α

The double_coset as an element of set α corresponding to s a t

Equations
• s t = s * {a} * t
theorem doset.mem_doset {α : Type u_2} [has_mul α] {s t : set α} {a b : α} :
b s t ∃ (x : α) (H : x s) (y : α) (H : y t), b = x * a * y
theorem doset.mem_doset_self {G : Type u_1} [group G] (H K : subgroup G) (a : G) :
a H K
theorem doset.doset_eq_of_mem {G : Type u_1} [group G] {H K : subgroup G} {a b : G} (hb : b H K) :
H K = H K
theorem doset.mem_doset_of_not_disjoint {G : Type u_1} [group G] {H K : subgroup G} {a b : G} (h : ¬disjoint (doset a H K) (doset b H K)) :
b H K
theorem doset.eq_of_not_disjoint {G : Type u_1} [group G] {H K : subgroup G} {a b : G} (h : ¬disjoint (doset a H K) (doset b H K)) :
H K = H K
def doset.setoid {G : Type u_1} [group G] (H K : set G) :

The setoid defined by the double_coset relation

Equations
def doset.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
Instances for doset.quotient
theorem doset.rel_iff {G : Type u_1} [group G] {H K : subgroup G} {x y : G} :
K).rel x y ∃ (a : G) (H : a H) (b : G) (H : b K), y = a * x * b
theorem doset.bot_rel_eq_left_rel {G : Type u_1} [group G] (H : subgroup G) :
theorem doset.rel_bot_eq_right_group_rel {G : Type u_1} [group G] (H : subgroup G) :
def doset.quot_to_doset {G : Type u_1} [group G] (H K : subgroup G) (q : K) :
set G

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

Equations
@[reducible]
def doset.mk {G : Type u_1} [group G] (H K : subgroup G) (a : G) :

Map from G to H \ G / K`

@[protected, instance]
def doset.quotient.inhabited {G : Type u_1} [group G] (H K : subgroup G) :
Equations
theorem doset.eq {G : Type u_1} [group G] (H K : subgroup G) (a b : G) :
K a = K b ∃ (h : G) (H : h H) (k : G) (H : k K), b = h * a * k
theorem doset.out_eq' {G : Type u_1} [group G] (H K : subgroup G) (q : K) :
K = q
theorem doset.mk_out'_eq_mul {G : Type u_1} [group G] (H K : subgroup G) (g : G) :
∃ (h 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 K : subgroup G} {a b : G} (h : H K = H K) :
K a = K b
theorem doset.disjoint_out' {G : Type u_1} [group G] {H K : subgroup G} {a b : K} :
a bdisjoint (doset H K) (doset H K)
theorem doset.union_quot_to_doset {G : Type u_1} [group G] (H K : subgroup G) :
(⋃ (q : K), q) = set.univ
theorem doset.doset_union_right_coset {G : Type u_1} [group G] (H K : subgroup G) (a : G) :
(⋃ (k : K), (a * k)) = H K
theorem doset.doset_union_left_coset {G : Type u_1} [group G] (H K : subgroup G) (a : G) :
(⋃ (h : H), left_coset (h * a) K) = H K
theorem doset.left_bot_eq_left_quot {G : Type u_1} [group G] (H : subgroup G) :
= (G H)
theorem doset.right_bot_eq_right_quot {G : Type u_1} [group G] (H : subgroup G) :