mathlib documentation

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 #

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
theorem doset.mem_doset {α : Type u_2} [has_mul α] {s t : set α} {a b : α} :
b doset a 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) :
theorem doset.doset_eq_of_mem {G : Type u_1} [group G] {H K : subgroup G} {a b : G} (hb : b doset a 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)) :
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)) :
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} :
(doset.setoid H K).rel x y ∃ (a : G) (H : a H) (b : G) (H : b K), y = a * x * b
def doset.quot_to_doset {G : Type u_1} [group G] (H K : subgroup G) (q : doset.quotient H K) :
set G

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

Equations
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) :
doset.mk H K a = doset.mk H 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 : doset.quotient H K) :
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 : doset a H K = 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 K : subgroup G} {a b : doset.quotient H.carrier K} :
theorem doset.union_quot_to_doset {G : Type u_1} [group G] (H K : subgroup G) :
theorem doset.doset_union_right_coset {G : Type u_1} [group G] (H K : subgroup G) (a : G) :
(⋃ (k : K), right_coset H (a * k)) = doset a 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) = doset a H K
theorem doset.left_bot_eq_left_quot {G : Type u_1} [group G] (H : subgroup G) :