モノイダル圏
MonoidalCategory.sig2-signature
<MonCAT: c; m, i; α, λ, ρ>
fixed-in <: CAT; ×, I>
Data
0-morph underlying @ c : CAT
1-morph product @ m : c × c -> c
1-morph unit @ i : I -> c
2-iso associator @ α
: (m × c^) * m => (c^ × m) * m
: c × c × c -> c
2-iso l-unitor @ λ
: (i × c^) * m => c^
: c -> c
2-iso r-unitor @ ρ
: (c^ × i) * m => c^
: c -> c
Axioms
3-eq triangle-identity
: (ρ × c^) * m =3= (c^ × i × c^) * α ; (c^ × λ) * m
: (c^ × i × c^) * (m × c^) * m => m
: c × c -> c
3-eq pentagon-identity
: (m × c^ × c^) * α ; (c^ × c^ × m) * α =3= (α × c^) * m ; (c^ × m × c^) * α ; (c^ × α) * m
: (m × c^ × c^) * (m × c^) * m => (c^ × c^ × m) * (c^ × m) * m
: c × c × c × c -> c\left\lang\mathrm{ MonCAT }\colon c; m, i; \alpha, \lambda, \rho \right\rang
fixed in \mathbf{CAT}_× = \left\lang \mathbf{CAT} ; (×), I \right\rang
0-morph
底圏c \colon \mathbf{CAT}
1-morph
m =(\otimes)\colon c×c\to c
i \colon c
i.e.i^\sim \colon I → c
2-iso
α \colon (m × c^\wedge) * m ⇒ (c^\wedge × m) * m
\colon (c×c)×c → c
i.e.
α\colon ( \_ ⊗ \_ ) ⊗ \_ \cong \_ ⊗ ( \_ ⊗ \_ )
\forall x,y,z \colon c
\alpha_{x,y,z}\colon (x \otimes y)\otimes z → x \otimes (y \otimes z)
\lambda\colon (i × c^\wedge) * m ⇒ c^\wedge
\colon I × c → c
i.e.
λ\colon i⊗\_ \cong \_
\lambda_x \colon i\otimes x → x
ρ\colon (c^\wedge × i) * m ⇒ c^\wedge
\colon c × I → c
i.e.
\rho\colon \_\otimes i \cong \_
\rho_x\colon x\otimes i → x
図式
Cat 1-2図式
Cat 1-P図式
\mathbf{CAT}_×上の積からモノイダル積にしている
公理系
Mac Laneの整合性条件
(ρ × c^\wedge) * m= ((c^\wedge × i × c^\wedge) * α) ; (c^\wedge × λ) * m
\colon (c^\wedge × i × c^\wedge) * (m × c^\wedge) * m ⇒ m
: c × c → c
i.e. \rho_x \otimes y^\wedge = \alpha_{x,i,y}; x^\wedge \otimes \lambda_y
(x\otimes i) \otimes y \to x\otimes y
(m × c^\wedge × c^\wedge) * α
; (c^\wedge × c^\wedge × m) * α
= (α × c^\wedge) * m
; (c^\wedge × m × c^\wedge) * α
; (c^\wedge × α) * m
\colon (m × c^\wedge × c^\wedge) * (m × c^\wedge) * m
⇒ (c^\wedge × c^\wedge × m) * (c^\wedge × m) * m
\colon c × c × c × c → c
i.e.\alpha_{x ⊗ y, z,w} ; \alpha_{x, y, z ⊗ w}= \alpha_{x,y,z} ⊗ w^\wedge ; \alpha_{x,y ⊗ z,w} ; x^\wedge ⊗ \alpha_{y,z,w}
((x ⊗ y)⊗ z)⊗ w\to x \otimes( y\otimes (z\otimes w))
sigMonoidalCategory = Monoid :in CATモノイダル圏の中のモノイダル……
上の世界の結合子とかが必要
>
>
