{-# OPTIONS -vtactic.hlevel:10 #-}
open import 1Lab.Prelude

open import Algebra.Magma.Unital hiding (idl ; idr)
open import Algebra.Semigroup
open import Algebra.Monoid
open import Algebra.Magma

import Algebra.Monoid.Reasoning as Mon

open is-monoid hiding (idl ; idr)

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

  infixr 20 _β€”_
  _β€”_ : A β†’ A β†’ A
  x β€” y = x * inverse y

  abstract
    inv-unit : inverse unit ≑ unit
    inv-unit = monoid-inverse-unique
      has-is-monoid unit _ _ inversel (has-is-monoid .is-monoid.idl)

    inv-inv : βˆ€ {x} β†’ inverse (inverse x) ≑ x
    inv-inv = monoid-inverse-unique
      has-is-monoid _ _ _ inversel inversel

    inv-comm : βˆ€ {x y} β†’ inverse (x * y) ≑ inverse y β€” x
    inv-comm {x = x} {y} =
      monoid-inverse-unique has-is-monoid _ _ _ inversel p
      where
        p : (x * y) * (inverse y β€” x) ≑ unit
        p = associative has-is-monoid
         βˆ™βˆ™ apβ‚‚ _*_
              (  sym (associative has-is-monoid)
              βˆ™βˆ™ apβ‚‚ _*_ refl inverser
              βˆ™βˆ™ has-is-monoid .is-monoid.idr)
              refl
         βˆ™βˆ™ inverser

    zero-diff : βˆ€ {x y} β†’ x β€” y ≑ unit β†’ x ≑ y
    zero-diff {x = x} {y = y} p =
      monoid-inverse-unique has-is-monoid _ _ _ p inversel

  underlying-monoid : Monoid β„“
  underlying-monoid = A , record
    { identity = unit ; _⋆_ = _*_ ; has-is-monoid = has-is-monoid }

  open Mon underlying-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 = Iso.injective 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 and inverses:

  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                 ∎

is-group-hom-is-prop
  : βˆ€ {β„“ β„“'} {A : Type β„“} {B : Type β„“'}
      {G : Group-on A} {H : Group-on B} {f}
  β†’ is-prop (is-group-hom G H f)
is-group-hom-is-prop {H = H} a b i .is-group-hom.pres-⋆ x y =
  Group-on.has-is-set H _ _ (a .is-group-hom.pres-⋆ x y) (b .is-group-hom.pres-⋆ x y) i

instance
  H-Level-group-hom
    : βˆ€ {n} {β„“ β„“'} {A : Type β„“} {B : Type β„“'}
      {G : Group-on A} {H : Group-on B} {f}
    β†’ H-Level (is-group-hom G H f) (suc n)
  H-Level-group-hom = prop-instance is-group-hom-is-prop

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
    invr : βˆ€ x β†’ mul x (inv x) ≑ unit
    invr 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-is-group : is-group mul
  to-is-group .is-group.unit = unit
  to-is-group .is-group.inverse = inv
  to-is-group .is-group.inversel = invl _
  to-is-group .is-group.inverser = invr _
  to-is-group .is-group.has-is-monoid .is-monoid.idl {x} = idl x
  to-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! (invr x) βŸ©β‰‘
    mul unit x               β‰‘βŸ¨ idl x βŸ©β‰‘
    x                        ∎
  to-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
           }

  to-group-on : Group-on G
  to-group-on .Group-on._⋆_ = mul
  to-group-on .Group-on.has-is-group = to-is-group

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