Kleisli Category の Comparison Functor
Menu MenuKleisli Category の Comparison Functor
examples/comparison-functor.agdai Monad の Resolution (UR,FR,εR) があると、その Adjoint Functor は、Kleisli Category の U_T, F_T と Comparison Functor K_T を通して関連します。ここでも問題になるのは、T と UR ○ FR が同じものなのに型が違うということです。
T=UF : T ≃ (UR ○ FR)があるのだから変換できるだろうと思うし、実際、
KtoT : (a b : Obj A) -> (RHom a b) -> {g h : Hom A (FObj ( U_K ○ F_K ) b) (FObj T b) } ->
([ A ] g ~ h) -> Hom A a (FObj T b)
KtoT _ _ f {g} {h} (Category.Cat.refl eq) = A [ g o (KMap f) ]
KTMap : {a b : Obj A} -> (f : RHom a b) -> Hom A a (FObj T b)
KTMap {a} {b} f = KtoT a b f {_} {_} (( ≃-sym (T=UF RK)) (id1 A b))
とかで変換しようと思えばできなくはないようです。 T ≃ (UR ○ FR) を [ A ] g ~ h で受けて、左辺と右辺を取り出すというような方法です。なのですが、どうしてもうまく行かず。「よくわからないがとにかく等しい」というのを扱うのは難しい。
でも、Adjoint があるので、それから Monad を構成すると、それは、(UR ○ FR) に対して定義された Monad になります。Resolution なのだから、それは元の Monad と同じはず。T と μ が等しい以上の意味はないわけですけど。この方針だと型は合います。
KTMap のような変換を使うのと証明の形自体は変わりません。 Comparison Functor の証明
まず、module のparameterとして、いろいろなものを定義します。
module comparison-functor
{ c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ }
{ T : Functor A A }
{ η : NTrans A A identityFunctor T }
{ μ : NTrans A A (T ○ T) T }
{ M' : Monad A T η μ }
{c₁' c₂' ℓ' : Level} ( B : Category c₁' c₂' ℓ' )
{ U_K : Functor B A } { F_K : Functor A B }
{ η_K : NTrans A A identityFunctor ( U_K ○ F_K ) }
{ ε_K : NTrans B B ( F_K ○ U_K ) identityFunctor }
{ μ_K' : NTrans A A (( U_K ○ F_K ) ○ ( U_K ○ F_K )) ( U_K ○ F_K ) }
( AdjK : Adjunction A B U_K F_K η_K ε_K )
( RK : MResolution A B T U_K F_K {η_K} {ε_K} {μ_K'} AdjK )
where
open import adj-monad
T_K = U_K ○ F_K
μ_K : NTrans A A (( U_K ○ F_K ) ○ ( U_K ○ F_K )) ( U_K ○ F_K )
μ_K = UεF A B U_K F_K ε_K
M : Monad A (U_K ○ F_K ) η_K μ_K
M = Adj2Monad A B {U_K} {F_K} {η_K} {ε_K} AdjK
open import kleisli {c₁} {c₂} {ℓ} {A} { U_K ○ F_K } { η_K } { μ_K } { M }
μ_K は UεF として作り、Adjunction AdjK から Monad M を作ります。その Monad に対して Kleisli Category を作ってやります。これで Resolution、Monad、Kleisli Category と道具立てはそろいました。
Functor K_T は、対象は F_K(a) で、射は ε(F_K b) o F_K(f) です。f は Hom A a b です。
open Functor
open NTrans
open KleisliHom
open Adjunction
open MResolution
kfmap : {a b : Obj A} (f : KHom a b) -> Hom B (FObj F_K a) (FObj F_K b)
kfmap {_} {b} f = B [ TMap ε_K (FObj F_K b) o FMap F_K (KMap f) ]
K_T : Functor KleisliCategory B
K_T = record {
FObj = FObj F_K
; FMap = kfmap
; isFunctor = record
{ ≈-cong = ≈-cong
; identity = identity
; distr = distr1
}
} where
identity : {a : Obj A} → B [ kfmap (K-id {a}) ≈ id1 B (FObj F_K a) ]
identity {a} = let open ≈-Reasoning (B) in
begin
kfmap (K-id {a})
≈⟨⟩
TMap ε_K (FObj F_K a) o FMap F_K (KMap (K-id {a}))
≈⟨⟩
TMap ε_K (FObj F_K a) o FMap F_K (TMap η_K a)
≈⟨ IsAdjunction.adjoint2 (isAdjunction AdjK) ⟩
id1 B (FObj F_K a)
∎
≈-cong : {a b : Obj A} -> {f g : KHom a b} → A [ KMap f ≈ KMap g ] → B [ kfmap f ≈ kfmap g ]
≈-cong {a} {b} {f} {g} f≈g = let open ≈-Reasoning (B) in
begin
kfmap f
≈⟨⟩
TMap ε_K (FObj F_K b) o FMap F_K (KMap f)
≈⟨ cdr ( fcong F_K f≈g) ⟩
TMap ε_K (FObj F_K b) o FMap F_K (KMap g)
≈⟨⟩
kfmap g
∎
identity と ≈-cong は簡単に証明できます。分配則は元の圏が Kleisli 圏なので厄介です。* が join です。
distr1 : {a b c : Obj A} {f : KHom a b} {g : KHom b c} → B [ kfmap (g * f) ≈ (B [ kfmap g o kfmap f ] )]
distr1 {a} {b} {c} {f} {g} = let open ≈-Reasoning (B) in
begin
kfmap (g * f)
≈⟨⟩
TMap ε_K (FObj F_K c) o FMap F_K (KMap (g * f))
≈⟨⟩
TMap ε_K (FObj F_K c) o FMap F_K (A [ TMap μ_K c o A [ FMap ( U_K ○ F_K ) (KMap g) o KMap f ] ] )
≈⟨ cdr ( distr F_K ) ⟩
TMap ε_K (FObj F_K c) o ( FMap F_K (TMap μ_K c) o ( FMap F_K (A [ FMap ( U_K ○ F_K ) (KMap g) o KMap f ])))
≈⟨ cdr (cdr ( distr F_K )) ⟩
TMap ε_K (FObj F_K c) o ( FMap F_K (TMap μ_K c) o (( FMap F_K (FMap ( U_K ○ F_K ) (KMap g))) o (FMap F_K (KMap f))))
≈⟨ cdr assoc ⟩
TMap ε_K (FObj F_K c) o ((( FMap F_K (TMap μ_K c) o ( FMap F_K (FMap (U_K ○ F_K) (KMap g))))) o (FMap F_K (KMap f)))
≈⟨⟩
TMap ε_K (FObj F_K c) o (( FMap F_K ( FMap U_K ( TMap ε_K ( FObj F_K c ) )) o
( FMap F_K (FMap (U_K ○ F_K) (KMap g)))) o (FMap F_K (KMap f)))
≈⟨ sym (cdr assoc) ⟩
TMap ε_K (FObj F_K c) o (( FMap F_K ( FMap U_K ( TMap ε_K ( FObj F_K c ) ))) o
(( FMap F_K (FMap (U_K ○ F_K) (KMap g))) o (FMap F_K (KMap f))))
≈⟨ assoc ⟩
(TMap ε_K (FObj F_K c) o ( FMap F_K ( FMap U_K ( TMap ε_K ( FObj F_K c ) )))) o
(( FMap F_K (FMap (U_K ○ F_K) (KMap g))) o (FMap F_K (KMap f)))
≈⟨ car (sym (nat ε_K)) ⟩
(TMap ε_K (FObj F_K c) o ( TMap ε_K (FObj (F_K ○ U_K) (FObj F_K c)))) o
(( FMap F_K (FMap (U_K ○ F_K) (KMap g))) o (FMap F_K (KMap f)))
≈⟨ sym assoc ⟩
TMap ε_K (FObj F_K c) o (( TMap ε_K (FObj (F_K ○ U_K) (FObj F_K c))) o
((( FMap F_K (FMap (U_K ○ F_K) (KMap g)))) o (FMap F_K (KMap f))))
≈⟨ cdr assoc ⟩
TMap ε_K (FObj F_K c) o ((( TMap ε_K (FObj (F_K ○ U_K) (FObj F_K c))) o
(( FMap F_K (FMap (U_K ○ F_K) (KMap g))))) o (FMap F_K (KMap f)))
≈⟨ cdr ( car (
begin
TMap ε_K (FObj (F_K ○ U_K) (FObj F_K c)) o ((FMap F_K (FMap (U_K ○ F_K) (KMap g))))
≈⟨⟩
TMap ε_K (FObj (F_K ○ U_K) (FObj F_K c)) o (FMap (F_K ○ U_K) (FMap F_K (KMap g)))
≈⟨ sym (nat ε_K) ⟩
( FMap F_K (KMap g)) o (TMap ε_K (FObj F_K b))
∎
)) ⟩
TMap ε_K (FObj F_K c) o ((( FMap F_K (KMap g)) o (TMap ε_K (FObj F_K b))) o FMap F_K (KMap f))
≈⟨ cdr (sym assoc) ⟩
TMap ε_K (FObj F_K c) o (( FMap F_K (KMap g)) o (TMap ε_K (FObj F_K b) o FMap F_K (KMap f)))
≈⟨ assoc ⟩
(TMap ε_K (FObj F_K c) o FMap F_K (KMap g)) o (TMap ε_K (FObj F_K b) o FMap F_K (KMap f))
≈⟨⟩
kfmap g o kfmap f
∎
わお。でも、こちらで使われているのは自然変換の可換性だけです。
これで Functor はできたので、あとは性質を見ていくだけです。
Lemma-K1 : {a b : Obj A} ( f : Hom A a b ) -> B [ FMap K_T ( FMap F_T f) ≈ FMap F_K f ]
Lemma-K1 {a} {b} f = let open ≈-Reasoning (B) in
begin
FMap K_T ( FMap F_T f)
≈⟨⟩
TMap ε_K (FObj F_K b) o FMap F_K (KMap( FMap F_T f))
≈⟨⟩
TMap ε_K (FObj F_K b) o FMap F_K (A [ TMap η_K b o f ])
≈⟨ cdr ( distr F_K) ⟩
TMap ε_K (FObj F_K b) o (FMap F_K (TMap η_K b) o FMap F_K f )
≈⟨ assoc ⟩
(TMap ε_K (FObj F_K b) o FMap F_K (TMap η_K b)) o FMap F_K f
≈⟨ car ( IsAdjunction.adjoint2 (isAdjunction AdjK)) ⟩
id1 B (FObj F_K b) o FMap F_K f
≈⟨ idL ⟩
FMap F_K f
∎
Lemma-K2 : {a b : Obj A} ( f : KHom a b ) -> A [ FMap U_K ( FMap K_T f) ≈ FMap U_T f ]
Lemma-K2 {a} {b} f = let open ≈-Reasoning (A) in
begin
FMap U_K ( FMap K_T f)
≈⟨⟩
FMap U_K ( B [ TMap ε_K (FObj F_K b) o FMap F_K (KMap f) ] )
≈⟨ distr U_K ⟩
FMap U_K ( TMap ε_K (FObj F_K b)) o FMap U_K (FMap F_K (KMap f) )
≈⟨⟩
TMap μ_K b o FMap T_K (KMap f)
≈⟨⟩ -- the definition
FMap U_T f
∎
この二つにより、
(K_T ○ F_T) ≃ F_K
(U_K ○ K_T) ≃ U_T
を証明することができます。任意の Resolution F_K, U_K は、Comparison Functor K_T により、Kleisli Category
による Resolution と結び付けられます。
kfmap {_} {b} f = B [ TMap ε_K (FObj F_K b) o FMap F_K (KMap f) ]
の必要性が、この二つの証明から出てくることがわかります。