モノイダル圏 - 雑多な感じ

モノイダル圏

monoidal category

summary.icon

モノイダル積とその単位対象を備えた圏指標

code:MonoidalCategory.sig

2-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

definition.icon モノイダル圏

$ \left\lang\mathrm{ MonCAT }\colon c; m, i; \alpha, \lambda, \rho \right\rang

fixed in $ \mathbf{CAT}_× = \left\lang \mathbf{CAT} ; (×), I \right\rang

dragoon8192.icon厳密な定義には$ \mathbf{CAT}_× の律子が必要

モノイダル圏の定義フルバージョン

0-morph

底圏$ c \colon \mathbf{CAT}

1-morph

モノイダル積 monoidal product

or テンソル積 tensor product

$ m =(\otimes)\colon c×c\to c

単位対象 unit object

$ i \colon c

i.e.$ i^\sim \colon I → c

2-iso

結合律子 associator

$ α \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)

左単位律子 left unitor

$ \lambda\colon (i × c^\wedge) * m ⇒ c^\wedge

$ \colon I × c → c

i.e.

$ λ\colon i⊗\_ \cong \_

$ \lambda_x \colon i\otimes x → x

右単位律子 right unitor

$ ρ\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図式

https://gyazo.com/2664e9f5a71bf50e07a729289766ad78

Cat 1-P図式

$ \mathbf{CAT}_× 上の積からモノイダル積にしている

https://gyazo.com/a913a1de1381f1ec14429065c8529ec5

公理系

Mac Laneの整合性条件

triangle identity

$ (ρ × 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

https://gyazo.com/15efa7109c11e9183e0393000efb1669

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

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

https://gyazo.com/aa34b444e8db0b19970fcb91ef7c5497

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))

out-of.icon

code:sig

MonoidalCategory = Monoid :in CAT

モノイダル圏の中のモノイダル……

モノイド対象

上の世界の結合子とかが必要

マイクロコスモ原理

Ref.icon マイクロコスモ原理と構造の無限タワー - 檜山正幸のキマイラ飼育記 (はてなBlog)

Ref.icon monoidal category in nLab

Ref.iconモノイド圏 - Wikipedia

Ref.icon マックレーンの五角形をインデックスなしの等式で表す - 檜山正幸のキマイラ飼育記 (はてなBlog)

https://upload.wikimedia.org/wikipedia/commons/thumb/8/82/Monoidal_category_pentagon.svg/1024px-Monoidal_category_pentagon.svg.png

https://upload.wikimedia.org/wikipedia/commons/thumb/e/e9/Monoidal_category_triangle.svg/1024px-Monoidal_category_triangle.svg.png