証明:左指数単位律子の可逆性

左指数単位律子の可逆性を示す

左右を入れ替えれば右指数単位律子も同様

函手の結合と向きを揃えるには、右の方が見やすかったね

$ ν :i⊸\_ ⇒ \_

https://gyazo.com/fd8bcbfb509e0b7d447c6f5579247e92 https://gyazo.com/c7292d1ce27efabffbcc9cddaafb1ddd

証明

MC C ⊗ i α λ ρ

モノイダル圏

Adjunction C C (i⊗) (i⊸) i.unit i.eval

単位対象iについての左指数随伴系

αとρは使わない

指標の接頭記号別名

% = L-MC C ⊗ i α λ ρ

埋め込み先を&とする

(Catなど)

以下が可逆であることを示す

左指数単位律子

code:sig

&2-iso

ν : (i⊸) ~= C^

i.e.

&2-morph

ν : (i⊸) => C^

ν- : C^ => (i⊸)

&3-eq

ν = (i⊸) * λ- ; i.eval

ν- = i.unit ; λ * (i⊸)

適用すると

code:sig

%0-morph

%1-morph

b.ν, b.ν-

%2-eq

b.ν = (i⊸b).λ- ; b.i.eval

b.ν- = b.i.unit ; i⊸(b.λ)

https://gyazo.com/bb3787670142ac626329e48656ff7f3d https://gyazo.com/96eae227f1085f89e6c4f350850adc02

https://gyazo.com/fa627c5f62cb2dc880a0a6577e5b2c39 https://gyazo.com/7712f8cbc9aa782ecf839e2f6c1693b6

P-1図式は右寄せP-1図式とする

where

モノイダル積の左単位律子$ λ \colon i⊗\_ ⇒\_ とその逆

https://gyazo.com/b8d8d8a09f141025c277e4c6a4250276

右の全てに作用する

可逆性

https://gyazo.com/1d510fdc173a484278452859ba101226 https://gyazo.com/7fb04472490b67604b20819044cda4c7

code:sig

&2-iso

λ : (i⊗) ~= C^

i.e.

&2-morph

λ : (i⊗) => C^

λ- : C^ => (i⊗)

&3-eq

λ; λ- = (i⊗)^

λ-; λ = C^^

指数随伴系の単位と余単位

code:sig

&2-morph

i.unit : C^ => (i⊗) * (i⊸)

i.eval : (i⊸) * (i⊗) => C^

以上とニョロニョロ公理から

https://gyazo.com/5856186eed60d6a1d127ac559da0f977 https://gyazo.com/7bf417918eb2f75436cb09a140e30157

code:sig

(i⊸)^

-- ニョロニョロ公理

= (i⊸) * i.unit; i.eval * (i⊸)

= (i⊸) * i.unit; (i⊸) * (i⊗) * (i⊸); i.eval * (i⊸)

-- λの可逆性

= (i⊸) * i.unit; (i⊸) * (λ; λ-) * (i⊸); i.eval * (i⊸)

-- 縦横の組み替え

= (i⊸) * i.unit; (i⊸) * λ * (i⊸); (i⊸) * λ- * (i⊸); i.eval * (i⊸)

= (i⊸) * i.unit; λ * (i⊸); (i⊸) * λ-; i.eval * (i⊸)

= (i⊸) * ν- ; ν * (i⊸) = ν * ν-

= ν ; ν-

https://gyazo.com/fd8bcbfb509e0b7d447c6f5579247e92

https://gyazo.com/5149b70c3d8cf41f72f8dc21f9012fc2 https://gyazo.com/9996dc7235bd5b4023c33550bd1437b1

code:sig

C^^

-- λの可逆性

= λ- ; λ = λ- ; (i⊗) ; λ

-- ニョロニョロ公理

= λ-; i.unit *(i⊗); (i⊗)* i.eval; λ

-- λたちの連続エレベーター

= i.unit * λ-; λ * i.eval

= i.unit; (i⊗) * (i⊸) * λ-; λ * (i⊸) * (i⊗); i.eval

= i.unit ; λ * (i⊸) * λ- ; i.eval

= i.unit ; λ * (i⊸); (i⊸) * λ- ; i.eval

= ν- ; ν

https://gyazo.com/c7292d1ce27efabffbcc9cddaafb1ddd

証明完了