Abstract groups

Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides, Eléonore Mangel, Victor Blanchi, favonia and Gregor Perčič.

Created on 2022-03-17.
Last modified on 2024-03-23.

module group-theory.groups where
Imports 
open import foundation.action-on-identifications-binary-functions
open import foundation.action-on-identifications-functions
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.function-types
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.invertible-elements-monoids
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.h-spaces
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-is-unital-Semigroup :
  {l : Level} (G : Semigroup l) → is-unital-Semigroup G → UU l
is-group-is-unital-Semigroup 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-Semigroup :
  {l : Level} (G : Semigroup l) → UU l
is-group-Semigroup G =
  Σ (is-unital-Semigroup G) (is-group-is-unital-Semigroup G)

The type of groups

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

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

  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 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 = x ＝ unit-Group

  is-unit-Group' : type-Group → UU l
  is-unit-Group' x = unit-Group ＝ x

  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-prop-is-unit-Group' : (x : type-Group) → is-prop (is-unit-Group' x)
  is-prop-is-unit-Group' x = is-set-type-Group unit-Group x

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

  is-unit-prop-Group' : type-Group → Prop l
  pr1 (is-unit-prop-Group' x) = is-unit-Group' x
  pr2 (is-unit-prop-Group' 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)

  coherence-unit-laws-mul-Group :
    left-unit-law-mul-Group unit-Group ＝ right-unit-law-mul-Group unit-Group
  coherence-unit-laws-mul-Group =
    eq-is-prop (is-set-type-Group _ _)

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

  h-space-Group : H-Space l
  pr1 h-space-Group = pointed-type-Group
  pr1 (pr2 h-space-Group) = mul-Group
  pr1 (pr2 (pr2 h-space-Group)) = left-unit-law-mul-Group
  pr1 (pr2 (pr2 (pr2 h-space-Group))) = right-unit-law-mul-Group
  pr2 (pr2 (pr2 (pr2 h-space-Group))) = coherence-unit-laws-mul-Group

  has-inverses-Group :
    is-group-is-unital-Semigroup 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)

  is-invertible-element-Group :
    (x : type-Group) → is-invertible-element-Monoid monoid-Group x
  pr1 (is-invertible-element-Group x) = inv-Group x
  pr1 (pr2 (is-invertible-element-Group x)) = right-inverse-law-mul-Group x
  pr2 (pr2 (is-invertible-element-Group x)) = left-inverse-law-mul-Group x

  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)

  left-swap-mul-Group :
    {x y z : type-Group} → mul-Group x y ＝ mul-Group y x →
    mul-Group x (mul-Group y z) ＝
    mul-Group y (mul-Group x z)
  left-swap-mul-Group =
    left-swap-mul-Semigroup semigroup-Group

  right-swap-mul-Group :
    {x y z : type-Group} → mul-Group y z ＝ mul-Group z y →
    mul-Group (mul-Group x y) z ＝
    mul-Group (mul-Group x z) y
  right-swap-mul-Group =
    right-swap-mul-Semigroup semigroup-Group

  interchange-mul-mul-Group :
    {x y z w : type-Group} → mul-Group y z ＝ mul-Group z y →
    mul-Group (mul-Group x y) (mul-Group z w) ＝
    mul-Group (mul-Group x z) (mul-Group y w)
  interchange-mul-mul-Group =
    interchange-mul-mul-Semigroup semigroup-Group

The structure of a group

structure-group :
  {l1 : Level} → UU l1 → UU l1
structure-group X =
  Σ ( structure-semigroup X)
    ( λ p → is-group-Semigroup (semigroup-structure-semigroup X p))

group-structure-group :
  {l1 : Level} → (X : UU l1) → structure-group X → Group l1
pr1 (group-structure-group X (p , q)) = semigroup-structure-semigroup X p
pr2 (group-structure-group X (p , q)) = q

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 =
    left-div-is-invertible-element-Monoid
      ( monoid-Group G)
      ( is-invertible-element-Group G x)

  ap-left-div-Group :
    {x x' y y' : type-Group G} → x ＝ x' → y ＝ y' →
    left-div-Group x y ＝ left-div-Group x' y'
  ap-left-div-Group p q = ap-binary left-div-Group p q

  is-section-left-div-Group :
    (x : type-Group G) → (mul-Group G x ∘ left-div-Group x) ~ id
  is-section-left-div-Group x =
    is-section-left-div-is-invertible-element-Monoid
      ( monoid-Group G)
      ( is-invertible-element-Group G x)

  is-retraction-left-div-Group :
    (x : type-Group G) → (left-div-Group x ∘ mul-Group G x) ~ id
  is-retraction-left-div-Group x =
    is-retraction-left-div-is-invertible-element-Monoid
      ( monoid-Group G)
      ( is-invertible-element-Group G x)

  is-equiv-mul-Group : (x : type-Group G) → is-equiv (mul-Group G x)
  is-equiv-mul-Group x =
    is-equiv-mul-is-invertible-element-Monoid
      ( monoid-Group G)
      ( is-invertible-element-Group G 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

  is-equiv-left-div-Group : (x : type-Group G) → is-equiv (left-div-Group x)
  is-equiv-left-div-Group x =
    is-equiv-is-invertible
      ( mul-Group G x)
      ( is-retraction-left-div-Group x)
      ( is-section-left-div-Group x)

  equiv-left-div-Group : (x : type-Group G) → type-Group G ≃ type-Group G
  pr1 (equiv-left-div-Group x) = left-div-Group x
  pr2 (equiv-left-div-Group x) = is-equiv-left-div-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 =
    right-div-is-invertible-element-Monoid
      ( monoid-Group G)
      ( is-invertible-element-Group G y)
      ( x)

  ap-right-div-Group :
    {x x' y y' : type-Group G} → x ＝ x' → y ＝ y' →
    right-div-Group x y ＝ right-div-Group x' y'
  ap-right-div-Group p q = ap-binary right-div-Group p q

  is-section-right-div-Group :
    (x : type-Group G) → (mul-Group' G x ∘ (λ y → right-div-Group y x)) ~ id
  is-section-right-div-Group x =
    is-section-right-div-is-invertible-element-Monoid
      ( monoid-Group G)
      ( is-invertible-element-Group G x)

  is-retraction-right-div-Group :
    (x : type-Group G) → ((λ y → right-div-Group y x) ∘ mul-Group' G x) ~ id
  is-retraction-right-div-Group x =
    is-retraction-right-div-is-invertible-element-Monoid
      ( monoid-Group G)
      ( is-invertible-element-Group G x)

  is-equiv-mul-Group' : (x : type-Group G) → is-equiv (mul-Group' G x)
  is-equiv-mul-Group' x =
    is-equiv-is-invertible
      ( λ y → right-div-Group y x)
      ( is-section-right-div-Group x)
      ( is-retraction-right-div-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

  is-equiv-right-div-Group :
    (x : type-Group G) → is-equiv (λ y → right-div-Group y x)
  is-equiv-right-div-Group x =
    is-equiv-is-invertible
      ( mul-Group' G x)
      ( is-retraction-right-div-Group x)
      ( is-section-right-div-Group x)

  equiv-right-div-Group :
    (x : type-Group G) → type-Group G ≃ type-Group G
  pr1 (equiv-right-div-Group x) y = right-div-Group y x
  pr2 (equiv-right-div-Group x) = is-equiv-right-div-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 ＝ right-div-Group z y
  transpose-eq-mul-Group {x} {y} {z} refl =
    inv (is-retraction-right-div-Group y x)

  inv-transpose-eq-mul-Group :
    {x y z : type-Group G} → x ＝ right-div-Group z y → mul-Group G x y ＝ z
  inv-transpose-eq-mul-Group {._} {y} {z} refl =
    is-section-right-div-Group y z

  transpose-eq-mul-Group' :
    {x y z : type-Group G} → mul-Group G x y ＝ z → y ＝ left-div-Group x z
  transpose-eq-mul-Group' {x} {y} {z} refl =
    inv (is-retraction-left-div-Group x y)

  inv-transpose-eq-mul-Group' :
    {x y z : type-Group G} → y ＝ left-div-Group x z → mul-Group G x y ＝ z
  inv-transpose-eq-mul-Group' {x} {y} {._} refl =
    is-section-left-div-Group x _

  double-transpose-eq-mul-Group :
    {x y z w : type-Group G} →
    mul-Group G y w ＝ mul-Group G x z →
    left-div-Group x y ＝ right-div-Group z w
  double-transpose-eq-mul-Group p =
    inv
      ( transpose-eq-mul-Group'
        ( inv (transpose-eq-mul-Group p ∙ associative-mul-Group G _ _ _)))

  double-transpose-eq-mul-Group' :
    {x y z w : type-Group G} →
    mul-Group G z x ＝ mul-Group G w y →
    right-div-Group x y ＝ left-div-Group z w
  double-transpose-eq-mul-Group' p =
    inv (double-transpose-eq-mul-Group (inv p))

Distributivity of inverses over multiplication

  distributive-inv-mul-Group :
    {x y : type-Group G} →
    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)))

  distributive-inv-mul-Group' :
    (x y : type-Group G) → mul-Group G x y ＝ mul-Group G y x →
    inv-Group G (mul-Group G x y) ＝ mul-Group G (inv-Group G x) (inv-Group G y)
  distributive-inv-mul-Group' x y H =
    ( distributive-inv-mul-Group) ∙
    ( inv (double-transpose-eq-mul-Group (double-transpose-eq-mul-Group H)))

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

  transpose-eq-inv-Group :
    {x y : type-Group G} →
    inv-Group G x ＝ y → x ＝ inv-Group G y
  transpose-eq-inv-Group refl = inv (inv-inv-Group _)

  transpose-eq-inv-Group' :
    {x y : type-Group G} →
    x ＝ inv-Group G y → inv-Group G x ＝ y
  transpose-eq-inv-Group' refl = inv-inv-Group _

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
      ＝ 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
      ＝ right-div-Group y x
        by ap (mul-Group' G (inv-Group G x)) (inv-inv-Group y)

The product 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 (left-div-Group x) (is-section-left-div-Group y z)

The product 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) (is-retraction-left-div-Group y (inv-Group G z))

For any semigroup, being a group is a property

abstract
  all-elements-equal-is-group-Semigroup :
    {l : Level} (G : Semigroup l) (e : is-unital-Semigroup G) →
    all-elements-equal (is-group-is-unital-Semigroup G e)
  all-elements-equal-is-group-Semigroup
    ( 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 →
        product-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-Semigroup :
    {l : Level} (G : Semigroup l) → is-prop (is-group-Semigroup G)
  is-prop-is-group-Semigroup G =
    is-prop-Σ
      ( is-prop-is-unital-Semigroup G)
      ( λ e →
        is-prop-all-elements-equal (all-elements-equal-is-group-Semigroup G e))

is-group-prop-Semigroup : {l : Level} (G : Semigroup l) → Prop l
pr1 (is-group-prop-Semigroup G) = is-group-Semigroup G
pr2 (is-group-prop-Semigroup G) = is-prop-is-group-Semigroup 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

Recent changes