Documentation

Mathlib.GroupTheory.DoubleCoset

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 #

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 (x1 x2 : α) => x1 * a * x2) 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} [Group G] (H : Subgroup G) (K : Subgroup G) (a : G) :
    a Doset.doset a H K
    theorem Doset.doset_eq_of_mem {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} {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} [Group G] {H : Subgroup G} {K : Subgroup G} {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} [Group G] {H : Subgroup G} {K : Subgroup G} {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} [Group G] (H : Set G) (K : Set G) :

    The setoid defined by the double_coset relation

    Equations
    Instances For
      def Doset.Quotient {G : Type u_1} [Group G] (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} [Group G] {H : Subgroup G} {K : Subgroup G} {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} [Group G] (H : Subgroup G) :
        (Doset.setoid H).Rel = (QuotientGroup.leftRel H).Rel
        def Doset.quotToDoset {G : Type u_1} [Group G] (H : Subgroup G) (K : Subgroup G) (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} [Group G] (H : Subgroup G) (K : Subgroup G) (a : G) :
          Doset.Quotient H K

          Map from G to H \ G / K

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