open import 1Lab.Prelude

open import Algebra.Magma.Unital
open import Algebra.Semigroup
open import Algebra.Monoid
open import Algebra.Magma

open import Cat.Instances.Delooping

import Cat.Reasoning

module Algebra.Group where

GroupsπŸ”—

A group is a monoid that has inverses for every element. The inverse for an element is necessarily, unique; Thus, to say that β€œ(G,⋆)(G, \star) is a group” is a statement about (G,⋆)(G, \star) having a certain property (namely, being a group), not structure on (G,⋆)(G, \star).

Furthermore, since group homomorphisms automatically preserve this structure, we are justified in calling this property rather than property-like structure.

In particular, for a binary operator to be a group operator, it has to be a monoid, meaning it must have a unit.

record is-group {β„“} {A : Type β„“} (_*_ : A β†’ A β†’ A) : Type β„“ where
  no-eta-equality
  field
    unit : A
    has-is-monoid : is-monoid unit _*_

There is also a map which assigns to each element xx its inverse xβˆ’1x^{-1}, and this inverse must multiply with xx to give the unit, both on the left and on the right:

    inverse : A β†’ A

    inversel : {x : A} β†’ inverse x * x ≑ unit
    inverser : {x : A} β†’ x * inverse x ≑ unit

  open is-monoid has-is-monoid public

is-group is propositionalπŸ”—

Showing that is-group takes values in propositions is straightforward, but tedious. Suppose that x,yx, y are both witnesses of is-group for the same operator; We’ll build a path x=yx = y.

is-group-is-prop : βˆ€ {β„“} {A : Type β„“} {_*_ : A β†’ A β†’ A}
                 β†’ is-prop (is-group _*_)
is-group-is-prop {A = A} {_*_ = _*_} x y = path where

We begin by constructing a line showing that the underlying monoid structures are identical – but since these have different types, we must also show that the units are the same.

  same-unit : x .unit ≑ y .unit
  same-unit =
    identities-equal (x .unit) (y .unit)
      (is-monoid→is-unital-magma (x .has-is-monoid))
      (is-monoid→is-unital-magma (y .has-is-monoid))

We then use the fact that is-monoid is a proposition to conclude that the monoid structures underlying xx and yy are the same.

  same-monoid : PathP (Ξ» i β†’ is-monoid (same-unit i) _*_)
                      (x .has-is-monoid) (y .has-is-monoid)
  same-monoid =
    is-prop→pathp (λ i → hlevel {T = is-monoid (same-unit i) _*_} 1)
      (x .has-is-monoid) (y .has-is-monoid)

Since inverses in monoids are unique (when they exist), it follows that the inverse-assigning maps are pointwise equal; By extensionality, they are the same map.

  same-inverses : (e : A) β†’ x .inverse e ≑ y .inverse e
  same-inverses e =
    monoid-inverse-unique (y .has-is-monoid) _ _ _
      (x .inversel βˆ™ same-unit) (y .inverser)

Since the underlying type of a group is a set, we have that any parallel paths are equal - even when the paths are dependent! This gives us the equations between the inversel and inverser fields of x and y.

  same-invl : (e : A) β†’ Square _ _ _ _
  same-invl e =
    is-set→squarep (λ _ _ → x .has-is-monoid .has-is-set)
      (apβ‚‚ _*_ (same-inverses e) refl) (x .inversel) (y .inversel) same-unit

  same-invr : (e : A) β†’ Square _ _ _ _
  same-invr e =
    is-set→squarep (λ _ _ → x .has-is-monoid .has-is-set)
      (apβ‚‚ _*_ refl (same-inverses e)) (x .inverser) (y .inverser) same-unit

Putting all of this together lets us conclude that x and y are identical.

  path : x ≑ y
  path i .unit         = same-unit i
  path i .has-is-monoid  = same-monoid i
  path i .inverse e    = same-inverses e i
  path i .inversel {e} = same-invl e i
  path i .inverser {e} = same-invr e i

instance
  H-Level-is-group
    : βˆ€ {β„“} {G : Type β„“} {_+_ : G β†’ G β†’ G} {n}
    β†’ H-Level (is-group _+_) (suc n)
  H-Level-is-group = prop-instance is-group-is-prop

Group HomomorphismsπŸ”—

In contrast with monoid homomorphisms, for group homomorphisms, it is not necessary for the underlying map to explicitly preserve the unit (and the inverses); It is sufficient for the map to preserve the multiplication.

As a stepping stone, we define what it means to equip a type with a group structure: a group structure on a type.

record Group-on {β„“} (A : Type β„“) : Type β„“ where
  field
    _⋆_ : A β†’ A β†’ A
    has-is-group : is-group _⋆_

  infixr 20 _⋆_
  infixl 30 _⁻¹

  _⁻¹ : A β†’ A
  x ⁻¹ = inverse has-is-group x

  open is-group has-is-group public

open Group-on

Group : (β„“ : Level) β†’ Type (lsuc β„“)
Group β„“ = Ξ£ Group-on

We have that a map is a group homomorphism if it preserves the multiplication.

record
  Group-hom {β„“} (A B : Group β„“) (e : A .fst β†’ B .fst) : Type β„“ where
  private
    module A = Group-on (A .snd)
    module B = Group-on (B .snd)

  field
    pres-⋆ : (x y : A .fst) β†’ e (x A.⋆ y) ≑ e x B.⋆ e y

A tedious calculation shows that this is sufficient to preserve the identity:

  private
    1A = A.unit
    1B = B.unit

  pres-id : e 1A ≑ 1B
  pres-id =
    e 1A                     β‰‘βŸ¨ sym B.idr βŸ©β‰‘
    e 1A B.⋆ 1B              β‰‘βŸ¨ apβ‚‚ B._⋆_ refl (sym B.inverser) βŸ©β‰‘
    e 1A B.⋆ (e 1A B.β€” e 1A) β‰‘βŸ¨ B.associative βŸ©β‰‘
    (e 1A B.⋆ e 1A) B.β€” e 1A β‰‘βŸ¨ apβ‚‚ B._⋆_ (sym (pres-⋆ _ _) βˆ™ ap e A.idl) refl βŸ©β‰‘
    e 1A B.β€” e 1A            β‰‘βŸ¨ B.inverser βŸ©β‰‘
    1B                       ∎

  pres-inv : βˆ€ {x} β†’ e (A.inverse x) ≑ B.inverse (e x)
  pres-inv {x} =
    monoid-inverse-unique B.has-is-monoid (e x) _ _
      (sym (pres-⋆ _ _) Β·Β· ap e A.inversel Β·Β· pres-id)
      B.inverser

  pres-diff : βˆ€ {x y} β†’ e (x A.β€” y) ≑ e x B.β€” e y
  pres-diff {x} {y} =
    e (x A.β€” y)             β‰‘βŸ¨ pres-⋆ _ _ βŸ©β‰‘
    e x B.⋆ e (A.inverse y) β‰‘βŸ¨ ap (_ B.⋆_) pres-inv βŸ©β‰‘
    e x B.β€” e y             ∎

An equivalence is an equivalence of groups when its underlying map is a group homomorphism.

Group≃ : βˆ€ {β„“} (A B : Group β„“) (e : A .fst ≃ B .fst) β†’ Type β„“
Group≃ A B (f , _) = Group-hom A B f

Group[_β‡’_] : βˆ€ {β„“} (A B : Group β„“) β†’ Type β„“
Group[ A β‡’ B ] = Ξ£ (Group-hom A B)

open Group-hom

We automatically derive the proof that paths between groups are homomorphic equivalences:

Group-univalent : βˆ€ {β„“} β†’ is-univalent {β„“ = β„“} (HomTβ†’Str Group≃)
Group-univalent {β„“ = β„“} =
  Derive-univalent-record (record-desc
    (Group-on {β„“ = β„“}) Group≃
    (record:
      field[ _⋆_         by pres-⋆ ]
      axiom[ has-is-group by (Ξ» _ β†’ is-group-is-prop) ]))

Making groupsπŸ”—

Since the interface of Group-on is very deeply nested, we introduce a helper function for arranging the data of a group into a record.

make-group
  : βˆ€ {β„“} {G : Type β„“}
  β†’ is-set G
  β†’ (unit : G) (_⋆_ : G β†’ G β†’ G) (inv : G β†’ G)
  β†’ (βˆ€ x y z β†’ (x ⋆ y) ⋆ z ≑ x ⋆ (y ⋆ z))
  β†’ (βˆ€ x β†’ inv x ⋆ x ≑ unit) β†’ (βˆ€ x β†’ x ⋆ inv x ≑ unit)
  β†’ (βˆ€ x β†’ unit ⋆ x ≑ x)
  β†’ Group-on G
make-group gset id star inv assoc invl invr g-idl = r where
  open is-group

  r : Group-on _
  r ._⋆_ = star
  r .has-is-group .unit = id
  r .has-is-group .has-is-monoid .has-is-semigroup .has-is-magma .has-is-set = gset
  r .has-is-group .has-is-monoid .has-is-semigroup .associative = sym (assoc _ _ _)
  r .has-is-group .has-is-monoid .idl = g-idl _
  r .has-is-group .has-is-monoid .idr {x = x} =
    star x id               β‰‘βŸ¨ apβ‚‚ star refl (sym (invl x)) βŸ©β‰‘
    star x (star (inv x) x) β‰‘βŸ¨ sym (assoc _ _ _) βŸ©β‰‘
    star (star x (inv x)) x β‰‘βŸ¨ apβ‚‚ star (invr x) refl βŸ©β‰‘
    star id x               β‰‘βŸ¨ g-idl x βŸ©β‰‘
    x                       ∎
  r .has-is-group .inverse = inv
  r .has-is-group .inversel = invl _
  r .has-is-group .inverser = invr _

Symmetric GroupsπŸ”—

If XX is a set, then the type of all bijections X≃XX \simeq X is also a set, and it forms the carrier for a group: The symmetric group on XX.

Sym : βˆ€ {β„“} β†’ Set β„“ β†’ Group β„“
Sym X .fst = ∣ X ∣ ≃ ∣ X ∣
Sym X .snd = group-str where
  open n-Type X using (H-Level-n-type)
  group-str : Group-on (∣ X ∣ ≃ ∣ X ∣)
  group-str ._⋆_ g f = f βˆ™e g

The group operation is composition of equivalences; The identity element is the identity equivalence.

  group-str .has-is-group .unit = id , id-equiv

This type is a set because X→XX \to X is a set (because XX is a set by assumption), and being an equivalence is a proposition.

  group-str .has-is-group .has-is-monoid .has-is-semigroup .has-is-magma .has-is-set =
    hlevel 2

The associativity and identity laws hold definitionally.

  group-str .has-is-group .has-is-monoid .has-is-semigroup .associative =
    Ξ£-prop-path is-equiv-is-prop refl
  group-str .has-is-group .has-is-monoid .idl = Ξ£-prop-path is-equiv-is-prop refl
  group-str .has-is-group .has-is-monoid .idr = Ξ£-prop-path is-equiv-is-prop refl

The inverse is given by the inverse equivalence, and the inverse equations hold by the fact that the inverse of an equivalence is both a section and a retraction.

  group-str .has-is-group .inverse = _e⁻¹
  group-str .has-is-group .inversel {x = f , eqv} =
    Σ-prop-path is-equiv-is-prop (funext (equiv→retraction eqv))
  group-str .has-is-group .inverser {x = f , eqv} =
    Σ-prop-path is-equiv-is-prop (funext (equiv→section eqv))