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 β€œ(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
    unit : A

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

    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

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 ; module HLevel-instance)
    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 30 _⁻¹

  _⁻¹ : 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 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 : βˆ€ {β„“} (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 X→XX \to X is a set (because XX 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 _ _ _ = Ξ£-prop-path is-equiv-is-prop refl
  group-str .idl _ = Ξ£-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 .inv = _e⁻¹
  group-str .invl (f , eqv) =
    Σ-prop-path is-equiv-is-prop (funext (equiv→unit eqv))