Documentation

Mathlib.GroupTheory.Coset.Defs

Cosets #

This file develops the basic theory of left and right cosets.

When G is a group and a : G, s : Set G, with open scoped Pointwise we can write:

If instead G is an additive group, we can write (with open scoped Pointwise still)

Main definitions #

Notation #

TODO #

Properly merge with pointwise actions on sets, by renaming and deduplicating lemmas as appropriate.

def QuotientGroup.leftRel {α : Type u_1} [Group α] (s : Subgroup α) :

The equivalence relation corresponding to the partition of a group by left cosets of a subgroup.

Equations
    Instances For
      def QuotientAddGroup.leftRel {α : Type u_1} [AddGroup α] (s : AddSubgroup α) :

      The equivalence relation corresponding to the partition of a group by left cosets of a subgroup.

      Equations
        Instances For
          theorem QuotientGroup.leftRel_apply {α : Type u_1} [Group α] {s : Subgroup α} {x y : α} :
          (leftRel s) x y x⁻¹ * y s
          theorem QuotientAddGroup.leftRel_apply {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {x y : α} :
          (leftRel s) x y -x + y s
          theorem QuotientGroup.leftRel_eq {α : Type u_1} [Group α] (s : Subgroup α) :
          (leftRel s) = fun (x y : α) => x⁻¹ * y s
          theorem QuotientAddGroup.leftRel_eq {α : Type u_1} [AddGroup α] (s : AddSubgroup α) :
          (leftRel s) = fun (x y : α) => -x + y s
          instance QuotientGroup.leftRelDecidable {α : Type u_1} [Group α] (s : Subgroup α) [DecidablePred fun (x : α) => x s] :
          Equations
            instance QuotientAddGroup.leftRelDecidable {α : Type u_1} [AddGroup α] (s : AddSubgroup α) [DecidablePred fun (x : α) => x s] :
            Equations

              α ⧸ s is the quotient type representing the left cosets of s. If s is a normal subgroup, α ⧸ s is a group

              Equations

                α ⧸ s is the quotient type representing the left cosets of s. If s is a normal subgroup, α ⧸ s is a group

                Equations
                  Equations
                    def QuotientGroup.rightRel {α : Type u_1} [Group α] (s : Subgroup α) :

                    The equivalence relation corresponding to the partition of a group by right cosets of a subgroup.

                    Equations
                      Instances For
                        def QuotientAddGroup.rightRel {α : Type u_1} [AddGroup α] (s : AddSubgroup α) :

                        The equivalence relation corresponding to the partition of a group by right cosets of a subgroup.

                        Equations
                          Instances For
                            theorem QuotientGroup.rightRel_apply {α : Type u_1} [Group α] {s : Subgroup α} {x y : α} :
                            (rightRel s) x y y * x⁻¹ s
                            theorem QuotientAddGroup.rightRel_apply {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {x y : α} :
                            (rightRel s) x y y + -x s
                            theorem QuotientGroup.rightRel_eq {α : Type u_1} [Group α] (s : Subgroup α) :
                            (rightRel s) = fun (x y : α) => y * x⁻¹ s
                            theorem QuotientAddGroup.rightRel_eq {α : Type u_1} [AddGroup α] (s : AddSubgroup α) :
                            (rightRel s) = fun (x y : α) => y + -x s
                            instance QuotientGroup.rightRelDecidable {α : Type u_1} [Group α] (s : Subgroup α) [DecidablePred fun (x : α) => x s] :
                            Equations
                              instance QuotientAddGroup.rightRelDecidable {α : Type u_1} [AddGroup α] (s : AddSubgroup α) [DecidablePred fun (x : α) => x s] :
                              Equations

                                Right cosets are in bijection with left cosets.

                                Equations
                                  Instances For

                                    Right cosets are in bijection with left cosets.

                                    Equations
                                      Instances For
                                        @[reducible, inline]
                                        abbrev QuotientGroup.mk {α : Type u_1} [Group α] {s : Subgroup α} (a : α) :
                                        α s

                                        The canonical map from a group α to the quotient α ⧸ s.

                                        Equations
                                          Instances For
                                            @[reducible, inline]
                                            abbrev QuotientAddGroup.mk {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (a : α) :
                                            α s

                                            The canonical map from an AddGroup α to the quotient α ⧸ s.

                                            Equations
                                              Instances For
                                                @[simp]
                                                theorem QuotientGroup.range_mk {α : Type u_1} [Group α] {s : Subgroup α} :
                                                theorem QuotientGroup.induction_on {α : Type u_1} [Group α] {s : Subgroup α} {C : α sProp} (x : α s) (H : ∀ (z : α), C z) :
                                                C x
                                                theorem QuotientAddGroup.induction_on {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {C : α sProp} (x : α s) (H : ∀ (z : α), C z) :
                                                C x
                                                instance QuotientGroup.instCoeQuotientSubgroup {α : Type u_1} [Group α] {s : Subgroup α} :
                                                Coe α (α s)
                                                Equations
                                                  instance QuotientAddGroup.instCoeQuotientAddSubgroup {α : Type u_1} [AddGroup α] {s : AddSubgroup α} :
                                                  Coe α (α s)
                                                  Equations
                                                    theorem QuotientGroup.induction_on' {α : Type u_1} [Group α] {s : Subgroup α} {C : α sProp} (x : α s) (H : ∀ (z : α), C z) :
                                                    C x

                                                    Alias of QuotientGroup.induction_on.

                                                    theorem QuotientAddGroup.induction_on' {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {C : α sProp} (x : α s) (H : ∀ (z : α), C z) :
                                                    C x
                                                    @[simp]
                                                    theorem QuotientGroup.quotient_liftOn_mk {α : Type u_1} [Group α] {s : Subgroup α} {β : Sort u_2} (f : αβ) (h : ∀ (a b : α), (leftRel s) a bf a = f b) (x : α) :
                                                    Quotient.liftOn' (↑x) f h = f x
                                                    @[simp]
                                                    theorem QuotientAddGroup.quotient_liftOn_mk {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {β : Sort u_2} (f : αβ) (h : ∀ (a b : α), (leftRel s) a bf a = f b) (x : α) :
                                                    Quotient.liftOn' (↑x) f h = f x
                                                    theorem QuotientGroup.forall_mk {α : Type u_1} [Group α] {s : Subgroup α} {C : α sProp} :
                                                    (∀ (x : α s), C x) ∀ (x : α), C x
                                                    theorem QuotientAddGroup.forall_mk {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {C : α sProp} :
                                                    (∀ (x : α s), C x) ∀ (x : α), C x
                                                    theorem QuotientGroup.exists_mk {α : Type u_1} [Group α] {s : Subgroup α} {C : α sProp} :
                                                    (∃ (x : α s), C x) ∃ (x : α), C x
                                                    theorem QuotientAddGroup.exists_mk {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {C : α sProp} :
                                                    (∃ (x : α s), C x) ∃ (x : α), C x
                                                    Equations
                                                      theorem QuotientGroup.eq {α : Type u_1} [Group α] {s : Subgroup α} {a b : α} :
                                                      a = b a⁻¹ * b s
                                                      theorem QuotientAddGroup.eq {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {a b : α} :
                                                      a = b -a + b s
                                                      theorem QuotientGroup.out_eq' {α : Type u_1} [Group α] {s : Subgroup α} (a : α s) :
                                                      (Quotient.out a) = a
                                                      theorem QuotientAddGroup.out_eq' {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (a : α s) :
                                                      (Quotient.out a) = a
                                                      theorem QuotientGroup.mk_out_eq_mul {α : Type u_1} [Group α] (s : Subgroup α) (g : α) :
                                                      ∃ (h : s), Quotient.out g = g * h
                                                      theorem QuotientAddGroup.mk_out_eq_mul {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (g : α) :
                                                      ∃ (h : s), Quotient.out g = g + h
                                                      @[simp]
                                                      theorem QuotientGroup.mk_mul_of_mem {α : Type u_1} [Group α] {s : Subgroup α} {b : α} (a : α) (hb : b s) :
                                                      ↑(a * b) = a
                                                      @[simp]
                                                      theorem QuotientAddGroup.mk_add_of_mem {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {b : α} (a : α) (hb : b s) :
                                                      ↑(a + b) = a
                                                      theorem QuotientGroup.preimage_image_mk {α : Type u_1} [Group α] (N : Subgroup α) (s : Set α) :
                                                      mk ⁻¹' (mk '' s) = ⋃ (x : N), (fun (x_1 : α) => x_1 * x) ⁻¹' s
                                                      theorem QuotientAddGroup.preimage_image_mk {α : Type u_1} [AddGroup α] (N : AddSubgroup α) (s : Set α) :
                                                      mk ⁻¹' (mk '' s) = ⋃ (x : N), (fun (x_1 : α) => x_1 + x) ⁻¹' s
                                                      theorem QuotientGroup.preimage_image_mk_eq_iUnion_image {α : Type u_1} [Group α] (N : Subgroup α) (s : Set α) :
                                                      mk ⁻¹' (mk '' s) = ⋃ (x : N), (fun (x_1 : α) => x_1 * x) '' s
                                                      theorem QuotientAddGroup.preimage_image_mk_eq_iUnion_image {α : Type u_1} [AddGroup α] (N : AddSubgroup α) (s : Set α) :
                                                      mk ⁻¹' (mk '' s) = ⋃ (x : N), (fun (x_1 : α) => x_1 + x) '' s
                                                      theorem QuotientGroup.preimage_image_mk_eq_mul {α : Type u_1} [Group α] (N : Subgroup α) (s : Set α) :
                                                      mk ⁻¹' (mk '' s) = s * N
                                                      theorem QuotientAddGroup.preimage_image_mk_eq_add {α : Type u_1} [AddGroup α] (N : AddSubgroup α) (s : Set α) :
                                                      mk ⁻¹' (mk '' s) = s + N
                                                      def Subgroup.quotientEquivOfEq {α : Type u_1} [Group α] {s t : Subgroup α} (h : s = t) :
                                                      α s α t

                                                      If two subgroups M and N of G are equal, their quotients are in bijection.

                                                      Equations
                                                        Instances For
                                                          def AddSubgroup.quotientEquivOfEq {α : Type u_1} [AddGroup α] {s t : AddSubgroup α} (h : s = t) :
                                                          α s α t

                                                          If two subgroups M and N of G are equal, their quotients are in bijection.

                                                          Equations
                                                            Instances For
                                                              theorem Subgroup.quotientEquivOfEq_mk {α : Type u_1} [Group α] {s t : Subgroup α} (h : s = t) (a : α) :
                                                              (quotientEquivOfEq h) a = a