open import Algebra.Group.Cat.Base
open import Algebra.Group

open import Cat.Functor.Properties
open import Cat.Prelude hiding (_*_ ; _+_)

import Cat.Reasoning

module Algebra.Group.Ab where

Abelian groupsπŸ”—

A very important class of groups (which includes most familiar examples of groups: the integers, all finite cyclic groups, etc) are those with a commutative group operation, that is, those for which Accordingly, these have a name reflecting their importance and ubiquity: They are called commutative groups. Just kidding! They’re named abelian groups, named after a person, because nothing can have self-explicative names in mathematics. It’s the law.

private variable
  β„“ : Level
  G : Type β„“

Group-on-is-abelian : Group-on G β†’ Type _
Group-on-is-abelian G = βˆ€ x y β†’ Group-on._⋆_ G x y ≑ Group-on._⋆_ G y x

Group-on-is-abelian-is-prop : (g : Group-on G) β†’ is-prop (Group-on-is-abelian g)
Group-on-is-abelian-is-prop g = Ξ -is-hlevelΒ² 1 Ξ» _ _ β†’ g .Group-on.has-is-set _ _

This module does the usual algebraic structure dance to set up the category of Abelian groups.

record is-abelian-group (_*_ : G β†’ G β†’ G) : Type (level-of G) where
  no-eta-equality
  field
    has-is-group : is-group _*_
    commutes     : βˆ€ {x y} β†’ x * y ≑ y * x
  open is-group has-is-group renaming (unit to 1g) public

  equal-sumβ†’equal-diff : βˆ€ a b c d β†’ a * b ≑ c * d β†’ a β€” c ≑ d β€” b
  equal-sumβ†’equal-diff a b c d p = commutes βˆ™ swizzle p inverser inversel

private unquoteDecl eqv = declare-record-iso eqv (quote is-abelian-group)
instance
  H-Level-is-abelian-group
    : βˆ€ {n} {* : G β†’ G β†’ G} β†’ H-Level (is-abelian-group *) (suc n)
  H-Level-is-abelian-group = prop-instance $ Iso→is-hlevel 1 eqv $
    Ξ£-is-hlevel 1 (hlevel 1) Ξ» x β†’ Ξ -is-hlevelΒ²' 1 Ξ» _ _ β†’
      is-group.has-is-set x _ _

record Abelian-group-on (T : Type β„“) : Type β„“ where
  no-eta-equality
  field
    _*_       : T β†’ T β†’ T
    has-is-ab : is-abelian-group _*_
  open is-abelian-group has-is-ab renaming (inverse to infixl 30 _⁻¹) public

  Abelian→Group-on : Group-on T
  Abelianβ†’Group-on .Group-on._⋆_ = _*_
  Abelian→Group-on .Group-on.has-is-group = has-is-group

  Abelian→Group-on-abelian : Group-on-is-abelian Abelian→Group-on
  Abelian→Group-on-abelian _ _ = commutes

  infixr 20 _*_

open Abelian-group-on using (Abelian→Group-on; Abelian→Group-on-abelian) public

Abelian-group-structure : βˆ€ β„“ β†’ Thin-structure β„“ Abelian-group-on
∣ Abelian-group-structure β„“ .is-hom f G₁ Gβ‚‚ ∣ =
  is-group-hom (Abelianβ†’Group-on G₁) (Abelianβ†’Group-on Gβ‚‚) f
Abelian-group-structure β„“ .is-hom f G₁ Gβ‚‚ .is-tr = hlevel 1
Abelian-group-structure β„“ .id-is-hom .is-group-hom.pres-⋆ x y = refl
Abelian-group-structure β„“ .∘-is-hom f g Ξ± Ξ² .is-group-hom.pres-⋆ x y =
  ap f (Ξ² .is-group-hom.pres-⋆ x y) βˆ™ Ξ± .is-group-hom.pres-⋆ (g x) (g y)
Abelian-group-structure β„“ .id-hom-unique {s = s} {t} Ξ± _ = p where
  open Abelian-group-on

  p : s ≑ t
  p i ._*_ x y = Ξ± .is-group-hom.pres-⋆ x y i
  p i .has-is-ab = is-prop→pathp
    (Ξ» i β†’ hlevel {T = is-abelian-group (Ξ» x y β†’ p i ._*_ x y)} 1)
    (s .has-is-ab) (t .has-is-ab) i

Ab : βˆ€ β„“ β†’ Precategory (lsuc β„“) β„“
Ab β„“ = Structured-objects (Abelian-group-structure β„“)

module Ab {β„“} = Cat.Reasoning (Ab β„“)

instance
  Ab-equational : βˆ€ {β„“} β†’ is-equational (Abelian-group-structure β„“)
  Ab-equational .is-equational.invert-id-hom = Groups-equational .is-equational.invert-id-hom

Abelian-group : (β„“ : Level) β†’ Type (lsuc β„“)
Abelian-group _ = Ab.Ob

Abelianβ†’Group : βˆ€ {β„“} β†’ Abelian-group β„“ β†’ Group β„“
Abelian→Group G = G .fst , Abelian→Group-on (G .snd)

record make-abelian-group (T : Type β„“) : Type β„“ where
  no-eta-equality
  field
    ab-is-set : is-set T
    mul   : T β†’ T β†’ T
    inv   : T β†’ T
    1g    : T
    idl   : βˆ€ x β†’ mul 1g x ≑ x
    assoc : βˆ€ x y z β†’ mul x (mul y z) ≑ mul (mul x y) z
    invl  : βˆ€ x β†’ mul (inv x) x ≑ 1g
    comm  : βˆ€ x y β†’ mul x y ≑ mul y x

  make-abelian-group→make-group : make-group T
  make-abelian-group→make-group = mg where
    mg : make-group T
    mg .make-group.group-is-set = ab-is-set
    mg .make-group.unit   = 1g
    mg .make-group.mul    = mul
    mg .make-group.inv    = inv
    mg .make-group.assoc  = assoc
    mg .make-group.invl   = invl
    mg .make-group.idl    = idl

  to-group-on-ab : Group-on T
  to-group-on-ab = to-group-on make-abelian-group→make-group

  to-abelian-group-on : Abelian-group-on T
  to-abelian-group-on .Abelian-group-on._*_ = mul
  to-abelian-group-on .Abelian-group-on.has-is-ab .is-abelian-group.has-is-group =
    Group-on.has-is-group to-group-on-ab
  to-abelian-group-on .Abelian-group-on.has-is-ab .is-abelian-group.commutes =
    comm _ _

  to-ab : Abelian-group β„“
  ∣ to-ab .fst ∣ = T
  to-ab .fst .is-tr = ab-is-set
  to-ab .snd = to-abelian-group-on

is-commutative-group : βˆ€ {β„“} β†’ Group β„“ β†’ Type β„“
is-commutative-group G = Group-on-is-abelian (G .snd)

from-commutative-group
  : βˆ€ {β„“} (G : Group β„“)
  β†’ is-commutative-group G
  β†’ Abelian-group β„“
from-commutative-group G comm .fst = G .fst
from-commutative-group G comm .snd .Abelian-group-on._*_ =
  Group-on._⋆_ (G .snd)
from-commutative-group G comm .snd .Abelian-group-on.has-is-ab .is-abelian-group.has-is-group =
  Group-on.has-is-group (G .snd)
from-commutative-group G comm .snd .Abelian-group-on.has-is-ab .is-abelian-group.commutes =
  comm _ _

Grp→Ab→Grp
  : βˆ€ {β„“} (G : Group β„“) (c : is-commutative-group G)
  β†’ Abelianβ†’Group (from-commutative-group G c) ≑ G
Grp→Ab→Grp G c = Σ-pathp refl go where
  go : Abelianβ†’Group-on (from-commutative-group G c .snd) ≑ G .snd
  go i .Group-on._⋆_ = G .snd .Group-on._⋆_
  go i .Group-on.has-is-group = G .snd .Group-on.has-is-group

open make-abelian-group using (make-abelian-group→make-group ; to-group-on-ab ; to-abelian-group-on ; to-ab) public

open Functor

Abβ†ͺGrp : βˆ€ {β„“} β†’ Functor (Ab β„“) (Groups β„“)
Abβ†ͺGrp .Fβ‚€ = Abelianβ†’Group
Abβ†ͺGrp .F₁ f .hom = f .hom
Abβ†ͺGrp .F₁ f .preserves = f .preserves
Abβ†ͺGrp .F-id = trivial!
Abβ†ͺGrp .F-∘ f g = trivial!

Abβ†ͺGrp-is-ff : βˆ€ {β„“} β†’ is-fully-faithful (Abβ†ͺGrp {β„“})
Abβ†ͺGrp-is-ff {x = A} {B} = is-isoβ†’is-equiv $ iso
  promote (Ξ» _ β†’ trivial!) (Ξ» _ β†’ trivial!)
  where
    promote : Groups.Hom (Abelian→Group A) (Abelian→Group B) → Ab.Hom A B
    promote f .hom = f .hom
    promote f .preserves = f .preserves

Abβ†ͺSets : βˆ€ {β„“} β†’ Functor (Ab β„“) (Sets β„“)
Abβ†ͺSets = Grpβ†ͺSets F∘ Abβ†ͺGrp

The fundamental example of an abelian group is the group of integers.

Given an abelian group we can define the negation automorphism which inverts every element: since the group operation is commutative, we have so this is a homomorphism.

module _ {β„“} (G : Abelian-group β„“) where
  open Abelian-group-on (G .snd)

  negation : G Ab.β‰… G
  negation = total-iso
    (_⁻¹ , is-involutiveβ†’is-equiv (Ξ» _ β†’ inv-inv))
    (record { pres-⋆ = Ξ» x y β†’ inv-comm βˆ™ commutes })