Adjoint から Monad を導く
Menu Menu随伴関手
examples/cat-utility.agda examples/adj-monad.agda 圏には随伴関手 Adjoint Functor というものがあり、重要だとされています。Adjoint は二つの圏A,Bと二つの関手F,U (と二つの自然変換η、μ)の関係です。これが一体なんなのかを理解するのが圏論の一つの目標です。
U : Functor B A
F : Functor A B
η : NTrans A A identityFunctor ( U ○ F )
ε : NTrans B B ( F ○ U ) identityFunctor
U ○ F は Functor の結合で、Category.Cat で定義されています。identityFunctor からFunctorへの自然変換ηは、Monad でも出てきました。これから、Monad ( U ○ F, η, UεF ) を Adjunction から導くので、まさに同じものです。
Adjunction の定義は以下の通りです。
record IsAdjunction {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
( U : Functor B A )
( F : Functor A B )
( η : NTrans A A identityFunctor ( U ○ F ) )
( ε : NTrans B B ( F ○ U ) identityFunctor )
: Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
field
adjoint1 : { b : Obj B } →
A [ A [ ( FMap U ( TMap ε b )) o ( TMap η ( FObj U b )) ] ≈ id1 A (FObj U b) ]
adjoint2 : {a : Obj A} →
B [ B [ ( TMap ε ( FObj F a )) o ( FMap F ( TMap η a )) ] ≈ id1 B (FObj F a) ]
record Adjunction {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
: Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
field
U : Functor B A
F : Functor A B
η : NTrans A A identityFunctor ( U ○ F )
ε : NTrans B B ( F ○ U ) identityFunctor
isAdjunction : IsAdjunction A B U F η ε
IsAdjunction には随伴函手の性質を記述します。ここには登場人物と、それが満たす論理式が書かれます。Adjunction は、引数に与えられる登場人物を書きます。field には、随伴函手があると存在することになる登場人物を記述します。随伴函手は凾手二つと自然変換二つ持っているので便利に使えます。でも、随伴函手を示すのは大変ということになります。
登場するものの数は多いですが、等式は二つです。
A [ A [ ( FMap U ( TMap ε b )) o ( TMap η ( FObj U b )) ] ≈ id1 A (FObj U b) ]
B [ B [ ( TMap ε ( FObj F a )) o ( FMap F ( TMap η a )) ] ≈ id1 B (FObj F a) ]
教科書風に書くと、UεoηU = 1_U, εFoFη = 1_F です。
Hom A a (FObj U b ) と Hom B (FObj F a ) b が一対一であるという性質でもあります。また、Universal mapping problem (普遍写像問題)とも対応しています。残念ながら、これらの証明は煩雑なので、ちょっと後回しにして、Monad との対応を先に示します。
まず、UεF を定義します。これは U(ε(F(a))) だったりするので、自然変換とFunctor の結合を先に定義します。
Functor*Nat : {c₁ c₂ ℓ c₁' c₂' ℓ' c₁'' c₂'' ℓ'' : Level} (A : Category c₁ c₂ ℓ) {B : Category c₁' c₂' ℓ'} (C : Category c₁'' c₂'' ℓ'')
(F : Functor B C) -> { G H : Functor A B } -> ( n : NTrans A B G H ) -> NTrans A C (F ○ G) (F ○ H)
Functor*Nat A {B} C F {G} {H} n = record {
TMap = \a -> FMap F (TMap n a)
; isNTrans = record {
commute = commute
}
} where
commute : {a b : Obj A} {f : Hom A a b}
→ C [ C [ (FMap F ( FMap H f )) o ( FMap F (TMap n a)) ] ≈ C [ (FMap F (TMap n b )) o (FMap F (FMap G f)) ] ]
commute {a} {b} {f} = let open ≈-Reasoning (C) in
begin
(FMap F ( FMap H f )) o ( FMap F (TMap n a))
≈⟨ sym (distr F) ⟩
FMap F ( B [ (FMap H f) o TMap n a ])
≈⟨ IsFunctor.≈-cong (isFunctor F) ( nat n ) ⟩
FMap F ( B [ (TMap n b ) o FMap G f ] )
≈⟨ distr F ⟩
(FMap F (TMap n b )) o (FMap F (FMap G f))
∎
Nat*Functor : {c₁ c₂ ℓ c₁' c₂' ℓ' c₁'' c₂'' ℓ'' : Level} (A : Category c₁ c₂ ℓ) {B : Category c₁' c₂' ℓ'} (C : Category c₁'' c₂'' ℓ'')
{ G H : Functor B C } -> ( n : NTrans B C G H ) -> (F : Functor A B) -> NTrans A C (G ○ F) (H ○ F)
Nat*Functor A {B} C {G} {H} n F = record {
TMap = \a -> TMap n (FObj F a)
; isNTrans = record {
commute = commute
}
} where
commute : {a b : Obj A} {f : Hom A a b}
→ C [ C [ ( FMap H (FMap F f )) o ( TMap n (FObj F a)) ] ≈ C [ (TMap n (FObj F b )) o (FMap G (FMap F f)) ] ]
commute {a} {b} {f} = IsNTrans.commute ( isNTrans n)
証明なので長くなりますが、
Fη : TMap = \a -> FMap F (TMap η a)
ηF : TMap = \a -> TMap η (FObj F a)
というだけです。Functor は対象と射の二つの写像を持ってますが、同じ記号を polymorphic に使っているわけですが、Agda では FObj, FMap
と違う名前になっています。Functor の分配法則があるので、Fηが正しく定義されるわけです。
これを使って、UεF を定義します。
UεF : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
( U : Functor B A )
( F : Functor A B )
( ε : NTrans B B ( F ○ U ) identityFunctor ) → NTrans A A (( U ○ F ) ○ ( U ○ F )) ( U ○ F )
UεF A B U F ε = lemma11 (
Functor*Nat A {B} A U {( F ○ U) ○ F} {identityFunctor ○ F} ( Nat*Functor A {B} B { F ○ U} {identityFunctor} ε F) ) where
lemma11 : NTrans A A ( U ○ ((F ○ U) ○ F )) ( U ○ (identityFunctor ○ F) )
→ NTrans A A (( U ○ F ) ○ ( U ○ F )) ( U ○ F )
lemma11 n = record { TMap = \a → TMap n a; isNTrans = record { commute = IsNTrans.commute ( isNTrans n ) }}
一つ、lemma を挟んでいるのでは、(( U ○ F ) ○ ( U ○ F )) ( U ○ F ) という要求されている型 T ○ T -> T に変換するためです。一度、record に分解してしまえば、Functor の合成は写像の合成ですから、Agda が推論してくれるわけです。射の結合の場合は手で assoc とかやらないといけなかったのですが、これは楽です。lemma11 の引数 n に Functor*Nat で作成した自然変換が入っています。
そして、Monad を作ります。
Adj2Monad : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
{ U : Functor B A }
{ F : Functor A B }
{ η : NTrans A A identityFunctor ( U ○ F ) }
{ ε : NTrans B B ( F ○ U ) identityFunctor } →
Adjunction A B U F η ε → Monad A (U ○ F) η (UεF A B U F ε)
Adj2Monad A B {U} {F} {η} {ε} adj = record {
isMonad = record {
assoc = assoc1;
unity1 = unity1;
unity2 = unity2
}
} where
T : Functor A A
T = U ○ F
μ : NTrans A A ( T ○ T ) T
μ = UεF A B U F ε
record の要素を定義していけば良いだけですが、三つの性質を証明する必要があります。ηは既に定義されています。
unity1 : {a : Obj A} → A [ A [ TMap μ a o TMap η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
unity1 {a} = let open ≈-Reasoning (A) in
begin
TMap μ a o TMap η ( FObj T a )
≈⟨⟩
(FMap U (TMap ε ( FObj F a ))) o TMap η ( FObj U ( FObj F a ))
≈⟨ IsAdjunction.adjoint1 ( isAdjunction adj ) ⟩
id (FObj U ( FObj F a ))
≈⟨⟩
id (FObj T a)
∎
unity1 は比較的簡単です。展開すると Adjoint の性質をすぐに使うことができます。
unity2 : {a : Obj A} → A [ A [ TMap μ a o (FMap T (TMap η a ))] ≈ Id {_} {_} {_} {A} (FObj T a) ]
unity2 {a} = let open ≈-Reasoning (A) in
begin
TMap μ a o (FMap T (TMap η a ))
≈⟨⟩
(FMap U (TMap ε ( FObj F a ))) o (FMap U ( FMap F (TMap η a )))
≈⟨ sym (distr U ) ⟩
FMap U ( B [ (TMap ε ( FObj F a )) o ( FMap F (TMap η a )) ])
≈⟨ (IsFunctor.≈-cong (isFunctor U)) (IsAdjunction.adjoint2 ( isAdjunction adj )) ⟩
FMap U ( id1 B (FObj F a) )
≈⟨ IsFunctor.identity ( isFunctor U ) ⟩
id (FObj T a)
∎
unity2 も若干の展開が必要なだけです。T と U ○ F の変換はAgdaの型推論の範囲内であり、わざわざ推論する必要はありません。unity1、unity2 が、それぞれ adjoin1, adjoin2 と対応していることがわかります。
assoc1 : {a : Obj A} → A [ A [ TMap μ a o TMap μ ( FObj T a ) ] ≈ A [ TMap μ a o FMap T (TMap μ a) ] ]
assoc1 {a} = let open ≈-Reasoning (A) in
begin
TMap μ a o TMap μ ( FObj T a )
≈⟨⟩
(FMap U (TMap ε ( FObj F a ))) o (FMap U (TMap ε ( FObj F ( FObj U (FObj F a )))))
≈⟨ sym (distr U) ⟩
FMap U (B [ TMap ε ( FObj F a ) o TMap ε ( FObj F ( FObj U (FObj F a ))) ] )
≈⟨ (IsFunctor.≈-cong (isFunctor U)) (lemma-assoc1 ( TMap ε (FObj F a ))) ⟩
FMap U (B [ (TMap ε ( FObj F a )) o FMap F (FMap U (TMap ε ( FObj F a ))) ] )
≈⟨ distr U ⟩
(FMap U (TMap ε ( FObj F a ))) o FMap U (FMap F (FMap U (TMap ε ( FObj F a ))))
≈⟨⟩
TMap μ a o FMap T (TMap μ a)
∎
問題は assoc です。cong を使いたいところですが、≈-cong でなんとかします。
lemma-assoc1 : {a b : Obj B} → ( f : Hom B a b) →
B [ B [ f o TMap ε a ] ≈ B [ TMap ε b o FMap F (FMap U f ) ] ]
lemma-assoc1 f = IsNTrans.commute ( isNTrans ε )
ここで、εの可換性を使っています。Adjoint の性質は、二つの等式だけでなく、自然変換やFunctor自体の性質も含まれているわけです。
これで、Adjoint から Monad を導くことができました。