Mercurial > hg > Members > kono > Proof > category
diff universal-mapping.agda @ 688:a5f2ca67e7c5
fix monad/adjunction definition
couniversal to limit does not work
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 11 Nov 2017 21:34:58 +0900 |
| parents | d6a6dd305da2 |
| children | fb9fc9652c04 |
line wrap: on
line diff
--- a/universal-mapping.agda Wed Nov 08 19:57:43 2017 +0900 +++ b/universal-mapping.agda Sat Nov 11 21:34:58 2017 +0900 @@ -16,22 +16,26 @@ -- -- -open Adjunction -open UniversalMapping - Adj2UM : {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 } → - Adjunction A B U F η ε → UniversalMapping A B U (FObj F) (TMap η) -Adj2UM A B {U} {F} {η} {ε} adj = record { + → Adjunction A B → UniversalMapping A B +Adj2UM A B adj = record { + U = U ; + F = FObj F ; + η = TMap η ; _* = solution ; isUniversalMapping = record { universalMapping = universalMapping; uniquness = uniqueness } } where + U : Functor B A + U = Adjunction.U adj + F : Functor A B + F = Adjunction.F adj + η : NTrans A A identityFunctor ( U ○ F ) + η = Adjunction.η adj + ε : NTrans B B ( F ○ U ) identityFunctor + ε = Adjunction.ε adj solution : { a : Obj A} { b : Obj B} → ( f : Hom A a (FObj U b) ) → Hom B (FObj F a ) b solution {_} {b} f = B [ TMap ε b o FMap F f ] universalMapping : {a' : Obj A} { b' : Obj B } → { f : Hom A a' (FObj U b') } → @@ -50,7 +54,7 @@ (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)) ⟩ + ≈⟨ car ( IsAdjunction.adjoint1 ( Adjunction.isAdjunction adj)) ⟩ id (FObj U b) o f ≈⟨ idL ⟩ f @@ -76,7 +80,7 @@ ( g o TMap ε ( FObj F a) ) o FMap F ( TMap η a ) ≈⟨ sym assoc ⟩ g o ( TMap ε ( FObj F a) o FMap F ( TMap η a ) ) - ≈⟨ cdr ( IsAdjunction.adjoint2 ( isAdjunction adj )) ⟩ + ≈⟨ cdr ( IsAdjunction.adjoint2 ( Adjunction.isAdjunction adj )) ⟩ g o id (FObj F a) ≈⟨ idR ⟩ g @@ -94,15 +98,20 @@ -- FunctorF : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') - { U : Functor B A } - { F : Obj A → Obj B } - { η : (a : Obj A) → Hom A a ( FObj U (F a) ) } → - UniversalMapping A B U F η → Functor A B -FunctorF A B {U} {F} {η} um = record { + → UniversalMapping A B → Functor A B +FunctorF A B um = record { FObj = F; FMap = myFMap ; isFunctor = myIsFunctor } where + U : Functor B A + U = UniversalMapping.U um + F : Obj A → Obj B + F = UniversalMapping.F um + η : (a : Obj A) → Hom A a ( FObj U (F a) ) + η = UniversalMapping.η um + _* : (UniversalMapping A B) → { a : Obj A} { b : Obj B} → ( Hom A a (FObj U b) ) → Hom B (F a ) b + _* _ = UniversalMapping._* um myFMap : {a b : Obj A} → Hom A a b → Hom B (F a) (F b) myFMap f = (_* um) (A [ η (Category.cod A f ) o f ]) lemma-id1 : {a : Obj A} → A [ A [ FMap U (id1 B (F a)) o η a ] ≈ (A [ (η a) o (id1 A a) ]) ] @@ -117,19 +126,19 @@ η a o id a ∎ lemma-id : {a : Obj A} → B [ ( (_* um) (A [ (η a) o (id1 A a)] )) ≈ (id1 B (F a)) ] - lemma-id {a} = ( IsUniversalMapping.uniquness ( isUniversalMapping um ) ) lemma-id1 + lemma-id {a} = ( IsUniversalMapping.uniquness ( UniversalMapping.isUniversalMapping um ) ) lemma-id1 lemma-cong2 : (a b : Obj A) (f g : Hom A a b) → A [ f ≈ g ] → A [ A [ FMap U ((_* um) (A [ η b o g ]) ) o η a ] ≈ A [ η b o f ] ] lemma-cong2 a b f g eq = let open ≈-Reasoning (A) in begin ( FMap U ((_* um) (A [ η b o g ]) )) o η a - ≈⟨ ( IsUniversalMapping.universalMapping ( isUniversalMapping um )) ⟩ + ≈⟨ ( IsUniversalMapping.universalMapping ( UniversalMapping.isUniversalMapping um )) ⟩ η b o g ≈⟨ ( IsCategory.o-resp-≈ ( Category.isCategory A ) (sym eq) (refl-hom) ) ⟩ η b o f ∎ lemma-cong1 : (a b : Obj A) (f g : Hom A a b) → A [ f ≈ g ] → B [ (_* um) (A [ η b o f ] ) ≈ (_* um) (A [ η b o g ]) ] - lemma-cong1 a b f g eq = ( IsUniversalMapping.uniquness ( isUniversalMapping um ) ) ( lemma-cong2 a b f g eq ) + lemma-cong1 a b f g eq = ( IsUniversalMapping.uniquness ( UniversalMapping.isUniversalMapping um ) ) ( lemma-cong2 a b f g eq ) lemma-cong : {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → B [ myFMap f ≈ myFMap g ] lemma-cong {a} {b} {f} {g} eq = lemma-cong1 a b f g eq lemma-distr2 : (a b c : Obj A) (f : Hom A a b) (g : Hom A b c) → @@ -141,18 +150,18 @@ (( FMap U ((_* um) (A [ η c o g ])) o ( FMap U ((_* um)( A [ η b o f ])))) ) o η a ≈⟨ sym assoc ⟩ ( FMap U ((_* um) (A [ η c o g ])) o (( FMap U ((_* um)( A [ η b o f ])))) o η a ) - ≈⟨ cdr ( IsUniversalMapping.universalMapping ( isUniversalMapping um )) ⟩ + ≈⟨ cdr ( IsUniversalMapping.universalMapping ( UniversalMapping.isUniversalMapping um )) ⟩ ( FMap U ((_* um) (A [ η c o g ])) o ( η b o f) ) ≈⟨ assoc ⟩ ( FMap U ((_* um) (A [ η c o g ])) o η b) o f - ≈⟨ car ( IsUniversalMapping.universalMapping ( isUniversalMapping um )) ⟩ + ≈⟨ car ( IsUniversalMapping.universalMapping ( UniversalMapping.isUniversalMapping um )) ⟩ ( η c o g ) o f ≈⟨ sym assoc ⟩ η c o ( g o f ) ∎ lemma-distr1 : (a b c : Obj A) (f : Hom A a b) (g : Hom A b c) → B [ (_* um) (A [ η c o A [ g o f ] ]) ≈ (B [(_* um) (A [ η c o g ]) o (_* um)( A [ η b o f ]) ] )] - lemma-distr1 a b c f g = ( IsUniversalMapping.uniquness ( isUniversalMapping um )) (lemma-distr2 a b c f g ) + lemma-distr1 a b c f g = ( IsUniversalMapping.uniquness ( UniversalMapping.isUniversalMapping um )) (lemma-distr2 a b c f g ) lemma-distr : {a b c : Obj A} {f : Hom A a b} {g : Hom A b c} → B [ myFMap (A [ g o f ]) ≈ (B [ myFMap g o myFMap f ] )] lemma-distr {a} {b} {c} {f} {g} = lemma-distr1 a b c f g myIsFunctor : IsFunctor A B F myFMap @@ -166,16 +175,21 @@ -- naturality of η -- nat-η : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') - { U : Functor B A } - { F : Obj A → Obj B } - { η : (a : Obj A) → Hom A a ( FObj U (F a) ) } → - (um : UniversalMapping A B U F η ) → - NTrans A A identityFunctor ( U ○ FunctorF A B um ) -nat-η A B {U} {F} {η} um = record { + → (um : UniversalMapping A B ) → + NTrans A A identityFunctor ( UniversalMapping.U um ○ FunctorF A B um ) +nat-η A B um = record { TMap = η ; isNTrans = myIsNTrans } where + U : Functor B A + U = UniversalMapping.U um + F : Obj A → Obj B + F = UniversalMapping.F um + η : (a : Obj A) → Hom A a ( FObj U (F a) ) + η = UniversalMapping.η um F' : Functor A B F' = FunctorF A B um + _* : (UniversalMapping A B) → { a : Obj A} { b : Obj B} → ( Hom A a (FObj U b) ) → Hom B (F a ) b + _* _ = UniversalMapping._* um 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 @@ -183,23 +197,28 @@ (FMap U (FMap F' f)) o ( η a ) ≈⟨⟩ (FMap U ((_* um) (A [ η b o f ]))) o ( η a ) - ≈⟨ (IsUniversalMapping.universalMapping ( isUniversalMapping um )) ⟩ + ≈⟨ (IsUniversalMapping.universalMapping ( UniversalMapping.isUniversalMapping um )) ⟩ (η b ) o f ∎ myIsNTrans : IsNTrans A A identityFunctor ( U ○ F' ) η myIsNTrans = record { commute = commute } nat-ε : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') - { U : Functor B A } - { F : Obj A → Obj B } - { η : (a : Obj A) → Hom A a ( FObj U (F a) ) } → - (um : UniversalMapping A B U F η ) → - NTrans B B ( FunctorF A B um ○ U) identityFunctor -nat-ε A B {U} {F} {η} um = record { + → (um : UniversalMapping A B ) → + NTrans B B ( FunctorF A B um ○ UniversalMapping.U um ) identityFunctor +nat-ε A B um = record { TMap = ε ; isNTrans = myIsNTrans } where + U : Functor B A + U = UniversalMapping.U um + F : Obj A → Obj B + F = UniversalMapping.F um + η : (a : Obj A) → Hom A a ( FObj U (F a) ) + η = UniversalMapping.η um F' : Functor A B F' = FunctorF A B um + _* : (UniversalMapping A B) → { a : Obj A} { b : Obj B} → ( Hom A a (FObj U b) ) → Hom B (F a ) b + _* _ = UniversalMapping._* um ε : ( b : Obj B ) → Hom B ( FObj F' ( FObj U b) ) b ε b = (_* um) ( id1 A (FObj U b)) lemma-nat1 : (a b : Obj B) (f : Hom B a b ) → @@ -212,11 +231,11 @@ ( FMap U ((um *) (id1 A (FObj U b))) o FMap U ((um *) ( η (FObj U b) o FMap U f )) ) o η (FObj U a) ≈⟨ sym assoc ⟩ FMap U ((um *) (id1 A (FObj U b))) o ( FMap U ((um *) ( η (FObj U b) o FMap U f ))) o η (FObj U a) - ≈⟨ cdr ((IsUniversalMapping.universalMapping ( isUniversalMapping um )) ) ⟩ + ≈⟨ cdr ((IsUniversalMapping.universalMapping ( UniversalMapping.isUniversalMapping um )) ) ⟩ FMap U ((um *) (id1 A (FObj U b))) o ( η (FObj U b) o FMap U f ) ≈⟨ assoc ⟩ (FMap U ((um *) (id1 A (FObj U b))) o η (FObj U b)) o FMap U f - ≈⟨ car ((IsUniversalMapping.universalMapping ( isUniversalMapping um )) ) ⟩ + ≈⟨ car ((IsUniversalMapping.universalMapping ( UniversalMapping.isUniversalMapping um )) ) ⟩ id1 A (FObj U b) o FMap U f ≈⟨ idL ⟩ FMap U f @@ -232,7 +251,7 @@ (FMap U f o FMap U ((um *) (id1 A (FObj U a )))) o η (FObj U a) ≈⟨ sym assoc ⟩ FMap U f o ( FMap U ((um *) (id1 A (FObj U a ))) o η (FObj U a) ) - ≈⟨ cdr ( IsUniversalMapping.universalMapping ( isUniversalMapping um)) ⟩ + ≈⟨ cdr ( IsUniversalMapping.universalMapping ( UniversalMapping.isUniversalMapping um)) ⟩ FMap U f o id (FObj U a ) ∎ commute : {a b : Obj B} {f : Hom B a b } @@ -244,9 +263,9 @@ ε b o ((_* um) (A [ η (FObj U b) o (FMap U f) ])) ≈⟨⟩ ((_* um) ( id1 A (FObj U b))) o ((_* um) (A [ η (FObj U b) o (FMap U f) ])) - ≈⟨ sym ( ( IsUniversalMapping.uniquness ( isUniversalMapping um ) (lemma-nat1 a b f))) ⟩ + ≈⟨ sym ( ( IsUniversalMapping.uniquness ( UniversalMapping.isUniversalMapping um ) (lemma-nat1 a b f))) ⟩ (_* um) ( A [ FMap U f o id1 A (FObj U a) ] ) - ≈⟨ (IsUniversalMapping.uniquness ( isUniversalMapping um ) (lemma-nat2 a b f)) ⟩ + ≈⟨ (IsUniversalMapping.uniquness ( UniversalMapping.isUniversalMapping um ) (lemma-nat2 a b f)) ⟩ f o ((_* um) ( id1 A (FObj U a))) ≈⟨⟩ f o (ε a) @@ -260,24 +279,32 @@ -- ----- -UMAdjunction : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') - ( U : Functor B A ) - ( F' : Obj A → Obj B ) - ( η' : (a : Obj A) → Hom A a ( FObj U (F' a) ) ) → - (um : UniversalMapping A B U F' η' ) → - Adjunction A B U (FunctorF A B um) (nat-η A B um) (nat-ε A B um) -UMAdjunction A B U F' η' um = record { +UMAdjunction : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') → + (um : UniversalMapping A B ) → + Adjunction A B +UMAdjunction A B um = record { + U = UniversalMapping.U um ; + F = FunctorF A B um ; + η = nat-η A B um ; + ε = nat-ε A B um ; isAdjunction = record { adjoint1 = adjoint1 ; adjoint2 = adjoint2 } } where + U : Functor B A + U = UniversalMapping.U um F : Functor A B F = FunctorF A B um η : NTrans A A identityFunctor ( U ○ F ) η = nat-η A B um + η' : (a : Obj A) → Hom A a ( FObj U (FObj F a) ) + η' = TMap (nat-η A B um) ε : NTrans B B ( F ○ U ) identityFunctor ε = nat-ε A B um + _* : UniversalMapping A B → { a : Obj A}{ b : Obj B} → ( Hom A a (FObj U b) ) → Hom B (FObj F a ) b + _* _ = UniversalMapping._* um + isUniversalMapping = UniversalMapping.isUniversalMapping adjoint1 : { b : Obj B } → A [ A [ ( FMap U ( TMap ε b )) o ( TMap η ( FObj U b )) ] ≈ id1 A (FObj U b) ] adjoint1 {b} = let open ≈-Reasoning (A) in @@ -409,12 +436,8 @@ lemma-2 g h = let open ≈-Reasoning (A) in car ( right-injective ) 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 { + ( adj : Adjunction A B ) → UnityOfOppsite A B (Adjunction.U adj) (Adjunction.F adj) +Adj2UO A B adj = record { right = right ; left = left ; right-injective = right-injective ; @@ -424,6 +447,14 @@ r-cong = r-cong ; l-cong = l-cong } where + U : Functor B A + U = Adjunction.U adj + F : Functor A B + F = Adjunction.F adj + η : NTrans A A identityFunctor ( U ○ F ) + η = Adjunction.η adj + ε : NTrans B B ( F ○ U ) identityFunctor + ε = Adjunction.ε adj 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 ) @@ -440,7 +471,7 @@ 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 )) ⟩ + ≈⟨ car ( IsAdjunction.adjoint1 ( Adjunction.isAdjunction adj )) ⟩ id1 A (FObj U b) o f ≈⟨ idL ⟩ f @@ -457,7 +488,7 @@ ( 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 )) ⟩ + ≈⟨ cdr ( IsAdjunction.adjoint2 ( Adjunction.isAdjunction adj )) ⟩ f o id1 B (FObj F a) ≈⟨ idR ⟩ f @@ -537,9 +568,12 @@ 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) ( uo-η-map A B U F uo ) + ( uo : UnityOfOppsite A B U F) → UniversalMapping A B UO2UM A B U F uo = record { _* = uo-solution A B U F uo ; + U = U ; + F = FObj F ; + η = uo-η-map A B U F uo ; isUniversalMapping = record { universalMapping = universalMapping; uniquness = uniqueness @@ -641,8 +675,12 @@ { U : Functor B A } { F : Functor A B } ( uo : UnityOfOppsite A B U F) - → Adjunction A B U F ( uo-η A B U F uo ) (uo-ε A B U F uo ) + → Adjunction A B UO2Adj A B {U} {F} uo = record { + U = U ; + F = F ; + η = uo-η A B U F uo ; + ε = uo-ε A B U F uo ; isAdjunction = record { adjoint1 = adjoint1 ; adjoint2 = adjoint2