Mercurial > hg > Members > kono > Proof > category

changeset 440:ff36c500962e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix limit
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 30 Aug 2016 14:22:47 +0900
parents bc0682b86b91
children 61550782be4a
files cat-utility.agda equalizer.agda freyd.agda limit-to.agda pullback.agda
diffstat 5 files changed, 76 insertions(+), 42 deletions(-) [+]
line wrap: on
line diff
--- a/cat-utility.agda	Tue Aug 30 01:40:56 2016 +0900
+++ b/cat-utility.agda	Tue Aug 30 14:22:47 2016 +0900
@@ -180,6 +180,12 @@
            equalizer : Hom A c a
            equalizer = e
 
+        record CreateEqualizer { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) : Set  (ℓ ⊔ (c₁ ⊔ c₂)) where
+           field
+                equalizer : {a b : Obj A} (f g : Hom A a b)  -> Obj A
+                equalizer-e : {a b : Obj A} (f g : Hom A a b)  -> Hom A (equalizer f g ) a
+                isEqualizer : {a b : Obj A} (f g : Hom A a b)  -> Equalizer A (equalizer-e f g ) f g 
+
         -- 
         -- Product
         --
@@ -201,12 +207,14 @@
               π2fxg=g : {c : Obj A} { f : Hom A c a } → { g : Hom A c b } → A [ A [ π2  o ( f × g )  ] ≈  g ]
               uniqueness : {c : Obj A} { h : Hom A c ab }  → A [  ( A [ π1  o h  ] ) × ( A [ π2  o h  ] ) ≈  h ]
               ×-cong : {c : Obj A} { f f' : Hom A c a } → { g g' : Hom A c b } → A [ f ≈ f' ] → A [ g ≈ g' ] → A [ f × g ≈ f' × g' ] 
-           axb : Obj A
-           axb = ab
-           pi1 : Hom A ab a 
-           pi1  = π1 
-           pi2 : Hom A ab b 
-           pi2  = π2 
+
+        record CreateProduct { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  
+                    : Set  (ℓ ⊔ (c₁ ⊔ c₂)) where
+           field
+              product : (a b : Obj A) -> Obj A
+              π1 : (a b : Obj A) -> Hom A (product a b ) a 
+              π2 : (a b : Obj A) -> Hom A (product a b ) b 
+              isProduct : (a b : Obj A) -> Product A a b (product  a b) (π1 a b ) (π2 a b)
 
         -- Pullback
         --         f
@@ -267,10 +275,32 @@
              limit :  ( a : Obj A ) → ( t : NTrans I A ( K A I a ) Γ ) → Hom A a a0
              t0f=t :  { a : Obj A } → { t : NTrans I A ( K A I a ) Γ } → ∀ { i : Obj I } →
                  A [ A [ TMap t0 i o  limit a t ]  ≈ TMap t i ]
-             limit-uniqueness : { a : Obj A } →  { t : NTrans I A ( K A I a ) Γ } → { f : Hom A a a0 } → ( ∀ { i : Obj I } →
+             limit-uniqueness : { a : Obj A } →  { t : NTrans I A ( K A I a ) Γ } → ( f : Hom A a a0 ) → ( ∀ { i : Obj I } →
                  A [ A [ TMap t0 i o  f ]  ≈ TMap t i ] ) → A [ limit a t ≈ f ]
           A0 : Obj A
           A0 = a0
           T0 : NTrans I A ( K A I a0 ) Γ
           T0 = t0
 
+        record CreateLimit { c₁' c₂' ℓ' : Level} { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Category c₁' c₂' ℓ' ) 
+                : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where
+          field
+             limit-c :  ( Γ : Functor I A ) -> Obj A 
+             limit-u :  ( Γ : Functor I A ) -> NTrans I A ( K A I (limit-c Γ) ) Γ 
+             isLimit :  ( Γ : Functor I A ) -> Limit A I Γ (limit-c Γ) (limit-u Γ)
+
+        record Complete { c₁' c₂' ℓ' : Level} { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Category c₁' c₂' ℓ' ) 
+                : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where
+          field
+             limit-c :  ( Γ : Functor I A ) -> Obj A 
+             limit-u :  ( Γ : Functor I A ) -> NTrans I A ( K A I (limit-c Γ) ) Γ 
+             isLimit :  ( Γ : Functor I A ) -> Limit A I Γ (limit-c Γ) (limit-u Γ)
+
+             product : (a b : Obj A) -> Obj A
+             π1 : (a b : Obj A) -> Hom A (product a b ) a 
+             π2 : (a b : Obj A) -> Hom A (product a b ) b 
+             isProduct : (a b : Obj A) -> Product A a b (product  a b) (π1 a b ) (π2 a b)
+
+             equalizer-p : {a b : Obj A} (f g : Hom A a b)  -> Obj A
+             equalizer-e : {a b : Obj A} (f g : Hom A a b)  -> Hom A (equalizer-p f g) a
+             isEqualizer : {a b : Obj A} (f g : Hom A a b)  -> Equalizer A (equalizer-e f g) f g 
--- a/equalizer.agda	Tue Aug 30 01:40:56 2016 +0900
+++ b/equalizer.agda	Tue Aug 30 14:22:47 2016 +0900
@@ -247,7 +247,7 @@
               → Burroni A {c} {a} {b} f g e
 lemma-equ1  {a} {b} {c} f g e eqa  = record {
       α = λ {a} {b} {c}  f g e  →  equalizer (eqa {a} {b} {c} f g {e} ) ; -- Hom A c a
-      γ = λ {a} {b} {c} {d} f g h → k (eqa f g ) {d} ( A [ h  o (equalizer ( eqa (A [ f  o  h ] ) (A [ g o h ] ))) ] ) 
+      γ = λ {a} {b} {c} {d} f g h → k (eqa {a} {b} {c} f g ) {d} ( A [ h  o (equalizer ( eqa (A [ f  o  h ] ) (A [ g o h ] ))) ] ) 
                             (lemma-equ4 {a} {b} {c} {d} f g h ) ;  -- Hom A c d
       δ =  λ {a} {b} {c} e f → k (eqa {a} {b} {c} f f {e} ) (id1 A a)  (f1=f1 f); -- Hom A a c
       cong-α = λ {a b c e f g g'} eq → cong-α1 {a} {b} {c} {e} {f} {g} {g'} eq ;
@@ -256,7 +256,7 @@
       b1 = fe=ge (eqa {a} {b} {c} f g {e}) ;
       b2 = lemma-b2 ;
       b3 = lemma-b3 ;
-      b4 = lemma-b4
+      b4 = lemma-b4 
  } where
      --
      --           e eqa f g        f
--- a/freyd.agda	Tue Aug 30 01:40:56 2016 +0900
+++ b/freyd.agda	Tue Aug 30 14:22:47 2016 +0900
@@ -40,45 +40,49 @@
 open Limit
 open SmallFullSubcategory
 open PreInitial
+open Complete
+open Equalizer
 
 initialFromPreInitialFullSubcategory : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
       (F : Functor A A ) ( FMap← : { a b : Obj A } → Hom A (FObj F a) (FObj F b ) → Hom A a b )
-      (lim : ( Γ : Functor A A ) → { a0 : Obj A } { u : NTrans A A ( K A A a0 ) Γ } → Limit A A Γ a0 u ) -- completeness
-      ( equ : {a b c : Obj A} → (f g : Hom A a b)  → {e : Hom A c a }  → Equalizer A e f g )
+      (comp : Complete A A)
       (SFS : SmallFullSubcategory A F FMap← ) → 
-      (PI : PreInitial A F ) → { a0 : Obj A } → 
-      { ee : {a b : Obj A} → {f g : Hom A a b}  → Obj A }
-      { ep :  {a b : Obj A} → {f g : Hom A a b}  → Hom A (ee {a} {b} {f} {g} ) a }
-      { u : (a : Obj A) → NTrans A A (K A A a) F }  
-          → HasInitialObject A a0
-initialFromPreInitialFullSubcategory A F  FMap← lim equ SFS PI {a0} {ee} {ep} {u} = record {
+      (PI : PreInitial A F ) → { a0 : Obj A } → HasInitialObject A (limit-c comp F)
+initialFromPreInitialFullSubcategory A F  FMap← comp SFS PI = record {
       initial = initialArrow ; 
       uniqueness  = λ a f → lemma1 a f
     } where
+      lim : ( Γ : Functor A A ) → Limit A A Γ (limit-c comp Γ)  (limit-u comp Γ)
+      lim Γ =  isLimit comp Γ 
+      equ : {a b : Obj A} → (f g : Hom A a b)  → Equalizer A (equalizer-e comp f g ) f g
+      equ f g = isEqualizer comp f g 
+      a0 = limit-c comp F
+      u = limit-u comp F
+      ee : {a b : Obj A} → {f g : Hom A a b}  → Obj A 
+      ee {a} {b} {f} {g} = equalizer-p comp f g
+      ep :  {a b : Obj A} → {f g : Hom A a b}  → Hom A (ee {a} {b} {f} {g} ) a 
+      ep {a} {b} {f} {g} = equalizer-e comp f g  
       f : {a : Obj A} -> Hom A  a0 (FObj F  (preinitialObj PI {a} ) ) 
-      f {a} = limit (lim F {FObj F (preinitialObj PI {a} )} {u (FObj F (preinitialObj PI))} ) a0 (u a0 )  
+      f {a} = TMap u (preinitialObj PI {a} ) 
       initialArrow :  ∀( a : Obj A )  →  Hom A a0 a
       initialArrow a  = A [ preinitialArrow PI {a}  o f ]
-      limit-u : Limit A A F a0 (u a0)
-      limit-u = lim F {a0} {u a0}
-      equ-fi : { a c : Obj A} -> { p : Hom A c a0 } -> {f' : Hom A a0 a} -> 
-          Equalizer A p ( A [ preinitialArrow PI {a} o  f ] ) f'
-      equ-fi  {a} {c} {p} {f'} = equ ( A [ preinitialArrow PI {a} o  limit (lim F) a0 (u a0) ] ) f'
-      e=id : {e : Hom A a0 a0} -> ( {c : Obj A} -> A [ A [ TMap (u a0)  c o  e ]  ≈  TMap (u a0) c ] ) -> A [ e  ≈ id1 A a0 ]
+      equ-fi : { a : Obj A} -> {f' : Hom A a0 a} -> 
+          Equalizer A ep ( A [ preinitialArrow PI {a} o  f ] ) f'
+      equ-fi  {a} {f'} = equ ( A [ preinitialArrow PI {a} o  f ] ) f'
+      e=id : {e : Hom A a0 a0} -> ( {c : Obj A} -> A [ A [ TMap u  c o  e ]  ≈  TMap u c ] ) -> A [ e  ≈ id1 A a0 ]
       e=id  {e} uce=uc =  let open ≈-Reasoning (A) in
             begin
               e
-            ≈↑⟨ limit-uniqueness limit-u {a0} {u a0} {e} ( \{i} -> uce=uc ) ⟩
-              limit limit-u a0 (u a0)
-            ≈⟨ limit-uniqueness limit-u {a0} {u a0} {id1 A a0} ( \{i} -> idR ) ⟩
+            ≈↑⟨ limit-uniqueness  (lim F) e ( \{i} -> uce=uc ) ⟩
+              limit (lim F) a0 u 
+            ≈⟨ limit-uniqueness (lim F) (id1 A a0) ( \{i} -> idR ) ⟩
               id1 A a0
             ∎
-      open Equalizer
-      kfuc=uc : {c k1 : Obj A} ->  {p : Hom A k1 a0} -> A [ A [ TMap (u a0)  c  o  
-              A [ p o A [ preinitialArrow PI {k1} o TMap (u a0) (preinitialObj PI) ] ] ]  
-                      ≈ TMap (u a0) c ]
+      kfuc=uc : {c k1 : Obj A} ->  {p : Hom A k1 a0} -> A [ A [ TMap u  c  o  
+              A [ p o A [ preinitialArrow PI {k1} o TMap u (preinitialObj PI) ] ] ]  
+                      ≈ TMap u c ]
       kfuc=uc {k1} {c} = {!!}
-      kfuc=1 : {k1 : Obj A} ->  {p : Hom A k1 a0} -> A [ A [ p o A [ preinitialArrow PI {k1} o TMap (u a0) (preinitialObj PI) ] ] ≈ id1 A a0 ]
+      kfuc=1 : {k1 : Obj A} ->  {p : Hom A k1 a0} -> A [ A [ p o A [ preinitialArrow PI {k1} o TMap u (preinitialObj PI) ] ] ≈ id1 A a0 ]
       kfuc=1 {k1} {p} = e=id ( kfuc=uc )
       -- if equalizer has right inverse, f = g
       lemma2 :  (a b : Obj A) {c : Obj A} ( f g : Hom A a b ) 
@@ -109,8 +113,8 @@
              begin
                  initialArrow a
              ≈⟨⟩
-                 preinitialArrow PI {a} o  limit (lim F) a0 (u a0) 
-             ≈⟨ lemma2 a0 a (A [ preinitialArrow PI {a} o  limit (lim F) a0 (u a0) ]) f' {ep {a0} {a} {f'} {f'} } equ-fi 
+                 preinitialArrow PI {a} o  f
+             ≈⟨ lemma2 a0 a (A [ preinitialArrow PI {a} o  f ]) f' {ep {a0} {a} {A [ preinitialArrow PI {a} o  f ]} {f'} } (equ-fi )
                       (kfuc=1 {ee} {ep} ) ⟩
                  f'
              ∎  )
--- a/limit-to.agda	Tue Aug 30 01:40:56 2016 +0900
+++ b/limit-to.agda	Tue Aug 30 14:22:47 2016 +0900
@@ -590,7 +590,7 @@
                 → A [ A [ e o k' ] ≈ h ] → A [ k h fh=gh ≈ k' ]
          uniquness d h fh=gh k' ek'=h =   begin
                     k h fh=gh
-                ≈⟨ limit-uniqueness eqlim {d} {nat1 d h fh=gh } {k'} ( λ{i} → uniq-nat {i} d h k' ek'=h ) ⟩
+                ≈⟨ limit-uniqueness eqlim k' ( λ{i} → uniq-nat {i} d h k' ek'=h ) ⟩
                     k'
                 ∎
 
--- a/pullback.agda	Tue Aug 30 01:40:56 2016 +0900
+++ b/pullback.agda	Tue Aug 30 14:22:47 2016 +0900
@@ -154,7 +154,7 @@
   A [ A [ iso-l I Γ a0 a0' t0 t0' lim lim' o iso-r I Γ a0 a0' t0 t0' lim lim'  ]  ≈ id1 A a0' ]
 iso-lr  I Γ a0 a0' t0 t0' lim lim' {i} =  let open ≈-Reasoning (A) in begin
            limit lim' a0 t0 o limit lim a0' t0'
-      ≈↑⟨ limit-uniqueness lim'  ( λ {i} → ( begin
+      ≈↑⟨ limit-uniqueness lim' ( limit lim' a0 t0 o limit lim a0' t0' )( λ {i} → ( begin
           TMap t0' i o ( limit lim' a0 t0 o limit lim a0' t0' )
       ≈⟨ assoc  ⟩
           ( TMap t0' i o  limit lim' a0 t0 ) o limit lim a0' t0'
@@ -164,7 +164,7 @@
           TMap t0' i
       ∎) ) ⟩
            limit lim' a0' t0'
-      ≈⟨ limit-uniqueness lim' idR ⟩
+      ≈⟨ limit-uniqueness lim' (id a0') idR ⟩
            id a0'
       ∎
 
@@ -242,7 +242,7 @@
          → A [ limit (lim b {a0 b} {t0 b} ) a f ≈ g ]
    couniquness2 {b} {a} {f} {g} lim-g=f  =  let  open ≈-Reasoning (A) in begin
             limit (lim b {a0 b} {t0 b} ) a f
-        ≈⟨ limit-uniqueness ( lim b {a0 b} {t0 b} ) lim-g=f ⟩
+        ≈⟨ limit-uniqueness ( lim b {a0 b} {t0 b} ) g lim-g=f ⟩
             g
         ∎
 
@@ -259,7 +259,7 @@
 univ2limit U ε univ Γ = record {
      limit = λ a t → limit1 a t ;
      t0f=t = λ {a t i } → t0f=t1 {a} {t} {i}  ;
-     limit-uniqueness =  λ {a} {t} {f} t=f → limit-uniqueness1 {a} {t} {f} t=f
+     limit-uniqueness =  λ {a} {t} f t=f → limit-uniqueness1 {a} {t} {f} t=f
  } where
      limit1 :  (a : Obj A) → NTrans I A (K A I a) Γ → Hom A a (U Γ)
      limit1 a t = _*' univ {_} {a} t
@@ -383,7 +383,7 @@
 limit-from prod eqa lim p e proj = record {
      limit = λ a t → limit1 a t ;
      t0f=t = λ {a t i } → t0f=t1 {a} {t} {i}  ;
-     limit-uniqueness =  λ {a} {t} {f} t=f → limit-uniqueness1 {a} {t} {f} t=f
+     limit-uniqueness =  λ {a} {t} f t=f → limit-uniqueness1 {a} {t} {f} t=f
     }  where
          limit1 :  (a : Obj A) → NTrans I A (K A I a) Γ → Hom A a lim
          limit1 a t = let  open ≈-Reasoning (A) in k (eqa e (id1 A p) (id1 A p )) (product ( prod p (FObj Γ)  proj ) (TMap t) ) refl-hom
@@ -455,7 +455,7 @@
 adjoint-preseve-limit B Γ lim tb limitb {U} {F} {η} {ε} adj = record {
      limit = λ a t → limit1 a t ;
      t0f=t = λ {a t i } → t0f=t1 {a} {t} {i}  ;
-     limit-uniqueness =  λ {a} {t} {f} t=f → limit-uniqueness1 {a} {t} {f} t=f
+     limit-uniqueness =  λ {a} {t} f t=f → limit-uniqueness1 {a} {t} {f} t=f
     } where
          ta = ta1 B Γ lim tb U
          tfmap : (a : Obj A) → NTrans I A (K A I a) (U ○ Γ) → (i : Obj I) → Hom B (FObj (K B I (FObj F a)) i) (FObj Γ i)
@@ -524,7 +524,7 @@
                  limit1 a t
                ≈⟨⟩
                  FMap U (limit limitb (FObj F a) (tF a t )) o TMap η a  
-               ≈⟨ car ( fcong U (limit-uniqueness limitb ( λ {i} →  lemma1 i) )) ⟩
+               ≈⟨ car ( fcong U (limit-uniqueness limitb (B [ TMap ε lim o FMap F f ] ) ( λ {i} →  lemma1 i) )) ⟩
                  FMap U ( B [ TMap ε lim o FMap F f ] ) o TMap η a   -- Universal mapping 
                ≈⟨ car (distr U ) ⟩
                  ( (FMap U (TMap ε lim))  o (FMap U ( FMap F f )) ) o TMap η a