open import Algebra.Group.Ab.Hom
open import Algebra.Group.Ab
open import Algebra.Group

open import Cat.Displayed.Univalence.Thin
open import Cat.Instances.Product
open import Cat.Displayed.Total
open import Cat.Prelude

import Cat.Functor.Bifunctor as Bifunctor

module Algebra.Group.Ab.Tensor where


# Bilinear maps🔗

private variable
ℓ ℓ′ ℓ′′ : Level


A function $f : 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)$ and $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 \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 \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 \to B \to C$ are equivalent to group homomorphisms $A \to [B,C]$, but is there a construction “$P(A, B)$”, playing the role of product type, such that $P(A, B) \to C$ is also the type of bilinear maps $A \to B \to C$?

module _ {ℓ ℓ′} (A : Abelian-group ℓ) (B : Abelian-group ℓ′) where
private
module A = Abelian-group-on (A .snd)
module B = Abelian-group-on (B .snd)


The answer is yes: rather than $P$, we write this infix as $A \otimes B$, and refer to it as the tensor product of abelian groups. Since $A \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 \otimes B$ should be an Abelian group, and it should admit a bilinear map $A \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 \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))
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 \to B \to C$, we can first extend it to a function of sets $A \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 #-}

module _ {ℓ} (A B 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)


  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)

  Bilinear≃Hom : Bilinear A B C ≃ Ab.Hom (A ⊗ B) C
Bilinear≃Hom = from-bilinear-map , from-bilinear-map-is-equiv
Hom≃Bilinear : Ab.Hom (A ⊗ B) C ≃ Bilinear A B C
Hom≃Bilinear = Bilinear≃Hom e⁻¹
module Bilinear≃Hom = Equiv Bilinear≃Hom
module Hom≃Bilinear = Equiv Hom≃Bilinear


open Functor


Since we have a construction $(A \otimes B)$ satisfying $(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