ラックス単位律

本編ネタ 圏一般論 モノイド圏

ラックス単位律とは、ラックス・モノイド関手の左または右単位律。これの、ポイントフリー記述が結構難しい。

左ラックス単位律の左辺を成分表示するが、上から下のストリング図で3つのパートに分ける。

  1. ι ⊗ id_{F(X)}
  2. ν_{(J, X)}
  3. F(l_{X})

反図式順にして：

  1. (ι, id_{X.F}).Q
  2. (J, X).ν
  3. X.l.F

自明圏の対象を 0 として、

  1. (0.ι, id_{X.F}).Q
  2. (0.J, X).ν
  3. (0, X).l.F

引数を分離抽出して、

  1. (0, X).(ι × ID_F).Q
  2. (0, X).(J × Id_C).ν
  3. (0, X).l.F

つまり、

(0, X).[(ι × ID_F)*Q ; (J × Id_C)*ν ; l*F] in D

引数をはずすと：

  (ι × ID_F)*Q ; (J × Id_C)*ν ; l*F 
 :: (J×F) * Q ⇒ F
 : 1×C → C

右辺にほうは

 (J × F)*l
 :: (J×F) * Q ⇒ F
 : 1×C → C