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 . 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 of abelian groups is better behaved than the category 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 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 :
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 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 . 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.mul = add-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 , the internal 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 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 ; There is also the βdirect (bi)productβ of abelian groups. The tensor product has primacy because it defines a left adjoint to the internal functor β that is, homs correspond to bilinear maps : functions which are βseparately group homomorphisms in each variableβ. By adjointness, these are the same as group homomorphisms .
module _ {β} (A B : AbGroup β) where private module A = AbGrp A module B = AbGrp B
While the universal property of is simple enough to state, actually constructing it is⦠another matter entirely. We construct the underlying set of , written Tensor in the code, as a massive higher inductive type:
- The first constructor is the inclusion 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 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 .
_β_ : 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 , 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 is a function of sets such that and , then it extends to an abelian group homomorphism .
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 , just packaged differently. By unpacking and re-packing that data, we can also turn those homomorphisms into ones .
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 to , too! It follows, since the underlying function is preserved, that this extends to an equivalence of -sets .
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 -groups, hence since is a univalent category, an identification of -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) β