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

open import Cat.Instances.Delooping

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 xy=yxxy = yx. Accordingly, these have a name reflecting their importance and ubiquity: They are called commutative groups. Just kidding! They’re named abelian groups, named after some dude, because nothing can have instructive names in mathematics. It’s the law.

The theory of abelian groups is generally simpler than that of arbitrary groups, and surprisingly the category Ab\ht{Ab} of abelian groups is better behaved than the category Grp\ht{Grp} of possibly non-commutative groups. This goes contrary to a common trade-off in category theory, that of a “category of nice objects” vs a “nice category of objects” (as an example, consider the category of fields: fields are very nice objects algebraically, but the category of fields is utterly terrible — but I digress).

We define the category Ab\ht{Ab} as the full subcategory of the category of groups consisting of those objects which are abelian groups.

Ab :    Precategory (lsuc ) 
Ab  = Restrict {C = Groups } is-abelian-group

module Ab {} = Cat (Ab )

AbGroup :    Type (lsuc )
AbGroup _ = Ab.Ob

This means that homomorphisms of abelian groups are the same as homomorphisms of their underlying groups: Commutativity of the operation is property, rather than structure. As a first example of the niceness of abelian groups (or perhaps the non-niceness of general groups), consider the following construction of a group of maps XGX \to G:

module _ { ℓ′} (X : Type ) (G : Group ℓ′) where private
  open Group-on (G .snd)

  Map-group : Group (  ℓ′)
  Map-group = _ , grp where
    grp : Group-on (X  G .fst)
    grp = make-group (hlevel 2)
       _  unit)
       f g x  f x  g x)
       f x  inverse (f x))
       f g h i x  associative {x = f x} {y = g x} {z = h x} (~ i))
       f i x  inversel {x = f x} i)
       f i x  inverser {x = f x} i)
       f i x  idl {x = f x} i)

This definition works fine for groups and maps of sets into a group, but maps of sets aren’t what we’re interested in when studying groups! We’d like to equip the set homGrp(A,B)\hom_{\ht{Grp}}(A, B) with a group structure induced by pointwise multiplication, but this turns out to be possible if, and only if, the groups involved are abelian. Let us skip the details of constructing the zero map, which is a group homomorphism since it is constantly zero, and skip to considering sums of maps:

  Hom-group : AbGroup 
  Hom-group = (T , grp) , abel where
    T = Ab.Hom A B
    add-map : T  T  T
    add-map (f , fh) (g , gh) .fst x = f x B.⋆ g x
    add-map (f , fh) (g , gh) .snd .p x y =
      f (x A.⋆ y) B.⋆ g (x A.⋆ y)     ≡⟨ ap₂ B._⋆_ (fh .p x y) (gh .p x y) 
      (f x B.⋆ f y) B.⋆ (g x B.⋆ g y) ≡⟨ solve-monoid B.underlying-monoid  
      f x B.⋆ (f y B.⋆ g x) B.⋆ g y   ≡⟨  i  f x B.⋆ B.commutative {x = f y} {y = g x} i B.⋆ g y) 
      f x B.⋆ (g x B.⋆ f y) B.⋆ g y   ≡⟨ solve-monoid B.underlying-monoid 
      (f x B.⋆ g x) B.⋆ (f y B.⋆ g y) 

Note the crucial third step in our calculation above: For the pointwise sum of two group homomorphisms to be a group homomorphism, we must have that f(y)g(x)=g(x)f(y)f(y)g(x) = g(x)f(y). We must also use commutativity to prove that the pointwise inverse of a group homomorphism is again a homomorphism, as is done in the calculation below.

    inv-map : T  T
    inv-map (f , fh) .fst x = f x B.⁻¹
    inv-map (f , fh) .snd .p x y =
      f (x A.⋆ y) ⁻¹   ≡⟨ ap B.inverse (fh .p _ _) 
      (f x B.⋆ f y) ⁻¹ ≡⟨ ap B.inverse B.commutative 
      (f y B.⋆ f x) ⁻¹ ≡⟨ B.inv-comm 
      (f x ⁻¹) B.— f y 

    grp : Group-on T
    grp = make-group (Ab.Hom-set A B)
      zero-map add-map inv-map
       f g h  Forget-is-faithful (funext λ x  sym B.associative))
       f  Forget-is-faithful (funext λ x  B.inversel))
       f  Forget-is-faithful (funext λ x  B.inverser))
       f  Forget-is-faithful (funext λ x  B.idl))

    abel : is-abelian-group (T , grp)
    abel f g = Forget-is-faithful (funext λ _  B.commutative)

By pre/post composition, the Hom-group construction extends to a functor Abop×AbAb\ht{Ab}\op \times \ht{Ab} \to \ht{Ab}, the internal hom\hom abelian group.

module _ {} where
  open Functor

  Ab-hom : Functor (Ab  ^op ×Cat Ab ) (Ab )
  Ab-hom .F₀ (A , B) = Hom-group A B
  Ab-hom .F₁ {x , y} {x′ , y′} (fh , gh) = f′ where
    module g = Group-hom (gh .snd)
    f′ : Groups.Hom (Hom-group x y .object) (Hom-group x′ y′ .object)
    f′ .fst h = gh Groups.∘ h Groups.∘ fh
    f′ .snd .Group-hom.pres-⋆ (m , mh) (n , nh) = Forget-is-faithful $ funext λ i
       g.pres-⋆ _ _

  Ab-hom .F-id = Forget-is-faithful $ funext λ i  Forget-is-faithful refl
  Ab-hom .F-∘ f g = Forget-is-faithful $ funext λ i  Forget-is-faithful refl

The tensor product🔗

We extend the category Ab\ht{Ab} defined above to a monoidal category by equipping it with the tensor product of abelian groups. Note that this is not the only notion of “product” in Ab\ht{Ab}; There is also the “direct (bi)product” of abelian groups. The tensor product has primacy because it defines a left adjoint to the internal hom\hom functor — that is, homs ABCA \otimes B \to C correspond to bilinear maps A,BCA, B \to C: functions which are “separately group homomorphisms in each variable”. By adjointness, these are the same as group homomorphisms A[B,C]A \to [B, C].

module _ {} (A B : AbGroup ) where
    module A = AbGrp A
    module B = AbGrp B

While the universal property of ABA \otimes B is simple enough to state, actually constructing it is… another matter entirely. We construct the underlying set of ABA \otimes B, written Tensor in the code, as a massive higher inductive type:

  • The first constructor is the inclusion A×BABA \times B \to A \otimes B which generates the tensor product (in fact, the tensor product is a kind of free group).
  data Tensor : Type  where
    _:,_     : A.₀  B.₀  Tensor
  • The next block of constructors ensures that Tensor is a group; We add “words” to Tensor, and identify them by the group axioms. Note that we don’t need x+0=xx + 0 = x as a constructor.
    :0       : Tensor
    _:+_     : Tensor  Tensor  Tensor
    :inv     : Tensor  Tensor
    t-squash : is-set Tensor
    t-invl   :  {x}  :inv x :+ x  :0
    t-invr   :  {x}  x :+ :inv x  :0
    t-idl    :  {x}  :0 :+ x  x
    t-assoc  :  {x y z}  (x :+ y) :+ z  x :+ (y :+ z)
  • The next constructor ensures that Tensor is abelian, and
    t-comm   :  {x y}  x :+ y  y :+ x
  • The last two constructors encode the “universal multi-linearity”: The group operation of the tensor product, with one coordinate fixed, is identified with the group operation of that factor.
    t-fixl   :  {x y z}  (x :, y) :+ (x :, z)  (x :, (y B.⋆ z))
    t-fixr   :  {x y z}  (x :, z) :+ (y :, z)  ((x A.⋆ y) :, z)

These constructors all conspire to make an abelian group ABA \otimes B.

  _⊗_ : AbGroup 
  _⊗_ =
    ( Tensor
    , make-group t-squash :0 _:+_ :inv
         _ _ _  t-assoc)
         _  t-invl)
         _  t-invr)
         _  t-idl))
    , λ x y  t-comm

All of those path constructors impose restrictions on mapping out of ABA \otimes B, to the point where actually writing down its induction principle would be wildly unpractical. Instead, we only write down the (non-dependent) universal property: if f:A×BCf : A \times B \to C is a function of sets such that f(xy,z)=f(x,z)f(y,z)f(xy, z) = f(x, z)f(y, z) and f(x,yz)=f(x,y)f(x,z)f(x, yz) = f(x, y)f(x, z), then it extends to an abelian group homomorphism hom(AB,C)\hom(A \otimes B, C).

    : (f : A.₀  B.₀  C.₀)
     (∀ x y z  f (x A.⋆ y) z  f x z C.⋆ f y z)
     (∀ x y z  f z (x B.⋆ y)  f z x C.⋆ f z y)
     Ab.Hom (A  B) C
  from-multilinear-map f fixr fixl = go , record { pres-⋆ = λ _ _  refl } where
    go : Tensor A B  C.₀
    go (x :, y) = f x y
    go (t-fixl  {x} {y} {z} i) = fixl y z x (~ i)
    go (t-fixr  {x} {y} {z} i) = fixr x y z (~ i)

These multilinear maps are given by exactly the same data as a group homomorphism hom(A,[B,C])\hom(A, [B, C]), just packaged differently. By unpacking and re-packing that data, we can also turn those homomorphisms into ones hom(AB,C)\hom(A \otimes B, C).

  from-ab-hom : (map : Ab.Hom A (Hom-group B C))  Ab.Hom (A  B) C
  from-ab-hom map = from-multilinear-map  x y  map .fst x .fst y)
     x y z  happly (ap fst (map .snd .pres-⋆ x y)) z)
     x y z  map .fst z .snd .pres-⋆ x y)

In fact, we can turn elements of hom(AB,C)\hom(A \otimes B, C) to hom(A,[B,C])\hom(A, [B, C]), too! It follows, since the underlying function is preserved, that this extends to an equivalence of hom\hom-sets hom(AB,C)hom(A,[B,C])\hom(A \otimes B, C) \cong \hom(A, [B, C]).

  tensor⊣hom : Ab.Hom (A  B) C  Ab.Hom A (Hom-group B C)
  tensor⊣hom = Iso→Equiv (to-ab-hom , iso from-ab-hom invr invl) where abstract
    invr : is-right-inverse from-ab-hom to-ab-hom
    invr f = Forget-is-faithful $ funext λ x  Forget-is-faithful refl

    invl : is-left-inverse from-ab-hom to-ab-hom
    invl f = Forget-is-faithful $ funext $
      Tensor-elim-prop _ _  x  C.has-is-set _ _)  x y  refl)
         p q  sym (f .snd .pres-⋆ _ _  ap₂ C._⋆_ (sym p) (sym q)))
         p  sym (pres-inv (f .snd)  ap C.inverse (sym p)))
        (sym (pres-id (f .snd)))

and indeed this isomorphism is one of hom\hom-groups, hence since Ab\ht{Ab} is a univalent category, an identification of hom\hom-groups.

  Tensor⊣Hom : Hom-group (A  B) C  Hom-group A (Hom-group B C)
  Tensor⊣Hom = iso→path (Ab _) Ab-is-category $
    Ab.make-iso (to-ab-hom , to′) (from-ab-hom , from′)
      (Forget-is-faithful $ funext (equiv→section (tensor⊣hom .snd)))
      (Forget-is-faithful $ funext (equiv→retraction (tensor⊣hom .snd)))
Actually establishing that the components of tensor⊣hom are group homomorphisms is very tedious, though!
    to′ : Group-hom (Hom-group (A  B) C .object) (Hom-group A (Hom-group B C) .object) to-ab-hom
    to′ .pres-⋆ f g = Forget-is-faithful $ funext λ x  Forget-is-faithful refl

    from′ : Group-hom (Hom-group A (Hom-group B C) .object) (Hom-group (A  B) C .object) from-ab-hom
    from′ .pres-⋆ f g = Forget-is-faithful $ funext $
      Tensor-elim-prop _ _  x  C.has-is-set _ _)
         x y  refl)
         {x} {y} p q  ap₂ C._⋆_ p q  path x y)
         {x} p  ap C.inverse p
                ·· C.inv-comm
                ·· sym (ap₂ C._⋆_ (pres-inv (g′ .snd) {x = x}) (pres-inv (f′ .snd) {x = x}))
        (sym ( ap₂ C._⋆_ (pres-id (f′ .snd))
                         (pres-id (f′ .snd))
        f′ = from-ab-hom f
        g′ = from-ab-hom g
        path :  x y  (f′ .fst x C.⋆ g′ .fst x) C.⋆ (f′ .fst y C.⋆ g′ .fst y)
                      f′ .fst (x :+ y) C.⋆ g′ .fst (x :+ y)
        path x y =
          (f′ .fst x C.⋆ g′ .fst x) C.⋆ (f′ .fst y C.⋆ g′ .fst y) ≡⟨ solve-monoid C.underlying-monoid 
          f′ .fst x C.⋆ (g′ .fst x C.⋆ f′ .fst y) C.⋆ g′ .fst y   ≡⟨  i  f′ .fst x C.⋆ C.commutative {x = g′ .fst x} {y = f′ .fst y} i C.⋆ g′ .fst y) 
          f′ .fst x C.⋆ (f′ .fst y C.⋆ g′ .fst x) C.⋆ g′ .fst y   ≡⟨ solve-monoid C.underlying-monoid 
          (f′ .fst x C.⋆ f′ .fst y) C.⋆ (g′ .fst x C.⋆ g′ .fst y) ≡˘⟨ ap₂ C._⋆_ (f′ .snd .pres-⋆ x y) (g′ .snd .pres-⋆ x y) ≡˘
          f′ .fst (x :+ y) C.⋆ g′ .fst (x :+ y)