モノイド閉圏の事例： ボックス積の双関手性

その他 特例

ボックス積 (-□-) を Box:SG×SG→SG とも書く。ボックス積が双関手性を持つとは、直積圏からの関手であることだから：

  1. Box( (f, f');(g, g') ) = Box( (f, f') );Box( (g, g') ) （結合の保存）
  2. Box( (A, B)^ ) = Box( (A, B) )^ （単位の保存）

中置演算子形式ならば：

  1. (f;g)□(f';g') = (f□f');(g□g') （交替律）
  2. A^□B^ = (A□B)^ （単位の交替律）

これらを計算により直接示す。

(f;g)□(f';g') = (f□f');(g□g')
  • f:A→B, g:B→C, f;g:A→C
  • f':A'→B', g':B'→C', f';g':A'→C'
  • (f;g)□(f';g'):A□A'→C□C'

とする。

左辺 : A□A'→C□C'
=
[
  λ0(a, a')∈A□A'.(
    ( (f;g)(a), (f';g')(a') ) ∈C□C'
  )
  ALSO
  λ1(a→a', a'')∈A□A'.(
    ( (f;g)(a→a'), (f';g')(a'') ) ∈C□C'
  )
  OR
  λ1(a, a'→a'')∈A□A'.(
    ( (f;g)(a), (f';g')(a→a'') ) ∈C□C'
  )
] : A□A'→C□C'

右辺 : A□A'→C□C'
= 
[
  λ0(a, a')∈A□A'.(
    ( f(a), f'(a') ) ∈B□B'
  )
  ALSO
  λ1(a→a', a'')∈A□A'.(
    ( f(a→a'), f'(a'') ) ∈B□B'
  )
  OR
  λ1(a, a'→a'')∈A□A'.(
    ( f(a), f'(a'→a'') ) ∈B□B'
  )
] ; [
  λ0(b, b')∈B□B'.(
    ( g(b), g'(b') ) ∈C□C'
  )
  ALSO
  λ1(b→b', b'')∈B□B'.(
    ( g(b→b'), g'(b'') ) ∈C□C'
  )
  OR
  λ1(b, b'→b'')∈B□B'.(
    ( g(a), g'(b'→b'') ) ∈C□C'
  )
] : A□A'→C□C'
= 
[
  λ0(a, a')∈A□A'.(
    ( (f;g)(a), (f';g')(a') ) ∈C□C'
  )
  ALSO
  λ1(a→a', a'')∈A□A'.(
    ( (f;g)(a→a'), (f';g')(a'') ) ∈C□C'
  )
  OR
  λ1(a, a'→a'')∈A□A'.(
    ( (f;g)(a), (f';g')(a'→a'') ) ∈C□C'
  )
] : A□A'→C□C'
A^□B^ = (A□B)^
左辺 :A□B→A□B
= A^□B^
=
[
  λ0(a, b)∈A□B.(
    (a, b) ∈A□B
   )
   ALSO
  λ1(a→a', b)∈A□B.(
    (a→a', b) ∈A□B
   )
   OR
  λ1(a, b→b')∈A□B.(
    (a, b→b') ∈A□B
   )
] :A□B→A□B

右辺も同じ表示になることは自明だろう。