module Algebra.Group.Ab.Tensor where

Bilinear mapsπŸ”—

A function f:F→G→Hf : F \to G \to H, where all types involved are equipped with abelian group structures, is called bilinear when it satisfies f(x+y,z)=f(x,z)+f(y,z)f(x + y, z) = f(x, z) + f(y, z) and f(x,y+z)=f(x,y)+f(x,z)f(x, y + z) = f(x, y) + f(x, z): it is a group homomorphism in each of its arguments.

record Bilinear (A : Abelian-group β„“) (B : Abelian-group β„“β€²) (C : Abelian-group β„“β€²β€²) : Type (β„“ βŠ” β„“β€² βŠ” β„“β€²β€²) where
  private
    module A = Abelian-group-on (A .snd)
    module B = Abelian-group-on (B .snd)
    module C = Abelian-group-on (C .snd)

  field
    map     : ⌞ A ⌟ β†’ ⌞ B ⌟ β†’ ⌞ C ⌟
    pres-*l : βˆ€ x y z β†’ map (x A.* y) z ≑ map x z C.* map y z
    pres-*r : βˆ€ x y z β†’ map x (y B.* z) ≑ map x y C.* map x z
  fixl-is-group-hom : βˆ€ a β†’
    is-group-hom B.Abelian→Group-on C.Abelian→Group-on (map a)
  fixl-is-group-hom a .is-group-hom.pres-⋆ x y = pres-*r a x y

  fixr-is-group-hom : βˆ€ b β†’
    is-group-hom A.Abelian→Group-on C.Abelian→Group-on (λ a → map a b)
  fixr-is-group-hom b .is-group-hom.pres-⋆ x y = pres-*l x y b

  module fixl {a} = is-group-hom (fixl-is-group-hom a)
  module fixr {a} = is-group-hom (fixr-is-group-hom a)

  open fixl
    renaming ( pres-id   to pres-idr
             ; pres-inv  to pres-invr
             ; pres-diff to pres-diffr
             )
    hiding ( pres-⋆ )
    public
  open fixr
    renaming ( pres-id   to pres-idl
             ; pres-inv  to pres-invl
             ; pres-diff to pres-diffl
             )
    hiding ( pres-⋆ )
    public

Bilinear-path
  : βˆ€ {A : Abelian-group β„“} {B : Abelian-group β„“β€²} {C : Abelian-group β„“β€²β€²}
  β†’ {ba bb : Bilinear A B C}
  β†’ (βˆ€ x y β†’ Bilinear.map ba x y ≑ Bilinear.map bb x y)
  β†’ ba ≑ bb
Bilinear-path {A = A} {B = B} {C = C} {ba = ba} {bb} p = q where
  module A = Abelian-group-on (A .snd)
  module B = Abelian-group-on (B .snd)
  module C = Abelian-group-on (C .snd)
  open Bilinear

  q : ba ≑ bb
  q i .map x y = p x y i
  q i .pres-*l x y z = is-prop→pathp (λ i → C.has-is-set (p (x A.* y) z i) (p x z i C.* p y z i))
    (ba .pres-*l x y z) (bb .pres-*l x y z) i
  q i .pres-*r x y z = is-prop→pathp (λ i → C.has-is-set (p x (y B.* z) i) (p x y i C.* p x z i))
    (ba .pres-*r x y z) (bb .pres-*r x y z) i

module _ {β„“} (A B C : Abelian-group β„“) where

We have already noted that the set of group homomorphisms between a pair of abelian groups is an abelian group, under pointwise multiplication. The type of bilinear maps is equivalent to the type of group homomorphisms A→[B,C]A \to [B,C].

  curry-bilinear : Bilinear A B C β†’ Ab.Hom A Ab[ B , C ]
  curry-bilinear f .hom a .hom       = f .Bilinear.map a
  curry-bilinear f .hom a .preserves = Bilinear.fixl-is-group-hom f a
  curry-bilinear f .preserves .is-group-hom.pres-⋆ x y =
    Homomorphism-path Ξ» z β†’ f .Bilinear.pres-*l _ _ _

  curry-bilinear-is-equiv : is-equiv curry-bilinear
  curry-bilinear-is-equiv = is-iso→is-equiv morp where
    morp : is-iso curry-bilinear
    morp .is-iso.inv uc .Bilinear.map x y = uc .hom x .hom y
    morp .is-iso.inv uc .Bilinear.pres-*l x y z = ap (_# _) (uc .preserves .is-group-hom.pres-⋆ _ _)
    morp .is-iso.inv uc .Bilinear.pres-*r x y z = uc .hom _ .preserves .is-group-hom.pres-⋆ _ _
    morp .is-iso.rinv uc = Homomorphism-path Ξ» x β†’ Homomorphism-path Ξ» y β†’ refl
    morp .is-iso.linv uc = Bilinear-path Ξ» x y β†’ refl

The tensor productπŸ”—

Thinking about the currying isomorphism Aβ†’(Bβ†’C)≃(AΓ—B)β†’CA \to (B \to C) \simeq (A \times B) \to C, we set out to search for an abelian group which lets us β€œassociate” Bilinear in the other direction: Bilinear maps Aβ†’Bβ†’CA \to B \to C are equivalent to group homomorphisms Aβ†’[B,C]A \to [B,C], but is there a construction β€œP(A,B)P(A, B)”, playing the role of product type, such that P(A,B)β†’CP(A, B) \to C is also the type of bilinear maps Aβ†’Bβ†’CA \to B \to C?

The answer is yes: rather than PP, we write this infix as AβŠ—BA \otimes B, and refer to it as the tensor product of abelian groups. Since AβŠ—BA \otimes B is determined by the maps out of it, we can construct it directly as a higher inductive type. We add a constructor for every operation we want, and for the equations these should satisfy: AβŠ—BA \otimes B should be an Abelian group, and it should admit a bilinear map Aβ†’Bβ†’AβŠ—BA \to B \to A \otimes B.

  data Tensor : Type (β„“ βŠ” β„“β€²) where
    :1       : Tensor
    _:*_     : Tensor β†’ Tensor β†’ Tensor
    :inv     : Tensor β†’ Tensor
    squash   : is-set Tensor
    t-invl   : βˆ€ {x} β†’ :inv x :* x ≑ :1
    t-idl    : βˆ€ {x} β†’ :1 :* x ≑ x
    t-assoc  : βˆ€ {x y z} β†’ x :* (y :* z) ≑ (x :* y) :* z
    t-comm   : βˆ€ {x y} β†’ x :* y ≑ y :* x

    _,_       : ⌞ A ⌟ β†’ ⌞ B ⌟ β†’ Tensor
    t-pres-*r : βˆ€ {x y z} β†’ (x , y B.* z) ≑ (x , y) :* (x , z)
    t-pres-*l : βˆ€ {x y z} β†’ (x A.* y , z) ≑ (x , z) :* (y , z)

The first 8 constructors are, by definition, exactly what we need to make Tensor into an abelian group. The latter three are the bilinear map Aβ†’Bβ†’AβŠ—BA \to B \to A \otimes B. Since this is an inductive type, it’s the initial object equipped with these data.

  open make-abelian-group
  make-abelian-tensor : make-abelian-group Tensor
  make-abelian-tensor .ab-is-set   = squash
  make-abelian-tensor .mul         = _:*_
  make-abelian-tensor .inv         = :inv
  make-abelian-tensor .1g          = :1
  make-abelian-tensor .idl x       = t-idl
  make-abelian-tensor .assoc x y z = t-assoc
  make-abelian-tensor .invl x      = t-invl
  make-abelian-tensor .comm x y    = t-comm

  _βŠ—_ : Abelian-group (β„“ βŠ” β„“β€²)
  _βŠ—_ = to-ab make-abelian-tensor

  to-tensor : Bilinear A B _βŠ—_
  to-tensor .Bilinear.map           = _,_
  to-tensor .Bilinear.pres-*l x y z = t-pres-*l
  to-tensor .Bilinear.pres-*r x y z = t-pres-*r
  Tensor-elim-prop
    : βˆ€ {β„“β€²} {P : Tensor β†’ Type β„“β€²}
    β†’ (βˆ€ x β†’ is-prop (P x))
    β†’ (βˆ€ x y β†’ P (x , y))
    β†’ (βˆ€ {x y} β†’ P x β†’ P y β†’ P (x :* y))
    β†’ (βˆ€ {x} β†’ P x β†’ P (:inv x))
    β†’ P :1
    β†’ βˆ€ x β†’ P x
  Tensor-elim-prop {P = P} pprop ppair padd pinv pz = go where
    go : βˆ€ x β†’ P x
    go (x , y) = ppair x y
    go :1 = pz
    go (x :* y) = padd (go x) (go y)
    go (:inv x) = pinv (go x)
    go (squash x y p q i j) = is-prop→squarep (λ i j → pprop (squash x y p q i j))
      (Ξ» i β†’ go x) (Ξ» i β†’ go (p i)) (Ξ» i β†’ go (q i)) (Ξ» i β†’ go y) i j
    go (t-invl {x} i) = is-prop→pathp (λ i → pprop (t-invl i)) (padd (pinv (go x)) (go x)) pz i
    go (t-idl {x} i) = is-prop→pathp (λ i → pprop (t-idl i)) (padd pz (go x)) (go x) i
    go (t-assoc {x} {y} {z} i) =
      is-prop→pathp (λ i → pprop (t-assoc i))
        (padd (go x) (padd (go y) (go z)))
        (padd (padd (go x) (go y)) (go z))
        i
    go (t-comm {x} {y} i) =
      is-prop→pathp (λ i → pprop (t-comm i)) (padd (go x) (go y)) (padd (go y) (go x)) i
    go (t-pres-*r {x} {y} {z} i) = is-prop→pathp (λ i → pprop (t-pres-*r i)) (ppair x (y B.* z)) (padd (ppair x y) (ppair x z)) i
    go (t-pres-*l {x} {y} {z} i) = is-prop→pathp (λ i → pprop (t-pres-*l i)) (ppair (x A.* y) z) (padd (ppair x z) (ppair y z)) i

module _ {β„“ β„“β€² β„“β€²β€²} (A : Abelian-group β„“) (B : Abelian-group β„“β€²) (C : Abelian-group β„“β€²β€²) where
  private
    module A = Abelian-group-on (A .snd)
    module B = Abelian-group-on (B .snd)
    module C = Abelian-group-on (C .snd)

If we have any bilinear map Aβ†’Bβ†’CA \to B \to C, we can first extend it to a function of sets AβŠ—Bβ†’CA \otimes B \to C by recursion, then prove that this is a group homomorphism. It turns out that this extension is definitionally a group homomorphism.

  bilinear-mapβ†’function : Bilinear A B C β†’ Tensor A B β†’ ⌞ C ⌟
  bilinear-map→function bilin = go module bilinear-map→function where
    go : Tensor A B β†’ ⌞ C ⌟
    go :1       = C.1g
    go (x :* y) = go x C.* go y
    go (:inv x) = go x C.⁻¹
    go (x , y)  = Bilinear.map bilin x y

    go (squash x y p q i j)      = C.has-is-set (go x) (go y) (Ξ» i β†’ go (p i)) (Ξ» i β†’ go (q i)) i j
    go (t-invl {x} i)            = C.inversel {x = go x} i
    go (t-idl {x} i)             = C.idl {x = go x} i
    go (t-assoc {x} {y} {z} i)   = C.associative {x = go x} {go y} {go z} i
    go (t-comm {x} {y} i)        = C.commutes {x = go x} {y = go y} i
    go (t-pres-*r {a} {b} {c} i) = Bilinear.pres-*r bilin a b c i
    go (t-pres-*l {a} {b} {c} i) = Bilinear.pres-*l bilin a b c i

  {-# DISPLAY bilinear-map→function.go b = bilinear-map→function b #-}
  from-bilinear-map : Bilinear A B C β†’ Ab.Hom (A βŠ— B) C
  from-bilinear-map bilin .hom = bilinear-map→function A B C bilin
  from-bilinear-map bilin .preserves .is-group-hom.pres-⋆ x y = refl

It’s also easy to construct a function in the opposite direction, turning group homomorphisms into bilinear maps, but proving that this is an equivalence requires appealing to an induction principle of Tensor which handles the equational fields: Tensor-elim-prop.

  to-bilinear-map : Ab.Hom (A βŠ— B) C β†’ Bilinear A B C
  to-bilinear-map gh .Bilinear.map x y = gh .hom (x , y)
  to-bilinear-map gh .Bilinear.pres-*l x y z =
    ap (gh .hom) t-pres-*l βˆ™ gh .preserves .is-group-hom.pres-⋆ _ _
  to-bilinear-map gh .Bilinear.pres-*r x y z =
    ap (gh .hom) t-pres-*r βˆ™ gh .preserves .is-group-hom.pres-⋆ _ _

  from-bilinear-map-is-equiv : is-equiv from-bilinear-map
  from-bilinear-map-is-equiv = is-iso→is-equiv morp where
    morp : is-iso from-bilinear-map
    morp .is-iso.inv = to-bilinear-map
    morp .is-iso.rinv hom = Homomorphism-path $ Tensor-elim-prop A B (Ξ» x β†’ C.has-is-set _ _)
      (Ξ» x y β†’ refl)
      (Ξ» x y β†’ apβ‚‚ C._*_ x y βˆ™ sym (hom .preserves .is-group-hom.pres-⋆ _ _))
      (Ξ» x β†’ ap C._⁻¹ x βˆ™ sym (is-group-hom.pres-inv (hom .preserves)))
      (sym (is-group-hom.pres-id (hom .preserves)))
    morp .is-iso.linv x = Bilinear-path (Ξ» x y β†’ refl)

The tensor-hom adjunctionπŸ”—

Since we have a construction (AβŠ—B)(A \otimes B) satisfying (AβŠ—B)β†’C≃Aβ†’[B,C](A \otimes B) \to C \simeq A \to [B, C], we’re driven, being category theorists, to question its naturality: Is the tensor product a functor, and is this equivalence of Hom-sets an adjunction?

The answer is yes, and the proofs are essentially plugging together existing definitions, other than the construction of the functorial action of βŠ—\otimes.

Ab-tensor-functor : Functor (Ab β„“ Γ—αΆœ Ab β„“) (Ab β„“)
Ab-tensor-functor .Fβ‚€ (A , B) = A βŠ— B
Ab-tensor-functor .F₁ (f , g) = from-bilinear-map _ _ _ bilin where
  bilin : Bilinear _ _ _
  bilin .Bilinear.map x y       = f .hom x , g .hom y
  bilin .Bilinear.pres-*l x y z = ap (_, g .hom z) (f .preserves .is-group-hom.pres-⋆ _ _) βˆ™ t-pres-*l
  bilin .Bilinear.pres-*r x y z = ap (f .hom x ,_) (g .preserves .is-group-hom.pres-⋆ _ _) βˆ™ t-pres-*r
Ab-tensor-functor .F-id    = Hom≃Bilinear.injective _ _ _ (Bilinear-path Ξ» x y β†’ refl)
Ab-tensor-functor .F-∘ f g = Hom≃Bilinear.injective _ _ _ (Bilinear-path Ξ» x y β†’ refl)

Tensor⊣Hom : (A : Abelian-group β„“) β†’ Bifunctor.Left Ab-tensor-functor A ⊣ Bifunctor.Right Ab-hom-functor A
Tensor⊣Hom A = hom-isoβ†’adjoints to to-eqv nat where
  to : βˆ€ {x y} β†’ Ab.Hom (x βŠ— A) y β†’ Ab.Hom x Ab[ A , y ]
  to f = curry-bilinear _ _ _ (to-bilinear-map _ _ _ f)

  to-eqv : βˆ€ {x y} β†’ is-equiv (to {x} {y})
  to-eqv = βˆ™-is-equiv
    (Hom≃Bilinear _ _ _ .snd)
    (curry-bilinear-is-equiv _ _ _)

  nat : hom-iso-natural {L = Bifunctor.Left Ab-tensor-functor A} {R = Bifunctor.Right Ab-hom-functor A} to
  nat f g h = Homomorphism-path Ξ» x β†’ Homomorphism-path Ξ» y β†’ refl