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, \star)$ is a groupβ is a statement about $(G, \star)$ having a certain property (namely, being a group), not structure on $(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 $x$ its inverse $x^{-1}$, and this inverse must multiply with $x$ 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, y$ are both witnesses of is-group for the same operator; Weβll build a path $x = 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 $x$ and $y$ 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


# 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 $X$ is a set, then the type of all bijections $X \simeq X$ is also a set, and it forms the carrier for a group: The symmetric group on $X$.

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 \to X$ is a set (because $X$ 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))