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 
    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.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 ${\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)))

    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)             ∎