Members/kono/Proof/category: pullback.agda comparison

comparison pullback.agda @ 282:c831abfa9bf4

limit on going...

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Mon, 23 Sep 2013 17:23:40 +0900
parents	dbd2044add2a
children	5492a0681f55

comparison

equal deleted inserted replaced

-:dbd2044add2a
+:c831abfa9bf4
 module pullback { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ') ( Γ : Functor I A ) where
 open import HomReasoning
 open import cat-utility
 --
 -- Pullback from equalizer and product
 --         f
 --     a -------> c
 --     ^          ^
 --  π1 |          |g
 --     |          |
 --    ab -------> b
 --     ^   π2
 --     |
 --     | e = equalizer (f π1) (g π1)
 --     |
 --     d <------------------ d'
 --         k (π1' × π2' )
 open Equalizer
 open Product
 open Pullback
 pullback-from :  (a b c ab d : Obj A)
 ( f : Hom A a c )    ( g : Hom A b c )
 ( π1 : Hom A ab a )  ( π2 : Hom A ab b ) ( e : Hom A d ab )
 ( eqa : {a b c : Obj A} → (f g : Hom A a b)  → {e : Hom A c a }  → Equalizer A e f g )
 ( prod : Product A a b ab π1 π2 ) → Pullback A a b c d f g
 ( A [  π1 o equalizer ( eqa ( A [ f  o π1 ] ) ( A [ g  o π2 ] ){e} )  ] )
 ( A [  π2 o equalizer ( eqa ( A [ f  o π1 ] ) ( A [ g  o π2 ] ){e} )  ] )
 pullback-from  a b c ab d f g π1 π2 e eqa prod =  record {
 commute = commute1 ;
 p = p1 ;
 π1p=π1 = λ {d} {π1'} {π2'} {eq} → π1p=π11  {d} {π1'} {π2'} {eq} ;
 π2p=π2 = λ {d} {π1'} {π2'} {eq} → π2p=π21  {d} {π1'} {π2'} {eq} ;
 uniqueness = uniqueness1
 } where
 commute1 :  A [ A [ f o A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] ] ≈ A [ g o A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] ] ]
 commute1 = let open ≈-Reasoning (A) in
 begin
 f o ( π1 o equalizer (eqa ( f o π1 ) ( g o π2 )) )
 ≈⟨ assoc ⟩
 ( f o  π1 ) o equalizer (eqa ( f o π1 ) ( g o π2 ))
 ≈⟨ fe=ge (eqa (A [ f o π1 ]) (A [ g o π2 ])) ⟩
 ( g o  π2 ) o equalizer (eqa ( f o π1 ) ( g o π2 ))
 ≈↑⟨ assoc ⟩
 g o ( π2 o equalizer (eqa ( f o π1 ) ( g o π2 )) )
 ∎
 lemma1 :  {d' : Obj A} {π1' : Hom A d' a} {π2' : Hom A d' b} → A [ A [ f o π1' ] ≈ A [ g o π2' ] ] →
 A [ A [ A [ f o π1 ] o (prod × π1') π2' ] ≈ A [ A [ g o π2 ] o (prod × π1') π2' ] ]
 lemma1  {d'} { π1' } { π2' } eq  = let open ≈-Reasoning (A) in
 begin
 ( f o π1 ) o (prod × π1') π2'
 ≈↑⟨ assoc ⟩
 f o ( π1  o (prod × π1') π2' )
 ≈⟨ cdr (π1fxg=f prod)  ⟩
 g o ( π2  o (prod × π1') π2'  )
 ≈⟨ assoc ⟩
 ( g o π2 ) o (prod × π1') π2'
 ∎
 p1 :  {d' : Obj A} {π1' : Hom A d' a} {π2' : Hom A d' b} → A [ A [ f o π1' ] ≈ A [ g o π2' ] ] → Hom A d' d
 p1 {d'} { π1' } { π2' } eq  =
 let open ≈-Reasoning (A) in k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod  π1'  π2' ) ( lemma1 eq )
 π1p=π11 :   {d₁ : Obj A} {π1' : Hom A d₁ a} {π2' : Hom A d₁ b} {eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ]} →
 A [ A [ A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]) {e} ) ] o p1 eq ] ≈ π1' ]
 π1p=π11 {d'} {π1'} {π2'} {eq} = let open ≈-Reasoning (A) in
 begin
 ( π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]) {e} ) ) o p1 eq
 ≈⟨⟩
 ( π1 o e) o  k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod  π1'  π2' ) (lemma1 eq)
 ≈↑⟨ assoc ⟩
 π1 o ( e o  k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod  π1'  π2' ) (lemma1 eq) )
 ≈⟨ cdr ( ek=h  ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} )) ⟩
 π1 o  (_×_ prod  π1'  π2' )
 ≈⟨ π1fxg=f prod ⟩
 π1'
 ∎
 π2p=π21 : {d₁ : Obj A} {π1' : Hom A d₁ a} {π2' : Hom A d₁ b} {eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ]} →
 A [ A [ A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]) {e} ) ] o p1 eq ] ≈ π2' ]
 π2p=π21  {d'} {π1'} {π2'} {eq} = let open ≈-Reasoning (A) in
 begin
 ( π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]) {e} ) ) o p1 eq
 ≈⟨⟩
 ( π2 o e) o  k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod  π1'  π2' ) (lemma1 eq)
 ≈↑⟨ assoc ⟩
 π2 o ( e o  k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod  π1'  π2' ) (lemma1 eq) )
 ≈⟨ cdr ( ek=h  ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} )) ⟩
 π2 o  (_×_ prod  π1'  π2' )
 ≈⟨ π2fxg=g prod ⟩
 π2'
 ∎
 uniqueness1 :  {d₁ : Obj A} (p' : Hom A d₁ d) {π1' : Hom A d₁ a} {π2' : Hom A d₁ b} {eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ]} →
 {eq1 : A [ A [ A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ] ≈ π1' ]} →
 equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) o p'
 ≈↑⟨ Product.uniqueness prod ⟩
 (prod × (  π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) o p') ) ( π2 o (equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) o p'))
 ≈⟨ ×-cong prod (assoc) (assoc) ⟩
 (prod × (A [ A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ]))
 (A [ A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ])
 ≈⟨ ×-cong prod eq1 eq2 ⟩
 ((prod × π1') π2')
 ∎ ) ⟩
 p'
 ∎
 }
 }
 open NTrans
 record Limit { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A )
 ( a0 : Obj A ) (  t0 : NTrans I A ( K I a0 ) Γ ) : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where
 field
 limit :  ( a : Obj A ) → ( t : NTrans I A ( K I a ) Γ ) → Hom A a a0
 t0f=t :  { a : Obj A } → { t : NTrans I A ( K 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 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 I a0 ) Γ
 T0 = t0
 --------------------------------
 --
 -- If we have two limits on c and c', there are isomorphic pair h, h'
 open Limit
 iso-l :  { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A )
 ( a0 a0' : Obj A ) (  t0 : NTrans I A ( K I a0 ) Γ ) (  t0' : NTrans I A ( K I a0' ) Γ )
 ( lim : Limit I Γ a0 t0 ) → ( lim' :  Limit I Γ a0' t0' )
 → Hom A a0 a0'
 iso-l  I Γ a0 a0' t0 t0' lim lim' = limit lim' a0 t0
 iso-r :  { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A )
 ( a0 a0' : Obj A ) (  t0 : NTrans I A ( K I a0 ) Γ ) (  t0' : NTrans I A ( K I a0' ) Γ )
 ( lim : Limit I Γ a0 t0 ) → ( lim' :  Limit I Γ a0' t0' )
 → Hom A a0' a0
 iso-r  I Γ a0 a0' t0 t0' lim lim' = limit lim a0' t0'
 iso-lr :  { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A )
 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
 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'
 ≈⟨ car ( t0f=t lim' ) ⟩
 TMap t0 i o limit lim a0' t0'
 ≈⟨ t0f=t lim ⟩
 TMap t0' i
 ∎) ) ⟩
 limit lim' a0' t0'
 ≈⟨ limit-uniqueness lim' idR ⟩
 id a0'
 ∎
 open import CatExponetial
 open Functor
 --------------------------------
 --
 KI : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) →  Functor A ( A ^ I )
 KI { c₁'} {c₂'} {ℓ'} I = record {
 FObj = λ a → K I a ;
 FMap = λ f → record { --  NTrans I A (K I a)  (K I b)
 TMap = λ a → f ;
 isNTrans = record {
 commute = λ {a b f₁} → commute1 {a} {b} {f₁} f
 }
 }  ;
 isFunctor = let  open ≈-Reasoning (A) in record {
 ≈-cong   = λ f=g {x} → f=g
 ; identity = refl-hom
 ; distr    = refl-hom
 }
 } where
 commute1 :  {a b : Obj I} {f₁ : Hom I a b} → {a' b' : Obj A} → (f : Hom A a' b' ) →
 A [ A [ FMap (K I b') f₁ o f ] ≈ A [ f o FMap (K I a') f₁ ] ]
 commute1 {a} {b} {f₁} {a'} {b'} f = let  open ≈-Reasoning (A) in begin
 FMap (K I b') f₁ o f
 ≈⟨ idL ⟩
 f
 ≈↑⟨ idR ⟩
 f o FMap (K I a') f₁
 ∎
 ---------
 --
 -- limit gives co universal mapping ( i.e. adjunction )
 --
 --     F = KI I : Functor A (A ^ I)
 --     U = λ b → A0 (lim b {a0 b} {t0 b}
 --     ε = λ b → T0 ( lim b {a0 b} {t0 b} )
 limit2couniv :
 ( lim : ( Γ : Functor I A ) → { a0 : Obj A } { t0 : NTrans I A ( K I a0 ) Γ } → Limit I Γ a0 t0 )
 → ( a0 : ( b : Functor I A ) → Obj A ) ( t0 :  ( b : Functor I A ) → NTrans I A ( K I (a0 b) ) b )
 →  coUniversalMapping A ( A ^ I ) (KI I) (λ b → A0 (lim b {a0 b} {t0 b} ) )  ( λ b → T0 ( lim b {a0 b} {t0 b} ) )
 limit2couniv lim a0 t0 = record {  -- F             U                            ε
 _*' = λ {b} {a} k → limit (lim b {a0 b} {t0 b} ) a k ; -- η
 iscoUniversalMapping = record {
 couniversalMapping = λ{ b a f} → couniversalMapping1 {b} {a} {f} ;
 couniquness = couniquness2
 }
 } where
 couniversalMapping1 :  {b : Obj (A ^ I)} {a : Obj A} {f : Hom (A ^ I) (FObj (KI I) a) b} →
 A ^ I [ A ^ I [ T0 (lim b {a0 b} {t0 b}) o FMap (KI I) (limit (lim b {a0 b} {t0 b}) a f) ] ≈ f ]
 couniversalMapping1 {b} {a} {f} {i} = let  open ≈-Reasoning (A) in begin
 TMap (T0 (lim b {a0 b} {t0 b})) i o TMap ( FMap (KI I) (limit (lim b {a0 b} {t0 b}) a f) ) i
 ≈⟨⟩
 TMap (t0 b) i o (limit (lim b) a f)
 ≈⟨ t0f=t (lim b) ⟩
 TMap f i  -- i comes from   ∀{i} → B [ TMap f i  ≈  TMap g i  ]
 ∎
 couniquness2 : {b : Obj (A ^ I)} {a : Obj A} {f : Hom (A ^ I) (FObj (KI I) a) b} {g : Hom A a (A0 (lim b {a0 b} {t0 b} ))} →
 ( ∀ { i : Obj I } → A [ A [ TMap (T0 (lim b {a0 b} {t0 b} )) i  o TMap ( FMap (KI I) g) i  ] ≈ TMap f i ] )
 → 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 ⟩
 g
 open import Category.Cat
 open coUniversalMapping
 univ2limit :
 ( U : Obj (A ^ I ) → Obj A )
 ( ε : ( b : Obj (A ^ I ) ) → NTrans I A (K I (U b)) b )
 ( univ :  coUniversalMapping A (A ^ I) (KI I) U (ε) ) →
 ( Γ : Functor I A ) →   Limit I Γ (U Γ) (ε Γ)
 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
 } where
 limit1 :  (a : Obj A) → NTrans I A (K I a) Γ → Hom A a (U Γ)
 limit1 a t = _*' univ {_} {a} t
 t0f=t1 :   {a : Obj A} {t : NTrans I A (K I a) Γ}  {i : Obj I} →
 A [ A [ TMap (ε Γ) i o limit1 a t ] ≈ TMap t i ]
 t0f=t1 {a} {t} {i} =  let  open ≈-Reasoning (A) in begin
 TMap (ε Γ) i o limit1 a t
 ≈⟨⟩
 TMap (ε Γ) i o _*' univ {Γ} {a} t
 ≈⟨ coIsUniversalMapping.couniversalMapping ( iscoUniversalMapping univ) {Γ} {a} {t} ⟩
 TMap t i
 ∎
 limit-uniqueness1 : { a : Obj A } →  { t : NTrans I A ( K I a ) Γ } → { f : Hom A a (U Γ)}
 → ( ∀ { i : Obj I } → A [ A [ TMap  (ε Γ) i o  f ]  ≈ TMap t i ] ) → A [ limit1 a t ≈ f ]
 limit-uniqueness1 {a} {t} {f} εf=t = let  open ≈-Reasoning (A) in begin
 _*' univ t
 ≈⟨  ( coIsUniversalMapping.couniquness ( iscoUniversalMapping univ) ) εf=t  ⟩
 f
 field
 product : {q : Obj A}  → ( qi : (i : I) → Hom A q (ai i) ) → Hom A q p
 pif=q :   {q : Obj A}  → ( qi : (i : I) → Hom A q (ai i) ) → ∀ { i : I } → A [ A [ ( pi i )  o ( product qi ) ] ≈  (qi i) ]
 ip-uniqueness :  {q : Obj A} { h : Hom A q p } → A [ product ( λ (i : I) →  A [ (pi i)  o h ] )  ≈  h ]
 ip-cong : {q : Obj A}   → ( qi : (i : I) → Hom A q (ai i) ) → ( qi' : (i : I) → Hom A q (ai i) )
 → ( ∀ (i : I ) →  A [ qi i ≈ qi' i ] ) → A [ product qi ≈ product qi' ]
 open IProduct
-limit-equalizer :
+--
+-- limit from equalizer and product
+--
+--
+--       ai
+--      ^ ^
+--      | | pi
+--      | |
+--      | p
+--      | ^
+--      | |
+--      | | e = equalizer (f pi) (g pi')
+--      | |
+--       lim <------------------ d'
+--         k ( product pi )
+open Equalizer
+limit-equalizer :
 ( prod : (p : Obj A) ( ai : Obj I → Obj A )  ( pi : (i : Obj I) → Hom A p ( ai i ) )
 →  IProduct {c₁'} A (Obj I) p ai pi )
 ( eqa : {a b c : Obj A} → (e : Hom A c a )  → (f g : Hom A a b)  → Equalizer A e f g )
 ( Γ : Functor I A ) →
-( lim : Obj A )
+( lim p : Obj A ) ( e : Hom  A lim p )
-( proj : (i : Obj I ) → Hom A lim (FObj Γ i) ) →
+( proj : (i : Obj I ) → Hom A p (FObj Γ i) ) →
 NTrans I A (K I lim) Γ
-limit-equalizer prod eqa Γ lim proj = record {
+limit-equalizer prod eqa Γ lim p e proj = record {
 TMap = tmap ;
 isNTrans = record {
-commute = {!!}
+commute = commute1
 }
 } where
 tmap : (i : Obj I) → Hom A (FObj (K I lim) i) (FObj Γ i)
-tmap i = A [ ( proj i )  o equalizer ( eqa (id1 A lim) (A [ FMap Γ (id1 I i) o proj i ] ) (A [ {!!} o {!!} ] )) ]
+tmap i = A [ ( proj i )  o e ]
+commute1 :  {a b : Obj I} {f : Hom I a b} →
-limit-from :
+A [ A [ FMap Γ f o tmap a ] ≈ A [ tmap b o FMap (K I lim) f ] ]
+commute1 {i} {j} {f} = let  open ≈-Reasoning (A) in begin
+FMap Γ f o tmap i
+≈⟨⟩
+FMap Γ f o ( proj i o e )
+≈⟨ assoc ⟩
+( FMap Γ f o  proj i ) o e
+≈⟨ {!!} ⟩
+proj j o e
+≈↑⟨ idR ⟩
+(proj j o e ) o id1 A lim
+≈⟨⟩
+tmap j o FMap (K I lim) f
+∎
+limit-from :
 ( prod : (p : Obj A) ( ai : Obj I → Obj A )  ( pi : (i : Obj I) → Hom A p ( ai i ) )
 →  IProduct {c₁'} A (Obj I) p ai pi )
 ( eqa : {a b c : Obj A} → (e : Hom A c a )  → (f g : Hom A a b)  → Equalizer A e f g )
 ( Γ : Functor I A ) →
-( lim : Obj A )
+( lim p : Obj A ) ( e : Hom  A lim p )
-( proj : (i : Obj I ) → Hom A lim (FObj Γ i) ) →
+( proj : (i : Obj I ) → Hom A p (FObj Γ i) ) →
-Limit I Γ lim ( limit-equalizer prod eqa Γ lim proj )
+Limit I Γ lim ( limit-equalizer prod eqa Γ lim p e proj )
-limit-from prod eqa lim Γ proj = {!!}
+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
+}  where
+limit1 :  (a : Obj A) → NTrans I A (K I a) Γ → Hom A a lim
+limit1 a t = k (eqa e {!!} {!!} ) (product ( prod p (FObj Γ)  proj ) (TMap t) ) {!!}
+t0f=t1 :  {a : Obj A} {t : NTrans I A (K I a) Γ} {i : Obj I} →
+A [ A [ TMap (limit-equalizer prod eqa Γ lim p e proj) i o limit1 a t ] ≈ TMap t i ]
+t0f=t1 = {!!}
+limit-uniqueness1 :  {a : Obj A} {t : NTrans I A (K I a) Γ} {f : Hom A a lim} → ({i : Obj I} →
+A [ A [ TMap (limit-equalizer prod eqa Γ lim p e proj) i o f ] ≈ TMap t i ]) →
+A [ limit1 a t ≈ f ]
+limit-uniqueness1 = {!!}

Mercurial > hg > Members > kono > Proof > category

comparison pullback.agda @ 282:c831abfa9bf4