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
Instances For
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 xs, yt, b = x * a * y
theorem Doset.mem_doset_self {G : Type u_1} [] (H : ) (K : ) (a : G) :
a Doset.doset a H K
theorem Doset.doset_eq_of_mem {G : Type u_1} [] {H : } {K : } {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} [] {H : } {K : } {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} [] {H : } {K : } {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} [] (H : Set G) (K : Set G) :

The setoid defined by the double_coset relation

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

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

Equations
Instances For
theorem Doset.rel_iff {G : Type u_1} [] {H : } {K : } {x : G} {y : G} :
(Doset.setoid H K).Rel x y aH, bK, y = a * x * b
theorem Doset.bot_rel_eq_leftRel {G : Type u_1} [] (H : ) :
().Rel = .Rel
theorem Doset.rel_bot_eq_right_group_rel {G : Type u_1} [] (H : ) :
().Rel = .Rel
def Doset.quotToDoset {G : Type u_1} [] (H : ) (K : ) (q : Doset.Quotient H K) :
Set G

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

Equations
Instances For
@[reducible, inline]
abbrev Doset.mk {G : Type u_1} [] (H : ) (K : ) (a : G) :
Doset.Quotient H K

Map from G to H \ G / K

Equations
Instances For
instance Doset.instInhabitedQuotientCoeSubgroup {G : Type u_1} [] (H : ) (K : ) :
Equations
theorem Doset.eq {G : Type u_1} [] (H : ) (K : ) (a : G) (b : G) :
Doset.mk H K a = Doset.mk H K b hH, kK, b = h * a * k
theorem Doset.out_eq' {G : Type u_1} [] (H : ) (K : ) (q : Doset.Quotient H K) :
Doset.mk H K () = q
theorem Doset.mk_out'_eq_mul {G : Type u_1} [] (H : ) (K : ) (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} [] {H : } {K : } {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} [] {H : } {K : } {a : Doset.Quotient H.toSubmonoid K} {b : Doset.Quotient H.toSubmonoid K} :
a bDisjoint (Doset.doset () H K) (Doset.doset () H K)
theorem Doset.union_quotToDoset {G : Type u_1} [] (H : ) (K : ) :
⋃ (q : Doset.Quotient H K), = Set.univ
theorem Doset.doset_union_rightCoset {G : Type u_1} [] (H : ) (K : ) (a : G) :
⋃ (k : K), MulOpposite.op (a * k) H = Doset.doset a H K
theorem Doset.doset_union_leftCoset {G : Type u_1} [] (H : ) (K : ) (a : G) :
⋃ (h : H), (h * a) K = Doset.doset a H K
theorem Doset.left_bot_eq_left_quot {G : Type u_1} [] (H : ) :
Doset.Quotient .toSubmonoid H = (G H)
theorem Doset.right_bot_eq_right_quot {G : Type u_1} [] (H : ) :
Doset.Quotient H.toSubmonoid =