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