Mercurial > hg > Members > kono > Proof > category

changeset 225:1a9f20917fbd

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
comment
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 05 Sep 2013 14:56:35 +0900
parents a9d311cea336
children 27f2c77c963f
files equalizer.agda
diffstat 1 files changed, 43 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- a/equalizer.agda	Thu Sep 05 11:39:06 2013 +0900
+++ b/equalizer.agda	Thu Sep 05 14:56:35 2013 +0900
@@ -31,7 +31,10 @@
    equalizer : Hom A c a
    equalizer = e
 
-record EqEqualizer { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  {c a b : Obj A} (f g : Hom A a b) : Set  (ℓ ⊔ (c₁ ⊔ c₂)) where
+-- 
+-- Flat Equational Definition of Equalizer
+-- 
+record Burroni { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  {c a b : Obj A} (f g : Hom A a b) : Set  (ℓ ⊔ (c₁ ⊔ c₂)) where
    field
       α : {a b c : Obj A } → (f : Hom A a b) → (g : Hom A a b ) →  Hom A c a
       γ : {a b c d : Obj A } → (f : Hom A a b) → (g : Hom A a b ) → (h : Hom A d a ) →  Hom A d c
@@ -46,8 +49,11 @@
    β {d} {e} {a} {b} f g h =  A [ γ {a} {b} {c} f g h o δ (A [ f o h ]) ] 
 
 open Equalizer
-open EqEqualizer
+open Burroni
 
+--
+-- Some obvious conditions for k  (fe = ge) → ( fh = gh )
+--
 
 f1=g1 : { a b c : Obj A } {f g : Hom A a b } → (eq : A [ f ≈ g ] ) → (h : Hom A c a) →  A [ A [ f o h ] ≈ A [ g o h ]  ]
 f1=g1 eq h = let open ≈-Reasoning (A) in (resp refl-hom eq )
@@ -65,6 +71,10 @@
                   g o ( e  o h )
              ∎
 
+--
+--  For e f f, we need e eqa = id1 A a, but it is equal to say k eqa (id a) is id
+--
+--     Equalizer has free choice of c up to isomorphism, we cannot prove eqa = id a
 
 equalizer-eq-k  : { a b : Obj A } {f g : Hom A a b } → (eq : A [ f ≈ g ] ) → ( eqa : Equalizer A {a} f g) → 
       A [ e eqa ≈ id1 A a ] →
@@ -96,6 +106,10 @@
                    id1 A a
              ∎
 
+--
+--
+--   An isomorphic element c' of c makes another equalizer
+--
 --           e eqa f g        f 
 --         c ----------> a ------->b
 --        |^ 
@@ -165,6 +179,8 @@
                    j
              ∎
 
+--  If we have equalizer f g, e fh gh is also equalizer if we have isomorphic pair (same as above)
+--
 --           e eqa f g        f
 --         c ----------> a ------->b
 --         ^ ---> d ---> 
@@ -252,6 +268,8 @@
                    k'
              ∎
 
+--  If we have equalizer f g, e hf hg is also equalizer if we have isomorphic pair 
+
 h+equalizer : {a b c d : Obj A } {f g : Hom A a b } ( eqa : Equalizer A {c} f g) (h : Hom A b d ) 
            → (h-1 : Hom A d b ) → A [ A [ h-1  o h ]  ≈ id1 A b ]
            → Equalizer A {c} (A [ h o f ])  (A [ h o g ] ) 
@@ -303,6 +321,8 @@
         A [ A [ e eqa o k' ] ≈ j ] → A [ k eqa j (fj=gj j eq) ≈ k' ]
       uniqueness1 = uniqueness eqa
       
+--  If we have equalizer f g, e (ef) (eg) is also an equalizer  and e = id c
+
 eefeg : {a b c d : Obj A } {f g : Hom A a b } ( eqa : Equalizer A {c} f g) 
            → Equalizer A {c} (A [ f o e eqa ])  (A [ g o e eqa ] ) 
 eefeg {a} {b} {c} {d} {f} {g} eqa =  record {
@@ -359,6 +379,14 @@
                    k'
              ∎
 
+--
+-- If we have two equalizers on c and c', there are isomorphic pair h, h'
+--
+--     h : c → c'  h' : c' → c
+--
+--     not yet done
+
+
 iso-rev  : { a b c : Obj A } {f g : Hom A a b } → (eq : A [ f ≈ g ] ) → ( eqa : Equalizer A {c} f g) →  Hom A a c
 iso-rev {a} {b} {c} {f} {g} eq eqa = k  eqa (id1 A a) (f1=g1 eq (id1 A a))
 
@@ -377,11 +405,6 @@
 --           e eqa f g        f
 --         c ----------> a ------->b
 --
-equalizer-iso-eq : { c c' a b : Obj A } {f g : Hom A a b } → ( eqa : Equalizer A {c} f g) → ( eqa' :  Equalizer A {c'} f g ) 
-      { h : Hom A a c } →  ( equalizer-iso-pair {a} {b} {c'} (eefeg eqa) )
-       → A [ A [ k eqa (e eqa' ) (fe=ge eqa') o k eqa' (e  eqa ) (fe=ge eqa)  ] ≈ id1 A c ]
-equalizer-iso-eq = ?
-
 equalizer-iso-eq' : { c c' a b : Obj A } {f g : Hom A a b } → ( eqa : Equalizer A {c} f g) → ( eqa' :  Equalizer A {c'} f g ) 
       { h : Hom A a c } →  A [ A [ h o e eqa ] ≈ id1 A c ] → A [ A [ k eqa (e eqa' ) (fe=ge eqa') o k eqa' (e  eqa ) (fe=ge eqa)  ] ≈ id1 A c ]
 equalizer-iso-eq' {c} {c'} {f} {g} eqa eqa' {h} rev =  let open ≈-Reasoning (A) in
@@ -403,14 +426,24 @@
                  id1 A c
              ∎
 
+equalizer-iso-eq : { c c' a b : Obj A } {f g : Hom A a b } → ( eqa : Equalizer A {c} f g) → ( eqa' :  Equalizer A {c'} f g ) 
+       → A [ A [ k eqa (e eqa' ) (fe=ge eqa') o k eqa' (e  eqa ) (fe=ge eqa)  ] ≈ id1 A c ]
+equalizer-iso-eq {c} {c'} {f} {g} eqa eqa' = equalizer-iso-eq' {c} {c'} {f} {g} eqa eqa' {{!!}}  {!!}
+
 -- ke = e' k'e' = e  → k k' = 1 , k' k = 1
 --     ke  = e'
 --     k'ke  = k'e' = e   kk' = 1
-
 --     x e = e -> x = id?
 
+----
+--
+-- An equalizer satisfies Burroni equations
+--
+--    b4 is not yet done 
+----
+
 lemma-equ1 : {a b c : Obj A} (f g : Hom A a b)  → 
-         ( {a b c : Obj A} → (f g : Hom A a b)  → Equalizer A {c} f g ) → EqEqualizer A {c} f g
+         ( {a b c : Obj A} → (f g : Hom A a b)  → Equalizer A {c} f g ) → Burroni A {c} f g
 lemma-equ1  {a} {b} {c} f g eqa = record {
       α = λ f g →  e (eqa f g ) ; -- Hom A c a
       γ = λ {a} {b} {c} {d} f g h → k (eqa f g ) {d} ( A [ h  o (e ( eqa (A [ f  o  h ] ) (A [ g o h ] ))) ] ) (lemma-equ4 {a} {b} {c} {d} f g h ) ;  -- Hom A c d
@@ -491,6 +524,7 @@
              ∎
 
 
+-- end