Mercurial > hg > Members > kono > Proof > category
diff pullback.agda @ 291:c8e26650ddf9
limit preserving ...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 25 Sep 2013 18:07:58 +0900 |
| parents | 1f897357ec6c |
| children | a84fab7cf46a |
line wrap: on
line diff
--- a/pullback.agda Wed Sep 25 13:59:56 2013 +0900 +++ b/pullback.agda Wed Sep 25 18:07:58 2013 +0900 @@ -134,8 +134,9 @@ -- Constancy Functor -K : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) → ( a : Obj A ) → Functor I A -K I a = record { +K : { c₁' c₂' ℓ' : Level} (A : Category c₁' c₂' ℓ') { c₁'' c₂'' ℓ'' : Level} ( I : Category c₁'' c₂'' ℓ'' ) + → ( a : Obj A ) → Functor I A +K A I a = record { FObj = λ i → a ; FMap = λ f → id1 A a ; isFunctor = let open ≈-Reasoning (A) in record { @@ -147,17 +148,17 @@ 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 +record Limit { c₁' c₂' ℓ' : Level} { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A ) + ( a0 : Obj A ) ( t0 : NTrans I A ( K A 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 } → + 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 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 I a0 ) Γ + T0 : NTrans I A ( K A I a0 ) Γ T0 = t0 -------------------------------- @@ -167,21 +168,21 @@ 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' ) + ( a0 a0' : Obj A ) ( t0 : NTrans I A ( K A I a0 ) Γ ) ( t0' : NTrans I A ( K A I a0' ) Γ ) + ( lim : Limit A I Γ a0 t0 ) → ( lim' : Limit A 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' ) + ( a0 a0' : Obj A ) ( t0 : NTrans I A ( K A I a0 ) Γ ) ( t0' : NTrans I A ( K A I a0' ) Γ ) + ( lim : Limit A I Γ a0 t0 ) → ( lim' : Limit A 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 ) - ( 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' ) → ∀{ i : Obj I } → + ( a0 a0' : Obj A ) ( t0 : NTrans I A ( K A I a0 ) Γ ) ( t0' : NTrans I A ( K A I a0' ) Γ ) + ( lim : Limit A I Γ a0 t0 ) → ( lim' : Limit A I Γ a0' t0' ) → ∀{ i : Obj I } → 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' @@ -210,8 +211,8 @@ 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) + FObj = λ a → K A I a ; + FMap = λ f → record { -- NTrans I A (K A I a) (K A I b) TMap = λ a → f ; isNTrans = record { commute = λ {a b f₁} → commute1 {a} {b} {f₁} f @@ -224,13 +225,13 @@ } } 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₁ ] ] + A [ A [ FMap (K A I b') f₁ o f ] ≈ A [ f o FMap (K A I a') f₁ ] ] commute1 {a} {b} {f₁} {a'} {b'} f = let open ≈-Reasoning (A) in begin - FMap (K I b') f₁ o f + FMap (K A I b') f₁ o f ≈⟨ idL ⟩ f ≈↑⟨ idR ⟩ - f o FMap (K I a') f₁ + f o FMap (K A I a') f₁ ∎ @@ -243,8 +244,8 @@ -- ε = λ 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 ) + ( lim : ( Γ : Functor I A ) → { a0 : Obj A } { t0 : NTrans I A ( K A I a0 ) Γ } → Limit A I Γ a0 t0 ) + → ( a0 : ( b : Functor I A ) → Obj A ) ( t0 : ( b : Functor I A ) → NTrans I A ( K A 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 ; -- η @@ -278,17 +279,17 @@ univ2limit : ( U : Obj (A ^ I ) → Obj A ) - ( ε : ( b : Obj (A ^ I ) ) → NTrans I A (K I (U b)) b ) + ( ε : ( b : Obj (A ^ I ) ) → NTrans I A (K A I (U b)) b ) ( univ : coUniversalMapping A (A ^ I) (KI I) U (ε) ) → - ( Γ : Functor I A ) → Limit I Γ (U Γ) (ε Γ) + ( Γ : Functor I A ) → Limit A 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 : Obj A) → NTrans I A (K A 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} → + t0f=t1 : {a : Obj A} {t : NTrans I A (K A 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 @@ -297,7 +298,7 @@ ≈⟨ 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 Γ)} + limit-uniqueness1 : { a : Obj A } → { t : NTrans I A ( K A 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 @@ -346,22 +347,38 @@ -- -- +-- pi-ε -- : ( 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 ) +-- ( lim p : Obj A ) ( e : Hom A lim p ) +-- ( proj : (i : Obj I ) → Hom A p (FObj Γ i) ) → +-- { i : Obj I } → { q : ( i : Obj I ) → Hom A p (FObj Γ i) } → A [ proj i ≈ q i ] +-- pi-ε prod lim p e proj {i} {q} = let open ≈-Reasoning (A) in begin +-- proj i +-- ≈↑⟨ idR ⟩ +-- proj i o id1 A p +-- ≈⟨ cdr {!!} ⟩ +-- proj i o product (prod p (FObj Γ) proj) q +-- ≈⟨ pif=q (prod p (FObj Γ) proj) q ⟩ +-- q i +-- ∎ + + limit-ε : ( 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 ) ( lim p : Obj A ) ( e : Hom A lim p ) ( proj : (i : Obj I ) → Hom A p (FObj Γ i) ) → - NTrans I A (K I lim) Γ + NTrans I A (K A I lim) Γ limit-ε prod lim p e proj = record { TMap = tmap ; isNTrans = record { commute = commute1 } } where - tmap : (i : Obj I) → Hom A (FObj (K I lim) i) (FObj Γ i) + tmap : (i : Obj I) → Hom A (FObj (K A I lim) i) (FObj Γ i) tmap i = A [ proj i o e ] commute1 : {i j : Obj I} {f : Hom I i j} → - A [ A [ FMap Γ f o tmap i ] ≈ A [ tmap j o FMap (K I lim) f ] ] + A [ A [ FMap Γ f o tmap i ] ≈ A [ tmap j o FMap (K A I lim) f ] ] commute1 {i} {j} {f} = let open ≈-Reasoning (A) in begin FMap Γ f o tmap i ≈⟨⟩ @@ -373,7 +390,7 @@ ≈↑⟨ idR ⟩ (proj j o e ) o id1 A lim ≈⟨⟩ - tmap j o FMap (K I lim) f + tmap j o FMap (K A I lim) f ∎ limit-from : @@ -383,15 +400,15 @@ ( lim p : Obj A ) -- limit to be made ( e : Hom A lim p ) -- existing of equalizer ( proj : (i : Obj I ) → Hom A p (FObj Γ i) ) -- existing of product ( projection actually ) - → Limit I Γ lim ( limit-ε prod lim p e proj ) + → Limit A I Γ lim ( limit-ε prod lim p e 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 : 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 - t0f=t1 : {a : Obj A} {t : NTrans I A (K I a) Γ} {i : Obj I} → + t0f=t1 : {a : Obj A} {t : NTrans I A (K A I a) Γ} {i : Obj I} → A [ A [ TMap (limit-ε prod lim p e proj ) i o limit1 a t ] ≈ TMap t i ] t0f=t1 {a} {t} {i} = let open ≈-Reasoning (A) in begin TMap (limit-ε prod lim p e proj ) i o limit1 a t @@ -404,7 +421,7 @@ ≈⟨ pif=q (prod p (FObj Γ) proj) (TMap t) ⟩ TMap t i ∎ - limit-uniqueness1 : {a : Obj A} {t : NTrans I A (K I a) Γ} {f : Hom A a lim} + limit-uniqueness1 : {a : Obj A} {t : NTrans I A (K A I a) Γ} {f : Hom A a lim} → ({i : Obj I} → A [ A [ TMap (limit-ε prod lim p e proj ) i o f ] ≈ TMap t i ]) → A [ limit1 a t ≈ f ] limit-uniqueness1 {a} {t} {f} lim=t = let open ≈-Reasoning (A) in begin @@ -427,3 +444,47 @@ f ∎ +---- +-- +-- Adjoint functor preserves limits +-- +-- + +open import Category.Cat + +ta1 : { c₁' c₂' ℓ' : Level} (B : Category c₁' c₂' ℓ') ( Γ : Functor I B ) + ( lim : Obj B ) ( tb : NTrans I B ( K B I lim ) Γ ) → ( limit : Limit B I Γ lim tb ) → + ( U : Functor B A) → NTrans I A ( K A I (FObj U lim) ) (U ○ Γ) +ta1 B Γ lim tb limit U = record { + TMap = TMap (Functor*Nat I A U tb) ; + isNTrans = record { commute = λ {a} {b} {f} → let open ≈-Reasoning (A) in begin + FMap (U ○ Γ) f o TMap (Functor*Nat I A U tb) a + ≈⟨ nat ( Functor*Nat I A U tb ) ⟩ + TMap (Functor*Nat I A U tb) b o FMap (U ○ K B I lim) f + ≈⟨ cdr (IsFunctor.identity (isFunctor U) ) ⟩ + TMap (Functor*Nat I A U tb) b o FMap (K A I (FObj U lim)) f + ∎ + } } + +adjoint-preseve-limit : + { c₁' c₂' ℓ' : Level} (B : Category c₁' c₂' ℓ') ( Γ : Functor I B ) + ( lim : Obj B ) ( tb : NTrans I B ( K B I lim ) Γ ) → ( limit : Limit B I Γ lim tb ) → + { U : Functor B A } { F : Functor A B } + { η : NTrans A A identityFunctor ( U ○ F ) } + { ε : NTrans B B ( F ○ U ) identityFunctor } → + ( adj : Adjunction A B U F η ε ) → Limit A I (U ○ Γ) (FObj U lim) (ta1 B Γ lim tb limit U ) +adjoint-preseve-limit B Γ lim tb limit {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 + } where + ta = ta1 B Γ lim tb limit U + limit1 : (a : Obj A) → NTrans I A (K A I a) (U ○ Γ) → Hom A a (FObj U lim) + limit1 a t = let open ≈-Reasoning (A) in ? + t0f=t1 : {a : Obj A} {t : NTrans I A (K A I a) (U ○ Γ)} {i : Obj I} → + A [ A [ TMap ta i o limit1 a t ] ≈ TMap t i ] + t0f=t1 {a} {t} {i} = let open ≈-Reasoning (A) in ? + limit-uniqueness1 : {a : Obj A} {t : NTrans I A (K A I a) (U ○ Γ)} {f : Hom A a (FObj U lim)} + → ({i : Obj I} → A [ A [ TMap ta i o f ] ≈ TMap t i ]) → + A [ limit1 a t ≈ f ] + limit-uniqueness1 {a} {t} {f} lim=t = let open ≈-Reasoning (A) in ?