mathlib3 documentation

group_theory.double_coset

Double cosets #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

doset a s t = s * {a} * t

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) :

a ∈ doset a ↑H ↑K

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) :

doset b ↑H ↑K = 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)) :

b ∈ doset a ↑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)) :

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

doset.setoid H K = setoid.ker (λ (x : G), doset x H K)

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

doset.quotient H K = quotient (doset.setoid H K)

Instances for doset.quotient

doset.quotient.inhabited

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

theorem doset.bot_rel_eq_left_rel {G : Type u_1} [group G] (H : subgroup G) :

(doset.setoid ↑⊥ ↑H).rel = (quotient_group.left_rel H).rel

theorem doset.rel_bot_eq_right_group_rel {G : Type u_1} [group G] (H : subgroup G) :

(doset.setoid ↑H ↑⊥).rel = (quotient_group.right_rel H).rel

def doset.quot_to_doset {G : Type u_1} [group G] (H K : subgroup G) (q : doset.quotient ↑H ↑K) :

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

Equations

doset.quot_to_doset H K q = doset (quotient.out' q) ↑H ↑K

@[reducible]

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

doset.quotient ↑H ↑K

Map from G to H \ G / K

@[protected, instance]

def doset.quotient.inhabited {G : Type u_1} [group G] (H K : subgroup G) :

inhabited (doset.quotient ↑H ↑K)

Equations

doset.quotient.inhabited H K = {default := doset.mk H K 1}

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) :

doset.mk H K (quotient.out' q) = 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 : 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} :

a ≠ b → disjoint (doset (quotient.out' a) ↑H ↑K) (doset (quotient.out' b) ↑H ↑K)

theorem doset.union_quot_to_doset {G : Type u_1} [group G] (H K : subgroup G) :

(⋃ (q : doset.quotient ↑H ↑K), doset.quot_to_doset H K q) = set.univ

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) :

doset.quotient ⊥.carrier ↑H = (G ⧸ H)

theorem doset.right_bot_eq_right_quot {G : Type u_1} [group G] (H : subgroup G) :

doset.quotient H.carrier ↑⊥ = quotient (quotient_group.right_rel H)