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

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

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

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

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

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

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

@[implicit_reducible]

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

The setoid defined by the doubleCoset relation

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

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

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

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

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

@[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

@[implicit_reducible]

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

theorem DoubleCoset.eq'' {G : Type u_1} [Group G] {a b : G} (H K : Subgroup G) : mk H K a = mk H K b ↔ (setoid ↑H ↑K) a b

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

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

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

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

theorem DoubleCoset.mem_quotToDoubleCoset_iff {G : Type u_1} [Group G] {H K : Subgroup G} (i : Quotient ↑H ↑K) (a : G) : a ∈ quotToDoubleCoset H K i ↔ mk H K a = i

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)

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

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

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

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

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

theorem DoubleCoset.finite_quotient_iff_exists_finset_iUnion_eq_univ {G : Type u_1} [Group G] (H K : Subgroup G) : Finite (Quotient ↑H ↑K) ↔ ∃ (I : Finset (Quotient ↑H ↑K)), ⋃ i ∈ I, quotToDoubleCoset H K i = Set.univ

theorem DoubleCoset.iUnion_image_mk_leftRel {G : Type u_1} [Group G] {H K : Subgroup G} : ⋃ (q : Quotient ↑H ↑K), Quot.mk ⇑(QuotientGroup.leftRel K) '' doubleCoset (Quotient.out q) ↑H ↑K = Set.univ

theorem DoubleCoset.iUnion_image_mk_rightRel {G : Type u_1} [Group G] {H K : Subgroup G} : ⋃ (q : Quotient ↑H ↑K), Quot.mk ⇑(QuotientGroup.rightRel H) '' doubleCoset (Quotient.out q) ↑H ↑K = Set.univ

theorem DoubleCoset.iUnion_finset_leftRel_eq_univ_of_leftRel {G : Type u_1} [Group G] {H K : Subgroup G} {t : Finset (Quotient ↑H ↑K)} (ht : Set.univ ⊆ ⋃ i ∈ t, Quot.mk ⇑(QuotientGroup.leftRel K) '' doubleCoset (Quotient.out i) ↑H ↑K) : ⋃ q ∈ t, doubleCoset (Quotient.out q) ↑H ↑K = Set.univ

theorem DoubleCoset.iUnion_finset_rightRel_eq_univ_of_rightRel {G : Type u_1} [Group G] {H K : Subgroup G} {t : Finset (Quotient ↑H ↑K)} (ht : Set.univ ⊆ ⋃ i ∈ t, Quot.mk ⇑(QuotientGroup.rightRel H) '' doubleCoset (Quotient.out i) ↑H ↑K) : ⋃ q ∈ t, doubleCoset (Quotient.out q) ↑H ↑K = Set.univ