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 β€œ is a group” is a statement about having a certain property (namely, being a group), not structure on

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

There is also a map which assigns to each element its inverse and this inverse must multiply with to give the unit, both on the left and on the right:

    inverse : A β†’ A

    has-is-monoid : is-monoid unit _*_
    inversel : {x : A} β†’ inverse x * x ≑ unit
    inverser : {x : A} β†’ x * inverse x ≑ unit

  open is-monoid has-is-monoid public

Note that any element of determines two bijections on the underlying set of by multiplication with on the left and on the right. The inverse of this bijection is given by multiplication with and the proof that these are in fact inverse functions are given by the group laws:

  ⋆-equivl : βˆ€ x β†’ is-equiv (x *_)
  ⋆-equivl x = is-isoβ†’is-equiv (iso (inverse x *_)
    (Ξ» _ β†’ cancell inverser) Ξ» _ β†’ cancell inversel)

  ⋆-equivr : βˆ€ y β†’ is-equiv (_* y)
  ⋆-equivr y = is-isoβ†’is-equiv (iso (_* inverse y)
    (Ξ» _ β†’ cancelr inversel) Ξ» _ β†’ cancelr inverser)

is-group is propositionalπŸ”—

Showing that is-group takes values in propositions is straightforward, but, fortunately, very easy to automate: Our automation takes care of all the propositional components, and we’ve already established that units and inverses (thus inverse-assigning maps) are unique in a monoid.

private unquoteDecl eqv = declare-record-iso eqv (quote is-group)

is-group-is-prop : βˆ€ {β„“} {A : Type β„“} {_*_ : A β†’ A β†’ A}
                 β†’ is-prop (is-group _*_)
is-group-is-prop {A = A} x y = Equiv.injective (Iso→Equiv eqv) $
     1x=1y
  ,β‚š funext (Ξ» a β†’
      monoid-inverse-unique x.has-is-monoid a _ _
        x.inversel
        (y.inverser βˆ™ sym 1x=1y))
  ,β‚š prop!
  where
    module x = is-group x
    module y = is-group y hiding (magma-hlevel)
    A-hl : βˆ€ {n} β†’ H-Level A (2 + n)
    A-hl = basic-instance {T = A} 2 (x .is-group.has-is-set)
    1x=1y = identities-equal _ _
      (is-monoid→is-unital-magma x.has-is-monoid)
      (is-monoid→is-unital-magma y.has-is-monoid)

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 35 _⁻¹

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

  open is-group has-is-group public

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

record
  is-group-hom
    {β„“ β„“'} {A : Type β„“} {B : Type β„“'}
    (G : Group-on A) (G' : Group-on B) (e : A β†’ B) : Type (β„“ βŠ” β„“') where
  private
    module A = Group-on G
    module B = Group-on G'

  field
    pres-⋆ : (x y : A) β†’ 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.inverser βŸ©β‰‘Λ˜
    e 1A B.⋆ (e 1A B.β€” e 1A)   β‰‘βŸ¨ B.associative βŸ©β‰‘
    ⌜ e 1A B.⋆ e 1A ⌝ B.β€” e 1A β‰‘βŸ¨ ap! (sym (pres-⋆ _ _) βˆ™ ap e A.idl) βŸ©β‰‘
    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! 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 : Ξ£ (Type β„“) Group-on) (e : A .fst ≃ B .fst) β†’ Type β„“
Group≃ A B (f , _) = is-group-hom (A .snd) (B .snd) f

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

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.

record make-group {β„“} (G : Type β„“) : Type β„“ where
  no-eta-equality
  field
    group-is-set : is-set G
    unit : G
    mul  : G β†’ G β†’ G
    inv  : G β†’ G

    assoc : βˆ€ x y z β†’ mul x (mul y z) ≑ mul (mul x y) z
    invl  : βˆ€ x β†’ mul (inv x) x ≑ unit
    idl   : βˆ€ x β†’ mul unit x ≑ x

  private
    inverser : βˆ€ x β†’ mul x (inv x) ≑ unit
    inverser x =
      mul x (inv x)                                   β‰‘Λ˜βŸ¨ idl _ βŸ©β‰‘Λ˜
      mul unit (mul x (inv x))                        β‰‘Λ˜βŸ¨ apβ‚‚ mul (invl _) refl βŸ©β‰‘Λ˜
      mul (mul (inv (inv x)) (inv x)) (mul x (inv x)) β‰‘Λ˜βŸ¨ assoc _ _ _ βŸ©β‰‘Λ˜
      mul (inv (inv x)) (mul (inv x) (mul x (inv x))) β‰‘βŸ¨ apβ‚‚ mul refl (assoc _ _ _) βŸ©β‰‘
      mul (inv (inv x)) (mul (mul (inv x) x) (inv x)) β‰‘βŸ¨ apβ‚‚ mul refl (apβ‚‚ mul (invl _) refl) βŸ©β‰‘
      mul (inv (inv x)) (mul unit (inv x))            β‰‘βŸ¨ apβ‚‚ mul refl (idl _) βŸ©β‰‘
      mul (inv (inv x)) (inv x)                       β‰‘βŸ¨ invl _ βŸ©β‰‘
      unit                                            ∎

  to-group-on : Group-on G
  to-group-on .Group-on._⋆_ = mul
  to-group-on .Group-on.has-is-group .is-group.unit = unit
  to-group-on .Group-on.has-is-group .is-group.inverse = inv
  to-group-on .Group-on.has-is-group .is-group.inversel = invl _
  to-group-on .Group-on.has-is-group .is-group.inverser = inverser _
  to-group-on .Group-on.has-is-group .is-group.has-is-monoid .is-monoid.idl {x} = idl x
  to-group-on .Group-on.has-is-group .is-group.has-is-monoid .is-monoid.idr {x} =
    mul x ⌜ unit ⌝           β‰‘Λ˜βŸ¨ apΒ‘ (invl x) βŸ©β‰‘Λ˜
    mul x (mul (inv x) x)    β‰‘βŸ¨ assoc _ _ _ βŸ©β‰‘
    mul ⌜ mul x (inv x) ⌝ x  β‰‘βŸ¨ ap! (inverser x) βŸ©β‰‘
    mul unit x               β‰‘βŸ¨ idl x βŸ©β‰‘
    x                        ∎
  to-group-on .Group-on.has-is-group .is-group.has-is-monoid .has-is-semigroup =
    record { has-is-magma = record { has-is-set = group-is-set }
           ; associative = Ξ» {x y z} β†’ assoc x y z
           }

open make-group using (to-group-on) public

Symmetric groupsπŸ”—

If is a set, then the type of all bijections is also a set, and it forms the carrier for a group: The symmetric group on

Sym : βˆ€ {β„“} (X : Set β„“) β†’ Group-on (∣ X ∣ ≃ ∣ X ∣)
Sym X = to-group-on group-str where
  open make-group
  group-str : make-group (∣ X ∣ ≃ ∣ X ∣)
  group-str .mul g f = f βˆ™e g

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

  group-str .unit = id , id-equiv

This type is a set because is a set (because is a set by assumption), and being an equivalence is a proposition.

  group-str .group-is-set = hlevel!

The associativity and identity laws hold definitionally.

  group-str .assoc _ _ _ = trivial!
  group-str .idl _ = trivial!

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 .inv = _e⁻¹
  group-str .invl (f , eqv) = ext (equiv→unit eqv)