Mercurial > hg > Members > kono > Proof > category
changeset 171:d25b0948e006
unity of oppsite
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 23 Aug 2013 10:11:58 +0900 |
| parents | 721cf9d9f5e3 |
| children | c7fef385330f |
| files | cat-utility.agda universal-mapping.agda |
| diffstat | 2 files changed, 123 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- a/cat-utility.agda Wed Aug 21 18:33:03 2013 +0900 +++ b/cat-utility.agda Fri Aug 23 10:11:58 2013 +0900 @@ -34,6 +34,16 @@ _* : { a : Obj A}{ b : Obj B} → ( Hom A a (FObj U b) ) → Hom B (F a ) b isUniversalMapping : IsUniversalMapping A B U F η _* + record UnityOfOppsite {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') + ( U : Functor B A ) + ( F : Functor A B ) + : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where + field + right : {a : Obj A} { b : Obj B } → Hom A a ( FObj U b ) → Hom B (FObj F a) b + left : {a : Obj A} { b : Obj B } → Hom B (FObj F a) b → Hom A a ( FObj U b ) + right-injective : {a : Obj A} { b : Obj B } → {f : Hom A a (FObj U b) } → A [ left ( right f ) ≈ f ] + left-injective : {a : Obj A} { b : Obj B } → {f : Hom B (FObj F a) b } → B [ right ( left f ) ≈ f ] + open NTrans open import Category.Cat record IsAdjunction {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
--- a/universal-mapping.agda Wed Aug 21 18:33:03 2013 +0900 +++ b/universal-mapping.agda Fri Aug 23 10:11:58 2013 +0900 @@ -330,5 +330,118 @@ ∎ +------ +-- +-- Hom(F(-),-) = Hom(-,U(-)) +-- Unity of opposite +----- + +Adj2UO : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') + { 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 η ε ) → UnityOfOppsite A B U F +Adj2UO A B {U} {F} {η} {ε} adj = record { + right = right ; + left = left ; + right-injective = right-injective ; + left-injective = left-injective + } where + right : {a : Obj A} { b : Obj B } → Hom A a ( FObj U b ) → Hom B (FObj F a) b + right {a} {b} f = B [ TMap ε b o FMap F f ] + left : {a : Obj A} { b : Obj B } → Hom B (FObj F a) b → Hom A a ( FObj U b ) + left {a} {b} f = A [ FMap U f o (TMap η a) ] + right-injective : {a : Obj A} { b : Obj B } → {f : Hom A a (FObj U b) } → A [ left ( right f ) ≈ f ] + right-injective {a} {b} {f} = let open ≈-Reasoning (A) in + begin + FMap U (B [ TMap ε b o FMap F f ]) o (TMap η a) + ≈⟨ car ( distr U ) ⟩ + ( FMap U (TMap ε b) o FMap U (FMap F f )) o (TMap η a) + ≈↑⟨ assoc ⟩ + FMap U (TMap ε b) o ( FMap U (FMap F f ) o (TMap η a) ) + ≈⟨ cdr ( nat η) ⟩ + FMap U (TMap ε b) o ((TMap η (FObj U b)) o f ) + ≈⟨ assoc ⟩ + (FMap U (TMap ε b) o (TMap η (FObj U b))) o f + ≈⟨ car ( IsAdjunction.adjoint1 ( isAdjunction adj )) ⟩ + id1 A (FObj U b) o f + ≈⟨ idL ⟩ + f + ∎ + left-injective : {a : Obj A} { b : Obj B } → {f : Hom B (FObj F a) b } → B [ right ( left f ) ≈ f ] + left-injective {a} {b} {f} = let open ≈-Reasoning (B) in + begin + TMap ε b o FMap F ( A [ FMap U f o (TMap η a) ]) + ≈⟨ cdr ( distr F ) ⟩ + TMap ε b o ( FMap F (FMap U f) o FMap F (TMap η a)) + ≈⟨ assoc ⟩ + ( TMap ε b o FMap F (FMap U f)) o FMap F (TMap η a) + ≈↑⟨ car (nat ε) ⟩ + ( f o TMap ε ( FObj F a )) o ( FMap F ( TMap η a )) + ≈↑⟨ assoc ⟩ + f o ( TMap ε ( FObj F a ) o ( FMap F ( TMap η a ))) + ≈⟨ cdr ( IsAdjunction.adjoint2 ( isAdjunction adj )) ⟩ + f o id1 B (FObj F a) + ≈⟨ idR ⟩ + f + ∎ + +open UnityOfOppsite + +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-η {_} {_} {_} {_} {_} {_} {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 + begin + (FMap U (FMap F f)) o ( η a ) + ≈⟨⟩ + (FMap U (FMap F f)) o left uo ( id1 B (FObj F a) ) + ≈⟨ {!!} ⟩ + left uo ( id1 B (FObj F b)) o f + ≈⟨⟩ + (η b ) o 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 = {!!} + +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 B B ( F ○ U ) identityFunctor +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 ) +UO2Adj A B {U} {F} uo = record { + isAdjunction = record { + adjoint1 = adjoint1 ; + adjoint2 = adjoint2 + } + } where + adjoint1 : { b : Obj B } → + A [ A [ ( FMap U ( TMap (uo-ε uo) b )) o ( TMap (uo-η uo) ( FObj U b )) ] ≈ id1 A (FObj U b) ] + adjoint1 {b} = {!!} + adjoint2 : {a : Obj A} → + B [ B [ ( TMap (uo-ε uo) ( FObj F a )) o ( FMap F ( TMap (uo-η uo) a )) ] ≈ id1 B (FObj F a) ] + adjoint2 {a} = {!!} + + -- done!