module Algebra.Group where


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
    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) $
  ,β‚š funext (Ξ» a β†’
      monoid-inverse-unique x.has-is-monoid a _ _
        (y.inverser βˆ™ sym 1x=1y))
  ,β‚š prop!
    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)

    : βˆ€ {β„“} {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
    _⋆_ : 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.

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

    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:

    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)

  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.

  : βˆ€ {β„“} (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
    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

    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)