open import Algebra.Group.Cat.Base
open import Algebra.Group.Solver
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 = 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 ${\mathbf{Ab}}$ of abelian groups is better behaved than the category ${\mathbf{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 ${\mathbf{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 β} Ξ» (_ , x) β is-abelian-group x

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 $X \to G$:

module _ {β ββ²} (X : Type β) (G : Group ββ²) where private
open Group-on (G .snd)

Map-group : Group (β β ββ²)
Map-group = to-group grp where
grp : make-group (X β β G β)
grp .make-group.group-is-set = hlevel 2
grp .make-group.unit = Ξ» _ β unit
grp .make-group.mul f g x = f x β g x
grp .make-group.inv f x = inverse (f x)
grp .make-group.assoc f g h i x = associative {x = f x} {y = g x} {z = h x} (~ i)
grp .make-group.invl f i x = inversel {x = f x} i
grp .make-group.invr f i x = inverser {x = f x} i
grp .make-group.idl 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 ${\mathbf{Hom}}_{{\mathbf{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 = restrict (to-group grp) abel where
T = Ab.Hom A B

    open import 1Lab.Reflection
add-map : T β T β T
add-map f g .hom x = (f # x) B.β (g # x)
add-map f g .preserves .p x y =
f # (x A.β y) B.β g # (x A.β y)         β‘β¨ apβ B._β_ (f .preserves .p x y) (g .preserves .p x y) β©β‘
(f # x B.β f # y) B.β (g # x B.β g # y) β‘β¨ group! (B .object)  β©β‘
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   β‘β¨ group! (B .object) β©β‘
(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)$. 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 .hom x = f # x B.β»ΒΉ
inv-map f .preserves .p x y =
f # (x A.β y) β»ΒΉ   β‘β¨ ap B.inverse (f .preserves .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 : make-group T
grp .make-group.group-is-set = Ab.Hom-set A B
grp .make-group.unit = zero-map
grp .make-group.inv = inv-map
grp .make-group.assoc x y z = Homomorphism-path Ξ» x β sym B.associative
grp .make-group.invl x = Homomorphism-path Ξ» x β B.inversel
grp .make-group.invr x = Homomorphism-path Ξ» x β B.inverser
grp .make-group.idl x = Homomorphism-path Ξ» x β B.idl

abel : is-abelian-group (to-group-on grp)
abel f g = Homomorphism-path Ξ» _ β B.commutative


By pre/post composition, the Hom-group construction extends to a functor ${\mathbf{Ab}}{^{{\mathrm{op}}}}\times {\mathbf{Ab}} \to {\mathbf{Ab}}$, the internal ${\mathbf{Hom}}$ abelian group.

module _ {β} where
open Functor

Ab-hom : Functor (Ab β ^op ΓαΆ 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 .preserves)
fβ² : Groups.Hom (Hom-group x y .object) (Hom-group xβ² yβ² .object)
fβ² .hom h = gh Groups.β h Groups.β fh
fβ² .preserves .Group-hom.pres-β _ _ = Homomorphism-path Ξ» i β g.pres-β _ _

Ab-hom .F-id = Homomorphism-path Ξ» i β Forget-is-faithful refl
Ab-hom .F-β f g = Homomorphism-path Ξ» i β Forget-is-faithful refl


# The tensor productπ

We extend the category ${\mathbf{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 ${\mathbf{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 ${\mathbf{Hom}}$ functor β that is, homs $A \otimes B \to C$ correspond to bilinear maps $A, B \to C$: functions which are βseparately group homomorphisms in each variableβ. By adjointness, these are the same as group homomorphisms $A \to [B, C]$.

module _ {β} (A B : AbGroup β) where
private
module A = AbGrp A
module B = AbGrp B


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

• The first constructor is the inclusion $A \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 = 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 $A \otimes B$.

  _β_ : AbGroup β
_β_ = restrict (to-group tensor) Ξ» x y β t-comm
where
tensor : make-group Tensor
tensor .make-group.group-is-set = t-squash
tensor .make-group.unit = :0
tensor .make-group.mul x y = x :+ y
tensor .make-group.inv = :inv
tensor .make-group.assoc x y z = t-assoc
tensor .make-group.invl x = t-invl
tensor .make-group.invr x = t-invr
tensor .make-group.idl x = t-idl


All of those path constructors impose restrictions on mapping out of $A \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 \times B \to C$ is a function of sets such that $f(xy, z) = f(x, z)f(y, z)$ and $f(x, yz) = f(x, y)f(x, z)$, then it extends to an abelian group homomorphism ${\mathbf{Hom}}(A \otimes B, C)$.

  from-multilinear-map
: (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 = total-hom 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 ${\mathbf{Hom}}(A, [B, C])$, just packaged differently. By unpacking and re-packing that data, we can also turn those homomorphisms into ones ${\mathbf{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 # x # y)
(Ξ» x y z β happly (ap hom (map .preserves .pres-β x y)) z)
(Ξ» x y z β (map # z) .preserves .pres-β x y)


In fact, we can turn elements of ${\mathbf{Hom}}(A \otimes B, C)$ to ${\mathbf{Hom}}(A, [B, C])$, too! It follows, since the underlying function is preserved, that this extends to an equivalence of ${\mathbf{Hom}}$-sets ${\mathbf{Hom}}(A \otimes B, C) \cong {\mathbf{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 .preserves .pres-β _ _ β apβ C._β_ (sym p) (sym q))) (Ξ» p β sym (pres-inv (f .preserves) β ap C.inverse (sym p))) (sym (pres-id (f .preserves)))  and indeed this isomorphism is one of ${\mathbf{Hom}}$-groups, hence since ${\mathbf{Ab}}$ is a univalent category, an identification of ${\mathbf{Hom}}$-groups.  Tensorβ£Hom : Hom-group (A β B) C β‘ Hom-group A (Hom-group B C) Tensorβ£Hom = Ab-is-category .to-path$
Ab.make-iso (total-hom to-ab-hom toβ²) (total-hom from-ab-hom fromβ²)
(Forget-is-faithful $funext (equivβcounit (tensorβ£hom .snd))) (Forget-is-faithful$ funext (equivβunit (tensorβ£hom .snd)))

Actually establishing that the components of tensorβ£hom are group homomorphisms is very tedious, though!
    where
toβ² : Group-hom _ _ to-ab-hom
toβ² .pres-β f g = Forget-is-faithful $funext Ξ» x β Forget-is-faithful refl fromβ² : Group-hom _ _ 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β² .preserves) {x = x}) (pres-inv (fβ² .preserves) {x = x}))
β C.commutative)
(sym ( apβ C._β_ (pres-id (fβ² .preserves))
(pres-id (fβ² .preserves))
β C.idl))
where
fβ² = from-ab-hom f
gβ² = from-ab-hom g
path : β x y β (fβ² # x C.β gβ² # x) C.β (fβ² # y C.β gβ² # y)
β‘ fβ² # (x :+ y) C.β gβ² # (x :+ y)
path x y =
(fβ² # x C.β gβ² # x) C.β (fβ² # y C.β gβ² # y) β‘β¨ group! (C .object) β©β‘
fβ² # x C.β (gβ² # x C.β fβ² # y) C.β gβ² # y   β‘β¨ (Ξ» i β fβ² # x C.β C.commutative {x = gβ² # x} {y = fβ² # y} i C.β gβ² # y) β©β‘
fβ² # x C.β (fβ² # y C.β gβ² # x) C.β gβ² # y   β‘β¨ group! (C .object) β©β‘
(fβ² # x C.β fβ² # y) C.β (gβ² # x C.β gβ² # y) β‘Λβ¨ apβ C._β_ (fβ² .preserves .pres-β x y) (gβ² .preserves .pres-β x y) β©β‘Λ
fβ² # (x :+ y) C.β gβ² # (x :+ y)             β