Mercurial > hg > Members > kono > Proof > category

changeset 175:795be747d7a9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
hom-set to universal mapping done.
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 24 Aug 2013 22:14:29 +0900
parents 1c4788483d46
children ae1a4f7e5203
files cat-utility.agda universal-mapping.agda
diffstat 2 files changed, 54 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- a/cat-utility.agda	Sat Aug 24 17:16:07 2013 +0900
+++ b/cat-utility.agda	Sat Aug 24 22:14:29 2013 +0900
@@ -77,7 +77,7 @@
                              lemma-1 : {a : Obj A} {b b' : Obj B } ->
                                ( g : Hom A a (FObj U b))  -> ( k : Hom B b b' ) ->
                                 A [ A [ FMap U k o left ( right g ) ]   ≈  A [ FMap U k o g  ] ]
-                             lemma-1 = let open ≈-Reasoning (A) in
+                             lemma-1 g k = let open ≈-Reasoning (A) in
                                    begin
                                         FMap U k o left ( right g ) 
                                    ≈⟨ cdr ( right-injective) ⟩
@@ -86,8 +86,20 @@
            right-commute2 : {a a' : Obj A} {b : Obj B } ->
                        ( g : Hom A a (FObj U b) )  -> ( h : Hom A a' a ) ->
                         B [ B [ right g  o  FMap F h ]   ≈  right ( A [ g o h ] ) ]
-           right-commute2 = {!!}
-
+           right-commute2 g h =  let open ≈-Reasoning (B) in
+                     begin
+                          right g  o  FMap F h 
+                     ≈⟨  sym left-injective ⟩
+                          right ( left ( right g  o  FMap F h  ))
+                     ≈⟨ r-cong ( left-commute2 (right g) h ) ⟩
+                          right ( A [ left ( right g ) o h ] )
+                     ≈⟨ r-cong ( lemma-2 g h  ) ⟩
+                          right ( A [ g o h ] )
+                     ∎  where
+                           lemma-2 :  {a a' : Obj A} {b : Obj B } ->
+                               ( g : Hom A a (FObj U b))  -> ( h : Hom A a' a ) ->
+                                A [ A [  left ( right g ) o h ]   ≈  A [ g o h  ] ]
+                           lemma-2 g h  = let open ≈-Reasoning (A) in car ( right-injective  )
         open NTrans
         open import Category.Cat
         record IsAdjunction  {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') 
--- a/universal-mapping.agda	Sat Aug 24 17:16:07 2013 +0900
+++ b/universal-mapping.agda	Sat Aug 24 22:14:29 2013 +0900
@@ -346,7 +346,11 @@
             right =  right ;
             left  =  left ; 
             right-injective =  right-injective  ;
-            left-injective = left-injective  
+            left-injective = left-injective  ;
+            left-commute1 = left-commute1 ;
+            left-commute2 = left-commute2 ;
+            r-cong = r-cong ;
+            l-cong = l-cong 
       } where
             right  : {a : Obj A} { b : Obj B } → Hom A a ( FObj U b ) → Hom B (FObj F a) b
             right {a} {b} f = B [ TMap ε b o FMap F f ] 
@@ -386,6 +390,19 @@
                      ≈⟨ idR  ⟩
                         f
                      ∎
+            left-commute1 : {a : Obj A} {b b' : Obj B } ->
+                       ( f : Hom B (FObj F a) b )  -> ( k : Hom B b b' ) ->
+                        A [  left ( B [ k o  f ] )  ≈ A [ FMap U k o left f  ] ]
+            left-commute1 = {!!}
+            left-commute2 : {a a' : Obj A} {b : Obj B } ->
+                       ( f : Hom B (FObj F a) b )  -> ( h : Hom A a' a ) ->
+                        A [ left ( B [ f  o  FMap F h ] )  ≈  A [ left f o h ] ]
+            left-commute2 = {!!}
+            r-cong : {a : Obj A} { b : Obj B } → { f g : Hom A a ( FObj U b ) } →  A [ f  ≈ g ] → B [ right f ≈ right g ]
+            r-cong eq = let open ≈-Reasoning (B) in ( cdr ( fcong F  eq ) )
+            l-cong : {a : Obj A} { b : Obj B } → { f g : Hom B (FObj F a) b }   →  B [ f  ≈ g ] → A [ left f ≈ left g   ]
+            l-cong eq = let open ≈-Reasoning (A) in ( car ( fcong U  eq ) )
+
 
 open UnityOfOppsite
 
@@ -436,15 +453,29 @@
                     FMap U ( uo-solution A B U F uo f) o ( uo-η-map uo  ) a
                ≈⟨⟩
                     FMap U ( right uo  f) o left uo ( id1 B (FObj F a)  )
-               ≈⟨ {!!} ⟩
+               ≈↑⟨  left-commute1 uo ( id1 B (FObj F a)) ( right uo  f)  ⟩
+                    left uo ( B [  right uo  f o  id1 B (FObj F a) ] )
+               ≈⟨ l-cong uo lemma-1  ⟩
+                    left uo ( right uo f )
+               ≈⟨ right-injective uo ⟩
                     f
-               ∎
+               ∎ where
+                  lemma-1 :  B [ B [  right uo f o  id1 B (FObj F a) ] ≈ right uo f ]
+                  lemma-1 = let open ≈-Reasoning (B) in idR
          uniqueness :   {a' : Obj A} { b' : Obj B } → { f : Hom A a' (FObj U b') } → { g :  Hom B (FObj F a') b'} →
                      A [ A [ FMap U g o  ( uo-η-map uo  ) a' ]  ≈ f ] → B [ uo-solution A B U F uo f  ≈ g ]
          uniqueness {a} {b} {f} {g} eq = let open ≈-Reasoning (B) in
                begin
                     uo-solution A B U F uo f
-               ≈⟨ {!!} ⟩
+               ≈⟨⟩
+                    right uo  f
+               ≈↑⟨ r-cong uo eq ⟩
+                    right uo  ( A [  FMap U g o  left uo ( id1 B (FObj F a) ) ] )
+               ≈↑⟨ r-cong uo ( left-commute1 uo ( id1 B (FObj F a) ) g ) ⟩
+                    right uo ( left uo ( g  o ( id1 B (FObj F a) ) ) )
+               ≈⟨ left-injective uo  ⟩
+                    g  o ( id1 B (FObj F a) )
+               ≈⟨ idR ⟩
                     g
                ∎ 
 
@@ -458,18 +489,20 @@
                  { U : Functor B A }
                  { F : Functor A B }→  
                  ( uo : UnityOfOppsite A B U F)  → NTrans A A identityFunctor ( U ○  F )
-uo-η = {!!}
+uo-η  = {!!}
 
 UO2Adj : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
                  { U : Functor B A }
                  { F : Functor A B }
-                 ( uo : UnityOfOppsite A B U F)  → Adjunction A B U F (uo-η uo) (uo-ε uo )
+                 ( uo : UnityOfOppsite A B U F)  
+                    → Adjunction A B U F ( uo-η uo ) (uo-ε uo )
 UO2Adj A B {U} {F} uo = record {
            isAdjunction = record {
                adjoint1 = adjoint1 ; 
                adjoint2 = adjoint2
            } 
        } where
+          um = UO2UM A B U F uo 
           adjoint1 :   { b : Obj B } →
                      A [ A [ ( FMap U ( TMap (uo-ε uo) b ))  o ( TMap (uo-η uo) ( FObj U b )) ]  ≈ id1 A (FObj U b) ]
           adjoint1  {b} = {!!}