/dragoon8192-main/モノイダル圏の定義フルバージョン

generated at 2/18/2025, 5:46:50 PM
モノイダル圏の定義 フルバージョン

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; α, λ, ρ \right\rang
fixed in \mathbf{CAT}_× = \left\lang \mathbf{CAT} ; (×), I ; \dot α, \dot λ, \dot ρ \right\rang
where
\forall a,b,c\colon \mathbf{CAT}
(a,b,c).\dot α \colon (a×b)× c → a×(b×c)
a.\dot λ \colon I × a → a
a.\dot ρ \colon a × I → a
0-morph
底圏c \colon \mathbf{CAT}
1-morph
モノイダル積 monoidal product
m =(\otimes)\colon c×c\to c
単位対象 unit object
i \colon I → c
2-iso
結合律子
α \colon  (m × c^\wedge) * m
⇒ (c,c,c).\dot α * (c^\wedge × m) * m
\colon (c×c)×c → c
左単位律子
λ\colon (i × c^\wedge) * m ⇒ c.\dot λ
\colon I × c → c
右単位律子
ρ\colon (c^\wedge × i) * m ⇒ c.\dot ρ
\colon c × I → c
  
公理系
triangle identity
(ρ × c^\wedge) * m
= ((c^\wedge × i) × c^\wedge) * α
; (c,I,c).\dot α * (c^\wedge × λ) * m
 \colon ((c^\wedge × i) × c^\wedge) * (m × c^\wedge) * m
⇒ (c,c).\mathrm{Tri} * m
: (c × I) × c → c
where
(c,i,c).\dot α
= ((c^\wedge × i) × c^\wedge) * (c,c,c).\dot α
= (c,I,c).\dot α * (c^\wedge × (i × c^\wedge )) 
(c,c).\mathrm{Tri} \coloneqq  c.\dot ρ × c^\wedge
= (c,I,c).\dot \alpha * (c^\wedge \times c.\dot \lambda)
\colon (c × I) \times c \to c\times c
\mathbf{CAT}_×での triangle identity
pentagon identity
(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))
 monoidal category in nLab