Kleisli Category の Comparison Functor

Menu Menu

top : Agda による圏論入門


Kleisli 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) ]

の必要性が、この二つの証明から出てくることがわかります。

Next : Elienberg-Moore 圏の構成と Resolution


Shinji KONO / Sat Jan 20 16:41:54 2018