Mercurial > hg > Members > kono > Proof > category

changeset 172:c7fef385330f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
hmm
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 23 Aug 2013 15:38:03 +0900
parents d25b0948e006
children bf7f06580f5e
files universal-mapping.agda
diffstat 1 files changed, 88 insertions(+), 28 deletions(-) [+]
line wrap: on
line diff
--- a/universal-mapping.agda	Fri Aug 23 10:11:58 2013 +0900
+++ b/universal-mapping.agda	Fri Aug 23 15:38:03 2013 +0900
@@ -29,7 +29,7 @@
          _* = solution  ;
          isUniversalMapping = record {
                     universalMapping  = universalMapping;
-                    uniquness = uniqness
+                    uniquness = uniqueness
               }
       } where
          solution :  { a : Obj A} { b : Obj B} → ( f : Hom A a (FObj U b) ) →  Hom B (FObj F a ) b 
@@ -59,9 +59,9 @@
                 A [ A [ FMap U g o  TMap η a ]  ≈ f ] →
                 B [  (FMap F (A [ FMap U g o TMap η a ] )) ≈ FMap F f ] 
          lemma1 a b f g k = IsFunctor.≈-cong (isFunctor F) k
-         uniqness :   {a' : Obj A} { b' : Obj B } → { f : Hom A a' (FObj U b') } → { g :  Hom B (FObj F a') b'} → 
+         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  TMap η a' ]  ≈ f ] → B [ solution f  ≈ g ]
-         uniqness {a} {b} {f} {g} k = let open ≈-Reasoning (B) in
+         uniqueness {a} {b} {f} {g} k = let open ≈-Reasoning (B) in
               begin 
                   solution f 
               ≈⟨⟩
@@ -389,35 +389,89 @@
 
 open UnityOfOppsite
 
-uo-η  : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} {A : Category c₁ c₂ ℓ} {B : Category c₁' c₂' ℓ'} 
+--    f   :   a -> U(b)
+--    f*  : F(a)->   b
+
+--   U(f*) :     UF(a) ->   U(b)
+
+--   ∃g          F(g) = right f         <-----       left F(g) = f
+--   ∃g          UF(g) = U(f*)
+
+--   ∃f          U(f) = left g         <-----        right U(f) = g
+
+--   UF(f) :     UF(a) -> UFU(b)
+
+
+
+uo-η-map  : {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)  →  NTrans  A A identityFunctor ( U ○ F )
-uo-η {_} {_} {_} {_} {_} {_} {A} {B} {U} {F} uo = record {
-             TMap = η ; isNTrans = myIsNTrans
-       } where
-            η : (a : Obj A) → Hom A a ( FObj U (FObj F a) )  
-            η a = left uo ( id1 B (FObj F a) ) 
-            commute :  {a b : Obj A} {f : Hom A a b}
-              → A [ A [ (FMap U (FMap F f))  o  ( η a ) ]  ≈ A [ (η b ) o f ] ]
-            commute {a} {b} {f} =   let open ≈-Reasoning (A) in
+                 ( uo : UnityOfOppsite A B U F)  →  (a : Obj A )  → Hom A a (FObj U ( FObj F ( a ) ))
+uo-η-map {_} {_} {_} {_} {_} {_} {A} {B} {U} {F} uo a =  {!!} -- ? left uo ( id1 B (FObj F a) )
+
+uo-solution  : {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)  →  {a : Obj A} {b : Obj B } -> 
+                       ( f : Hom A a (FObj U b )) -> Hom B (FObj F a) b
+uo-solution A B U F uo {a} {b} f =  B  [ right uo (id1 A (FObj U b)) o FMap F f ] --   right uo f
+
+lemma-u1 :  {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)  →
+                {a : Obj A} {b : Obj B } -> ( f : Hom A a (FObj U b ))  ->
+        B [ B  [ right uo (id1 A (FObj U b)) o FMap F f ] ≈  right uo f ]
+lemma-u1 = {!!}
+
+lemma-u2 :  {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)  →
+                {a : Obj A} {b : Obj B } -> ( f* : Hom B (FObj F a ) b )  ->
+        A [ A  [ FMap U f*  o  left uo (id1 B (FObj F a)) ] ≈  left uo f* ]
+lemma-u2 = {!!}
+---   FMap U f*  o id  = FMap U f*
+---       left uo f * = FMap U f*
+---       left uo id1 = FMap U id = id
+--            f = right (FMap U f)
+
+lemma-u3 :  {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)  →
+                {a : Obj A} {b : Obj B } -> ( f* : Hom B (FObj F a ) b )  ->
+        B [  right uo ( FMap U f*) ≈  ? ]
+lemma-u3 = ?
+
+
+UO2UM  : {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)  → UniversalMapping A B U (FObj F) ( uo-η-map uo  )
+UO2UM  A B U F uo = record {
+         _* = uo-solution A B U F uo  ;
+         isUniversalMapping = record {
+                    universalMapping  = universalMapping;
+                    uniquness = uniqueness
+              }
+      } where
+         universalMapping :   {a' : Obj A} { b' : Obj B } → { f : Hom A a' (FObj U b') } →
+                     A [ A [ FMap U ( uo-solution A B U F uo f) o ( uo-η-map uo  ) a' ]  ≈ f ]
+         universalMapping {a} {b} {f}  = let open ≈-Reasoning (A) in
                begin
-                    (FMap U (FMap F f))  o  ( η a )
-               ≈⟨⟩
-                    (FMap U (FMap F f))  o left uo ( id1 B (FObj F a) )
+                    FMap U ( uo-solution A B U F uo f) o ( uo-η-map uo  ) a
                ≈⟨ {!!} ⟩
-                    left uo ( id1 B (FObj F b)) o f
-               ≈⟨⟩
-                    (η b ) o f
+                    f
                ∎
-            myIsNTrans : IsNTrans A A identityFunctor ( U ○  F ) η
-            myIsNTrans = record { commute = commute }
-
-UO2UM  : {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)  → UniversalMapping A B U (FObj F) (TMap (uo-η uo) )
-UO2UM  = {!!}
+         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
+               ≈⟨ {!!} ⟩
+                    g
+               ∎ 
 
 uo-ε  : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} {A : Category c₁ c₂ ℓ} {B : Category c₁' c₂' ℓ'}
                  { U : Functor B A }
@@ -425,10 +479,16 @@
                  ( uo : UnityOfOppsite A B U F)  → NTrans B B  ( F ○  U ) identityFunctor  
 uo-ε = {!!}
 
+uo-η  : {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)  → NTrans A A identityFunctor ( U ○  F )
+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 ;