Mercurial > hg > Members > kono > Proof > category
changeset 174:1c4788483d46
add more axiom on unity of oppsite
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 24 Aug 2013 17:16:07 +0900 |
| parents | bf7f06580f5e |
| children | 795be747d7a9 |
| files | cat-utility.agda category.pdf universal-mapping.agda |
| diffstat | 3 files changed, 59 insertions(+), 27 deletions(-) [+] |
line wrap: on
line diff
--- a/cat-utility.agda Fri Aug 23 17:30:04 2013 +0900 +++ b/cat-utility.agda Sat Aug 24 17:16:07 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 η _* +-- naturality of left +-- f' = k* f k*: Hom A F(a) k, +-- left left +-- f : Hom A F(a) b --------> f* : Hom B a U(b) f : Hom A F(a')b --------> f* : Hom B a' U(b) +-- | | | | +-- |k* |U(k*) |F(h*) |h* +-- v v v v +-- f': Hom A F(a) b'--------> f* : Hom B a U(b') f': Hom A F(a) b --------> f* : Hom B a U(b) +-- left + record UnityOfOppsite {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') ( U : Functor B A ) ( F : Functor A B ) @@ -43,6 +53,40 @@ 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 ] + left-commute1 : {a : Obj A} {b b' : Obj B } -> + ( f : Hom B (FObj F a) b ) -> ( k : Hom B b b' ) -> + A [ left ( B [ k o f ] ) ≈ A [ FMap U k o left f ] ] + left-commute2 : {a a' : Obj A} {b : Obj B } -> + ( f : Hom B (FObj F a) b ) -> ( h : Hom A a' a ) -> + A [ left ( B [ f o FMap F h ] ) ≈ A [ left f o h ] ] + r-cong : {a : Obj A} { b : Obj B } → { f g : Hom A a ( FObj U b ) } → A [ f ≈ g ] → B [ right f ≈ right g ] + l-cong : {a : Obj A} { b : Obj B } → { f g : Hom B (FObj F a) b } → B [ f ≈ g ] → A [ left f ≈ left g ] + right-commute1 : {a : Obj A} {b b' : Obj B } -> + ( g : Hom A a (FObj U b)) -> ( k : Hom B b b' ) -> + B [ B [ k o right g ] ≈ right ( A [ FMap U k o g ] ) ] + right-commute1 g k = let open ≈-Reasoning (B) in + begin + k o right g + ≈⟨ sym left-injective ⟩ + right ( left ( k o right g ) ) + ≈⟨ r-cong ( left-commute1 (right g) k ) ⟩ + right ( A [ FMap U k o left ( right g ) ] ) + ≈⟨ r-cong (lemma-1 g k) ⟩ + right ( A [ FMap U k o g ] ) + ∎ where + lemma-1 : {a : Obj A} {b b' : Obj B } -> + ( g : Hom A a (FObj U b)) -> ( k : Hom B b b' ) -> + A [ A [ FMap U k o left ( right g ) ] ≈ A [ FMap U k o g ] ] + lemma-1 = let open ≈-Reasoning (A) in + begin + FMap U k o left ( right g ) + ≈⟨ cdr ( right-injective) ⟩ + FMap U k o g + ∎ + right-commute2 : {a a' : Obj A} {b : Obj B } -> + ( g : Hom A a (FObj U b) ) -> ( h : Hom A a' a ) -> + B [ B [ right g o FMap F h ] ≈ right ( A [ g o h ] ) ] + right-commute2 = {!!} open NTrans open import Category.Cat
--- a/universal-mapping.agda Fri Aug 23 17:30:04 2013 +0900 +++ b/universal-mapping.agda Sat Aug 24 17:16:07 2013 +0900 @@ -390,44 +390,30 @@ open UnityOfOppsite -- f : a -----------> U(b) --- FMap U ( right uo f ) : UF(a) --> U(b) --- FMap U ( right uo f ) o η : a -> UF(a) --> U(b) --- right (FMap U ( right uo f ) o η) - --- right f : F(a) --------> b --- ε o (FMap F f) : F(a)--FU(b)--> b --- left (ε o (FMap F f)) : a -----------> U(b) +-- 1_F(a) :F(a) ---------> F(a) +-- ε(b) = right uo (1_F(a)) :UF(b)---------> a +-- η(a) = left uo (1_U(a)) : a -----------> FU(a) uo-η-map : {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) → (a : Obj A ) → Hom A a (FObj U ( FObj F ( a ) )) -uo-η-map {_} {_} {_} {_} {_} {_} {A} {B} {U} {F} uo a = {!!} -- ? left uo ( id1 B (FObj F a) ) + ( uo : UnityOfOppsite A B U F) → (a : Obj A ) → Hom A a (FObj U ( FObj F a )) +uo-η-map {_} {_} {_} {_} {_} {_} {A} {B} {U} {F} uo a = left uo ( id1 B (FObj F a) ) + +uo-ε-map : {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) → (b : Obj B ) → Hom B (FObj F ( FObj U ( b ) )) b +uo-ε-map {_} {_} {_} {_} {_} {_} {A} {B} {U} {F} uo b = right uo ( id1 A (FObj U b) ) uo-solution : {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) → {a : Obj A} {b : Obj B } -> ( f : Hom A a (FObj U b )) -> Hom B (FObj F a) b -uo-solution A B U F uo {a} {b} f = {!!} -- B [ right uo (id1 A (FObj U b)) o FMap F f ] - -- right uo f - -lemma-u2 : {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) → - {a : Obj A} {b : Obj B } -> ( f : Hom A a (FObj U b )) -> - B [ B [ right uo (id1 A (FObj U b)) o FMap F f ] ≈ right uo f ] -lemma-u2 = {!!} - -lemma-u1 : {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) → - {a : Obj A} {b : Obj B } -> ( f : Hom A a (FObj U b ) ) -> - A [ A [ FMap U (right uo f) o left uo (id1 B (FObj F a)) ] ≈ f ] -lemma-u1 = {!!} +uo-solution A B U F uo {a} {b} f = -- B [ right uo (id1 A (FObj U b)) o FMap F f ] + right uo f -- F(ε(b)) o η(F(b)) -- F( right uo (id1 A (FObj U b)) ) o left uo (id1 B (FObj F a)) ] == 1 @@ -448,6 +434,8 @@ universalMapping {a} {b} {f} = let open ≈-Reasoning (A) in begin FMap U ( uo-solution A B U F uo f) o ( uo-η-map uo ) a + ≈⟨⟩ + FMap U ( right uo f) o left uo ( id1 B (FObj F a) ) ≈⟨ {!!} ⟩ f ∎