Abstract groups

module group-theory.groups where
Imports
open import foundation.binary-embeddings
open import foundation.binary-equivalences
open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.embeddings
open import foundation.equivalences
open import foundation.function-extensionality
open import foundation.functions
open import foundation.homotopies
open import foundation.identity-types
open import foundation.injective-maps
open import foundation.involutions
open import foundation.propositions
open import foundation.sets
open import foundation.subtypes
open import foundation.universe-levels

open import group-theory.monoids
open import group-theory.products-of-elements-monoids
open import group-theory.semigroups

open import lists.concatenation-lists
open import lists.lists

open import structured-types.pointed-types
open import structured-types.pointed-types-equipped-with-automorphisms

Idea

An abstract group is a group in the usual algebraic sense, i.e., it consists of a set equipped with a unit element e, a binary operation x, y ↦ xy, and an inverse operation x ↦ x⁻¹ satisfying the group laws

  (xy)z = x(yz)      (associativity)
     ex = x          (left unit law)
     xe = x          (right unit law)
   x⁻¹x = e          (left inverse law)
   xx⁻¹ = e          (right inverse law)

Definition

The condition that a semigroup is a group

is-group' :
  {l : Level} (G : Semigroup l)  is-unital-Semigroup G  UU l
is-group' G is-unital-Semigroup-G =
  Σ ( type-Semigroup G  type-Semigroup G)
    ( λ i 
      ( (x : type-Semigroup G) 
        Id (mul-Semigroup G (i x) x) (pr1 is-unital-Semigroup-G)) ×
      ( (x : type-Semigroup G) 
        Id (mul-Semigroup G x (i x)) (pr1 is-unital-Semigroup-G)))

is-group :
  {l : Level} (G : Semigroup l)  UU l
is-group G =
  Σ (is-unital-Semigroup G) (is-group' G)

The type of groups

Group :
  (l : Level)  UU (lsuc l)
Group l = Σ (Semigroup l) is-group

module _
  {l : Level} (G : Group l)
  where

  semigroup-Group : Semigroup l
  semigroup-Group = pr1 G

  set-Group : Set l
  set-Group = pr1 semigroup-Group

  type-Group : UU l
  type-Group = pr1 set-Group

  is-set-type-Group : is-set type-Group
  is-set-type-Group = pr2 set-Group

  has-associative-mul-Group : has-associative-mul type-Group
  has-associative-mul-Group = pr2 semigroup-Group

  mul-Group : type-Group  type-Group  type-Group
  mul-Group = pr1 has-associative-mul-Group

  ap-mul-Group :
    {x x' y y' : type-Group} (p : Id x x') (q : Id y y') 
    Id (mul-Group x y) (mul-Group x' y')
  ap-mul-Group p q = ap-binary mul-Group p q

  mul-Group' : type-Group  type-Group  type-Group
  mul-Group' x y = mul-Group y x

  commute-Group : type-Group  type-Group  UU l
  commute-Group x y = mul-Group x y  mul-Group y x

  associative-mul-Group :
    (x y z : type-Group) 
    Id (mul-Group (mul-Group x y) z) (mul-Group x (mul-Group y z))
  associative-mul-Group = pr2 has-associative-mul-Group

  is-group-Group : is-group semigroup-Group
  is-group-Group = pr2 G

  is-unital-Group : is-unital-Semigroup semigroup-Group
  is-unital-Group = pr1 is-group-Group

  monoid-Group : Monoid l
  pr1 monoid-Group = semigroup-Group
  pr2 monoid-Group = is-unital-Group

  unit-Group : type-Group
  unit-Group = pr1 is-unital-Group

  is-unit-Group : type-Group  UU l
  is-unit-Group x = Id x unit-Group

  is-prop-is-unit-Group : (x : type-Group)  is-prop (is-unit-Group x)
  is-prop-is-unit-Group x = is-set-type-Group x unit-Group

  is-unit-group-Prop : type-Group  Prop l
  pr1 (is-unit-group-Prop x) = is-unit-Group x
  pr2 (is-unit-group-Prop x) = is-prop-is-unit-Group x

  left-unit-law-mul-Group :
    (x : type-Group)  Id (mul-Group unit-Group x) x
  left-unit-law-mul-Group = pr1 (pr2 is-unital-Group)

  right-unit-law-mul-Group :
    (x : type-Group)  Id (mul-Group x unit-Group) x
  right-unit-law-mul-Group = pr2 (pr2 is-unital-Group)

  pointed-type-Group : Pointed-Type l
  pr1 pointed-type-Group = type-Group
  pr2 pointed-type-Group = unit-Group

  has-inverses-Group : is-group' semigroup-Group is-unital-Group
  has-inverses-Group = pr2 is-group-Group

  inv-Group : type-Group  type-Group
  inv-Group = pr1 has-inverses-Group

  left-inverse-law-mul-Group :
    (x : type-Group)  Id (mul-Group (inv-Group x) x) unit-Group
  left-inverse-law-mul-Group = pr1 (pr2 has-inverses-Group)

  right-inverse-law-mul-Group :
    (x : type-Group)  Id (mul-Group x (inv-Group x)) unit-Group
  right-inverse-law-mul-Group = pr2 (pr2 has-inverses-Group)

  inv-unit-Group :
    Id (inv-Group unit-Group) unit-Group
  inv-unit-Group =
    ( inv (left-unit-law-mul-Group (inv-Group unit-Group))) 
      ( right-inverse-law-mul-Group unit-Group)

Properties

Multiplication by x from the left is an equivalence

module _
  {l : Level} (G : Group l)
  where

  left-div-Group : type-Group G  type-Group G  type-Group G
  left-div-Group x y = mul-Group G (inv-Group G x) y

  issec-mul-inv-Group :
    (x : type-Group G)  (mul-Group G x  left-div-Group x) ~ id
  issec-mul-inv-Group x y =
    ( inv (associative-mul-Group G _ _ _)) 
    ( ( ap (mul-Group' G y) (right-inverse-law-mul-Group G x)) 
      ( left-unit-law-mul-Group G y))

  isretr-mul-inv-Group :
    (x : type-Group G)  (left-div-Group x  mul-Group G x) ~ id
  isretr-mul-inv-Group x y =
    ( inv (associative-mul-Group G _ _ _)) 
    ( ( ap (mul-Group' G y) (left-inverse-law-mul-Group G x)) 
      ( left-unit-law-mul-Group G y))

  is-equiv-mul-Group : (x : type-Group G)  is-equiv (mul-Group G x)
  is-equiv-mul-Group x =
    is-equiv-has-inverse
      ( left-div-Group x)
      ( issec-mul-inv-Group x)
      ( isretr-mul-inv-Group x)

  equiv-mul-Group : (x : type-Group G)  type-Group G  type-Group G
  pr1 (equiv-mul-Group x) = mul-Group G x
  pr2 (equiv-mul-Group x) = is-equiv-mul-Group x

Multiplication by x from the right is an equivalence

  right-div-Group : type-Group G  type-Group G  type-Group G
  right-div-Group x y = mul-Group G x (inv-Group G y)

  issec-mul-inv-Group' :
    (x : type-Group G)  (mul-Group' G x   y  right-div-Group y x)) ~ id
  issec-mul-inv-Group' x y =
    ( associative-mul-Group G _ _ _) 
    ( ( ap (mul-Group G y) (left-inverse-law-mul-Group G x)) 
      ( right-unit-law-mul-Group G y))

  isretr-mul-inv-Group' :
    (x : type-Group G)  ((λ y  right-div-Group y x)  mul-Group' G x) ~ id
  isretr-mul-inv-Group' x y =
    ( associative-mul-Group G _ _ _) 
    ( ( ap (mul-Group G y) (right-inverse-law-mul-Group G x)) 
      ( right-unit-law-mul-Group G y))

  is-equiv-mul-Group' : (x : type-Group G)  is-equiv (mul-Group' G x)
  is-equiv-mul-Group' x =
    is-equiv-has-inverse
      ( λ y  right-div-Group y x)
      ( issec-mul-inv-Group' x)
      ( isretr-mul-inv-Group' x)

  equiv-mul-Group' : (x : type-Group G)  type-Group G  type-Group G
  pr1 (equiv-mul-Group' x) = mul-Group' G x
  pr2 (equiv-mul-Group' x) = is-equiv-mul-Group' x

Multiplication is a binary equivalence and a binary embedding

  is-binary-equiv-mul-Group : is-binary-equiv (mul-Group G)
  pr1 is-binary-equiv-mul-Group = is-equiv-mul-Group'
  pr2 is-binary-equiv-mul-Group = is-equiv-mul-Group

  is-binary-emb-mul-Group : is-binary-emb (mul-Group G)
  is-binary-emb-mul-Group =
    is-binary-emb-is-binary-equiv is-binary-equiv-mul-Group

  is-emb-mul-Group : (x : type-Group G)  is-emb (mul-Group G x)
  is-emb-mul-Group x = is-emb-is-equiv (is-equiv-mul-Group x)

  is-emb-mul-Group' : (x : type-Group G)  is-emb (mul-Group' G x)
  is-emb-mul-Group' x = is-emb-is-equiv (is-equiv-mul-Group' x)

  is-injective-mul-Group : (x : type-Group G)  is-injective (mul-Group G x)
  is-injective-mul-Group x = is-injective-is-equiv (is-equiv-mul-Group x)

  is-injective-mul-Group' : (x : type-Group G)  is-injective (mul-Group' G x)
  is-injective-mul-Group' x = is-injective-is-equiv (is-equiv-mul-Group' x)

Transposition laws for equalities in groups

  transpose-eq-mul-Group :
    {x y z : type-Group G} 
    (mul-Group G x y  z)  (x  mul-Group G z (inv-Group G y))
  transpose-eq-mul-Group {x} {y} {z} refl =
    inv (isretr-mul-inv-Group' y x)

  inv-transpose-eq-mul-Group :
    {x y z : type-Group G} 
    (x  mul-Group G z (inv-Group G y))  (mul-Group G x y  z)
  inv-transpose-eq-mul-Group {._} {y} {z} refl =
    issec-mul-inv-Group' y z

  transpose-eq-mul-Group' :
    {x y z : type-Group G} 
    Id (mul-Group G x y) z  Id y (mul-Group G (inv-Group G x) z)
  transpose-eq-mul-Group' {x} {y} {z} refl =
    inv (isretr-mul-inv-Group x y)

  inv-transpose-eq-mul-Group' :
    {x y z : type-Group G} 
    Id y (mul-Group G (inv-Group G x) z)  (mul-Group G x y  z)
  inv-transpose-eq-mul-Group' {x} {y} {._} refl =
    issec-mul-inv-Group x _

Distributivity of inverses over multiplication

  distributive-inv-mul-Group :
    (x y : type-Group G) 
    Id
      ( inv-Group G (mul-Group G x y))
      ( mul-Group G (inv-Group G y) (inv-Group G x))
  distributive-inv-mul-Group x y =
    transpose-eq-mul-Group
      ( ( transpose-eq-mul-Group
          ( ( associative-mul-Group G (inv-Group G (mul-Group G x y)) x y) 
            ( left-inverse-law-mul-Group G (mul-Group G x y)))) 
        ( left-unit-law-mul-Group G (inv-Group G y)))

Inverting elements of a group is an involution

  inv-inv-Group :
    (x : type-Group G)  Id (inv-Group G (inv-Group G x)) x
  inv-inv-Group x =
    is-injective-mul-Group
      ( inv-Group G x)
      ( ( right-inverse-law-mul-Group G (inv-Group G x)) 
        ( inv (left-inverse-law-mul-Group G x)))

Inverting elements of a group is an equivalence

  is-equiv-inv-Group : is-equiv (inv-Group G)
  is-equiv-inv-Group = is-equiv-is-involution inv-inv-Group

  equiv-equiv-inv-Group : type-Group G  type-Group G
  pr1 equiv-equiv-inv-Group = inv-Group G
  pr2 equiv-equiv-inv-Group = is-equiv-inv-Group

Two elements x and y are equal iff x⁻¹y=1

  eq-is-unit-left-div-Group :
    {x y : type-Group G}  is-unit-Group G (left-div-Group x y)  x  y
  eq-is-unit-left-div-Group {x} {y} H =
    ( inv (right-unit-law-mul-Group G x)) 
    ( inv-transpose-eq-mul-Group' (inv H))

  is-unit-left-div-eq-Group :
    {x y : type-Group G}  x  y  is-unit-Group G (left-div-Group x y)
  is-unit-left-div-eq-Group refl = left-inverse-law-mul-Group G _

Two elements x and y are equal iff xy⁻¹=1

  eq-is-unit-right-div-Group :
    {x y : type-Group G}  is-unit-Group G (right-div-Group x y)  x  y
  eq-is-unit-right-div-Group H =
    inv (inv-transpose-eq-mul-Group (inv H))  left-unit-law-mul-Group G _

  is-unit-right-div-eq-Group :
    {x y : type-Group G}  x  y  is-unit-Group G (right-div-Group x y)
  is-unit-right-div-eq-Group refl = right-inverse-law-mul-Group G _

The inverse of x⁻¹y is y⁻¹x

  inv-left-div-Group :
    (x y : type-Group G) 
    inv-Group G (left-div-Group x y)  left-div-Group y x
  inv-left-div-Group x y =
    equational-reasoning
      inv-Group G (left-div-Group x y)
       left-div-Group y (inv-Group G (inv-Group G x))
        by distributive-inv-mul-Group (inv-Group G x) y
       left-div-Group y x
        by ap (left-div-Group y) (inv-inv-Group x)

The inverse of xy⁻¹ is yx⁻¹

  inv-right-div-Group :
    (x y : type-Group G) 
    inv-Group G (right-div-Group x y)  right-div-Group y x
  inv-right-div-Group x y =
    equational-reasoning
      inv-Group G (right-div-Group x y)
       right-div-Group (inv-Group G (inv-Group G y)) x
        by distributive-inv-mul-Group x (inv-Group G y)
       right-div-Group y x
        by ap (mul-Group' G (inv-Group G x)) (inv-inv-Group y)

The multiple of x⁻¹y and y⁻¹z is x⁻¹z

  mul-left-div-Group :
    (x y z : type-Group G) 
    mul-Group G (left-div-Group x y) (left-div-Group y z)  left-div-Group x z
  mul-left-div-Group x y z =
    equational-reasoning
      mul-Group G (left-div-Group x y) (left-div-Group y z)
       mul-Group G (inv-Group G x) (mul-Group G y (left-div-Group y z))
        by associative-mul-Group G (inv-Group G x) y (left-div-Group y z)
       left-div-Group x z
        by ap (mul-Group G (inv-Group G x)) (issec-mul-inv-Group y z)

The multiple of xy⁻¹ and yz⁻¹ is xz⁻¹

  mul-right-div-Group :
    (x y z : type-Group G) 
    mul-Group G (right-div-Group x y) (right-div-Group y z) 
    right-div-Group x z
  mul-right-div-Group x y z =
    equational-reasoning
      mul-Group G (right-div-Group x y) (right-div-Group y z)
       mul-Group G x (mul-Group G (inv-Group G y) (right-div-Group y z))
        by associative-mul-Group G x (inv-Group G y) (right-div-Group y z)
       right-div-Group x z
        by ap (mul-Group G x) (isretr-mul-inv-Group y (inv-Group G z))

For any semigroup, being a group is a property

abstract
  all-elements-equal-is-group :
    {l : Level} (G : Semigroup l) (e : is-unital-Semigroup G) 
    all-elements-equal (is-group' G e)
  all-elements-equal-is-group
    ( pair G (pair μ associative-G))
    ( pair e (pair left-unit-G right-unit-G))
    ( pair i (pair left-inv-i right-inv-i))
    ( pair i' (pair left-inv-i' right-inv-i')) =
    eq-type-subtype
      ( λ i 
        prod-Prop
          ( Π-Prop (type-Set G)  x  Id-Prop G (μ (i x) x) e))
          ( Π-Prop (type-Set G)  x  Id-Prop G (μ x (i x)) e)))
      ( eq-htpy
        ( λ x  equational-reasoning
          i x
           μ e (i x)
            by inv (left-unit-G (i x))
           μ (μ (i' x) x) (i x)
            by ap  y  μ y (i x)) (inv (left-inv-i' x))
           μ (i' x) (μ x (i x))
            by associative-G (i' x) x (i x)
           μ (i' x) e
            by ap (μ (i' x)) (right-inv-i x)
           i' x
            by right-unit-G (i' x)))

abstract
  is-prop-is-group :
    {l : Level} (G : Semigroup l)  is-prop (is-group G)
  is-prop-is-group G =
    is-prop-Σ
      ( is-prop-is-unital-Semigroup G)
      ( λ e 
        is-prop-all-elements-equal (all-elements-equal-is-group G e))

is-group-Prop : {l : Level} (G : Semigroup l)  Prop l
pr1 (is-group-Prop G) = is-group G
pr2 (is-group-Prop G) = is-prop-is-group G

Any idempotent element in a group is the unit

module _
  {l : Level} (G : Group l)
  where

  is-idempotent-Group : type-Group G  UU l
  is-idempotent-Group x = Id (mul-Group G x x) x

  is-unit-is-idempotent-Group :
    {x : type-Group G}  is-idempotent-Group x  is-unit-Group G x
  is-unit-is-idempotent-Group {x} p =
    is-injective-mul-Group G x (p  inv (right-unit-law-mul-Group G x))

Multiplication of a list of elements in a group

module _
  {l : Level} (G : Group l)
  where

  mul-list-Group : list (type-Group G)  type-Group G
  mul-list-Group = mul-list-Monoid (monoid-Group G)

  preserves-concat-mul-list-Group :
    (l1 l2 : list (type-Group G)) 
    Id
      ( mul-list-Group (concat-list l1 l2))
      ( mul-Group G (mul-list-Group l1) (mul-list-Group l2))
  preserves-concat-mul-list-Group =
    distributive-mul-concat-list-Monoid (monoid-Group G)

Any group element yields a type equipped with an automorphism

module _
  {l : Level} (G : Group l) (g : type-Group G)
  where

  pointed-type-with-aut-Group : Pointed-Type-With-Aut l
  pr1 pointed-type-with-aut-Group = pointed-type-Group G
  pr2 pointed-type-with-aut-Group = equiv-mul-Group G g