module Algebra.Group.Ab.Tensor where
Bilinear mapsπ
A function , where all types involved are equipped with abelian group structures, is called bilinear when it satisfies and : 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 .
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 , we set out to search for an abelian group which lets us βassociateβ Bilinear in the other direction: Bilinear maps are equivalent to group homomorphisms , but is there a construction ββ, playing the role of product type, such that is also the type of bilinear maps ?
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 , we write this infix as , and refer to it as the tensor product of abelian groups. Since 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: should be an Abelian group, and it should admit a bilinear map .
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 . 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 , we can first extend it to a function of sets 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
The tensor-hom adjunctionπ
Since we have a construction satisfying , 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 .
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