login  home  contents  what's new  discussion  bug reports help  links  subscribe  changes  refresh  edit
 Topics FrontPage Aldor FriCAS language SandBox SandBox Aldor Category Theory SandBox Aldor Category Theory Categories <-- You are here. aldor#include "axiom" #pile #library lBasics "basics.ao" import from lBasics +++ +++ Adjoint functors Left -| Right +++ +++ << and >> are the left and right adjunctions: they are the defining isomorphism +++ +++ Hom(Left A,B) << >> Hom( A, Right B) +++ +++ unit and counit are the equivalent natural transformations. left and right are the +++ action of the Left and Right functors on the arrows. unit, counit, left and right are +++ provided by default. +++ define Adjoint(ObjA:Category,ObjB:Category, Left:ObjA->ObjB, Right:ObjB->ObjA):Category == with { >>: (A:ObjA,B:ObjB, Left A -> B ) -> ( A -> Right B ); -- 1/2 of the adj. isomorphism <<: (A:ObjA,B:ObjB, A -> Right B ) -> ( Left A -> B ); -- 2/2 of the adj. isomorphism unit: (A:ObjA) -> ( A -> Right Left A); -- unit natural transformation counit: (B:ObjB) -> (Left Right B -> B); -- counit natural transformation left: (X:ObjA,Y:ObjA,X->Y) -> ( Left X -> Left Y ); -- Left functor action on morphisms right: (X:ObjB,Y:ObjB,X->Y) -> ( Right X -> Right Y ); -- Right functor action on morphisms default { unit (A:ObjA):(A -> Right Left A) == >>( A,Left A,(l:Left A):Left A +-> l); counit(B:ObjB):(Left Right B -> B) == <<(Right B, B,(r:Right B):Right B +-> r); left (X:ObjA,Y:ObjA,f:X->Y):( Left X -> Left Y) == <<( X,Left Y,(x: X):Right Left Y +-> unit(Y)(f x)); right(X:ObjB,Y:ObjB,f:X->Y):(Right X -> Right Y) == >>(Right X, Y,(x:Left Right X): Y +-> f counit(X)(x) ) } } +++ +++ The right adjoint of Left +++ define RightAdjoint(ObjA:Category,ObjB:Category,Left:ObjA->ObjB):Category == with { Right: ObjB -> ObjA; Adjoint(ObjA,ObjB,Left,Right) } +++ +++ The left adjoint of Right +++ define LeftAdjoint(ObjA:Category,ObjB:Category,Right:ObjB->ObjA):Category == with { Left: ObjA -> ObjB; Adjoint(ObjA,ObjB,Left,Right) } +++ +++ Free construction +++ define FreeConstruction(ObjA:Category,ObjB:Category,Forget:ObjB->ObjA):Category == LeftAdjoint(ObjA,ObjB,Forget) with --LeftCategory(ObjA:Category,CatA:MathCategory ObjA, ObjB:Category, Left:ObjA->ObjB, Ad:RightAdjoint(ObjA,ObjB,Left)):_ -- MathCategory ObjB with { -- if CatA has Initial ObjA then Initial ObjB; -- if CatA has CoProduct ObjA then CoProduct ObjB; -- if CatA has CoEqualizer ObjA then CoEqualizer ObjB; -- if CatA has Pushout ObjA then Pushout ObjB; --} == add { -- if CatA has Initial ObjA then { -- Zero():ObjB == { -- LC0:ObjB == Left Zero() add; -- LC0 add -- } -- zero(A:ObjB):(Zero()->A) == { -- A1:ObjA == (Right$Ad) A; -- z:(Zero$CatA)()->A1 == (zero$CatA)(A1); -- -- error " " -- } -- } -- if CatA has CoProduct ObjA then { -- CoProduct(A:ObjB,B:ObjB):(AB:ObjB,A->AB,B->AB,(X:ObjB)->(A->X,B->X)->(AB->X)) == { -- A1:ObjA == (Right$Ad) A; -- B1:ObjA == (Right$Ad) B; -- (AB1:ObjA,ia1:A1->AB1,ib1:B1->AB1,coproduct1:(X1:ObjA)->(A1->X1,B1->X1)->(AB1->X1)) == (CoProduct$CatA)(A1,B1); -- error " " -- } -- } --} --define LeftCategory(ObjA:Category,CatA:MathCategory ObjA, ObjB:Category,Left:ObjA->ObjB, _ -- Ad:RightAdjoint(ObjA,ObjB,Left)):Category == with { -- if CatA has Initial ObjA then Initial ObjB; -- if CatA has CoProduct ObjA then CoProduct ObjB; -- if CatA has CoEqualizer ObjA then CoEqualizer ObjB; -- if CatA has Pushout ObjA then Pushout ObjB; --} --default { -- if CatA has Initial ObjA then { -- Zero():ObjB == { -- LC0:ObjB == Left Zero() add; -- LC0 add -- } -- } --} ------- this won't work due to bugs in 1.1.12p6 --+++ --+++ Adjoint in general from ObjA to ObjB --+++ --define Adjoint(ObjA:Category,ObjB:Category):Category == with -- Left: ObjA -> ObjB -- Right: ObjB -> ObjA -- Adjoint(ObjA,ObjB,Left,Right) -- --+++ --+++ Free construction via a forgetful functor. This is an adjoint with --+++ conventional renaming. --+++ --define FreeConstruction(ObjA:Category,ObjB:Category):Category == with -- Free: ObjA -> ObjB -- Free: (X:ObjA,Y:ObjA,X->Y) -> (Free X -> Free Y) -- Forget: ObjB -> ObjA -- Forget: (X:ObjB,Y:ObjB,X->Y) -> (Forget X -> Forget Y) -- Adjoint(ObjA,ObjB,Free,Forget) -- default -- Free (X:Domain,Y:Domain,f:X->Y):(Free X->Free Y) == left(X,Y,f) -- Forget(X:Set,Y:Set,f:X->Y):(Forget X->Forget Y) == right(X,Y,f) define Arrow(Obj:Category):Category == with domain: Obj codomain: Obj arrow: domain -> codomain put: (domain,codomain) -> % get: % -> (domain,codomain) Arrow(Obj:Category,A:Obj,B:Obj,f:A->B):Arrow Obj with Set == add domain: Obj == A codomain: Obj == B arrow: domain -> codomain == (x:domain):codomain +-> ( f (x pretend A) ) pretend codomain Rep == domain; import from Rep (x:%)=(y:%):Boolean == if domain has Set then xd:domain == rep x yd:domain == rep y xd = yd else { error "Equality is not defined for this arrow." } coerce(x:%):OutputForm == if domain has Set and codomain has Set then import from codomain import from List OutputForm xd:domain == rep x hconcat [coerce(xd), message "->", coerce arrow xd] else { error "<< not available for this arrow" } put(a:domain,b:codomain):% == if domain has Set and codomain has Set then if not(arrow a=b) then error "An arrow square fails to commute." a pretend % get(x:%):(domain,codomain) == ( rep x , arrow rep x ) #if bugs_get_fixed -- the code below causes runtime errors. --- --- Given a category, the domain below supplies a new category where the --- objects are Arrows and the morphisms are 2-morphisms. --- ArrowCategory(Obj:Category,Cat:MathCategory Obj):MathCategory Arrow Obj with if Cat has Final Obj then Final Arrow Obj if Cat has Initial Obj then Initial Arrow Obj == add if Cat has Final Obj then 1:Arrow Obj == Arrow(Obj,(1$Cat),(1$Cat),(1$Cat)(1$Cat)) 1(A:Arrow Obj):(A->1) == (a:A):1 +-> (1$Cat)@Obj pretend 1 if Cat has Initial Obj then 0:Arrow Obj == Arrow(Obj,(0$Cat),(0$Cat),(0$Cat)(0$Cat)) 0(A:Arrow Obj):(0->A) == (z:0):A +-> never -- -- this does also... just try the most obvious thing and it will blow up -- It seems to be compiler problems. (1.1.12p6) -- --ArrowCategory(Cat:MathCategory Set with Final Set):MathCategory Arrow Set with -- Final Arrow Set --== add -- 1:Arrow Set == Arrow(Set,(1$Cat),(1$Cat),(1$Cat)(1$Cat)) -- 1(A:Arrow Set):(A->1) == (a:A):1 +-> (1$Cat)@Set pretend 1 -- #endif define AutomorphismCategory(Obj:Category,A:Obj):Category == Groups with aut: (A->A,A->A) -> % -- create an automorphism from a morphism and it's inverse aut: % ->(A->A,A->A) -- create a morphism and it's inverse from an automorphism +++ +++ If X is an object in any category, Aut X given below is the group +++ of automorphisms. If the category has Set and CountablyInfinite, +++ autmorphisms are said to be equal if they have equal values at each +++ point in their domain. +++ define Automorphism(Obj:Category):Category == with Aut: (A:Obj) -> AutomorphismCategory (Obj,A) default Aut(A:Obj):AutomorphismCategory(Obj,A) == WW0:AutomorphismCategory(Obj,A) == add Rep == Record(iso:A->A,isi:A->A); import from Rep 1:% == per [(a:A):A +-> a, (a:A):A +-> a] (x:%)=(y:%):Boolean == A has CountablyFinite with Set => import from A forall? ( ((rep x).iso)(a) = ((rep y).iso)(a) for a in (elements$A)() ) error "Equality is not available for these automorphisms." import from o(Obj,A,A,A) (g:%)*(f:%):% == per [ ((rep g).iso) ** ((rep f).iso) , ((rep f).isi) ** ((rep g).isi) ] inv(f:%):% == per [ (rep f).isi, (rep f).iso ] aut(isomorphism:A->A,isomorphismInverse:A->A):% == per [isomorphism,isomorphismInverse] aut(f:%):(A->A,A->A) == explode rep f coerce(f:%):OutputForm == message "[Automorphism]" WW0 add define EndomorphismCategory(Obj:Category,A:Obj):Category == Monoids with end: (A->A) -> % -- create an endomorphisms from a morphism end: % -> (A->A) -- create a morphism from an endomorphism +++ +++ If X is an object in any category, End X given below is the monoid +++ of endomorphisms. If the category has Set and CountablyInfinite, +++ endomorphisms are computed to be equal if they have equal values at +++ each point in their domain. +++ define Endomorphism(Obj:Category):Category == with End: (A:Obj) -> EndomorphismCategory(Obj,A) default End(A:Obj):EndomorphismCategory(Obj,A) == WW1:EndomorphismCategory(Obj,A) == add Rep ==> A->A 1:% == per ( (a:A):A +-> a ) import from o(Obj,A,A,A) (x:%)=(y:%):Boolean == A has CountablyFinite with Set => import from A forall? ( (rep x) a = (rep y) a for a in (elements$A)() ) error "Equality is not available for endomorphisms." (g:%)*(f:%):% == per ( (rep g)**(rep f) ) end(f:A->A):% == per f end(f:%):(A->A) == rep f coerce(f:%):OutputForm == message "[Endomorphism]" WW1 add define Morphisms(Obj:Category):Category == Join(Automorphism Obj, Endomorphism Obj) +++ +++ The Aldor category of mathematical categories +++ define MathCategory(Obj:Category):Category == Join(Id Obj, Compose Obj, Morphisms Obj) +++ +++ One sometimes needs the Hom-style categories where morphisms from A to B +++ are objects in Hom(A,B) rather than A->B. +++ define MathCategory(Obj:Category,Hom:(Obj,Obj)->Domain):Category == with id: (A:Obj) -> Hom(A,A) compose: (A:Obj,B:Obj,C:Obj) -> (Hom(A,B),Hom(B,C)) -> Hom(A,C) +++ +++ Identities +++ define Id(Obj:Category):Category == with id: (A:Obj) -> (A->A) default id(A:Obj):(A->A) == (a:A):A +-> a +++ +++ Composition of Morphisms +++ define Compose(Obj:Category):Category == with compose: (A:Obj,B:Obj,C:Obj) -> (A->B,B->C) -> (A->C) default compose(A:Obj,B:Obj,C:Obj)(f:A->B,g:B->C):(A->C) == (a:A):C +-> g f a +++ +++ Initial Objects +++ define Initial(Obj:Category):Category == with Zero: () -> Obj zero: (A:Obj) -> (Zero()->A) -- 0: Obj -- 0: (A:Obj)->(0->A) +++ +++ Final Objects +++ define Final(Obj:Category):Category == with One: () -> Obj one: (A:Obj) -> (A->One()) -- 1: Obj -- 1: (A:Obj)->(A->1) +++ +++ Equalizer +++ define Equalizer(Obj:Category):Category == with Equalizer: (A:Obj,B:Obj,A->B,A->B) -> (E:Obj,E->A) +++ +++ CoEqualizer +++ define CoEqualizer(Obj:Category):Category == with CoEqualizer: (A:Obj,B:Obj,B->A,B->A) -> (E:Obj,A->E) +++ +++ Pullback Square +++ define Pullback(Obj:Category):Category == with Pullback: (A:Obj,C:Obj,B:Obj) -> (A->C,B->C) -> ( Pullback:Obj, Pullback->A,Pullback->B,(X:Obj,X->A,X->B) -> (X->Pullback)) +++ +++ Pushout Square, the dual of a Pullback Square +++ define Pushout(Obj:Category):Category == with Pushout: (A:Obj,C:Obj,B:Obj) -> (C->A,C->B) -> ( Pushout:Obj, A->Pushout,B->Pushout, (X:Obj,A->X,A->X) -> ( Pushout->X)) +++ +++ Exponential object +++ define Exp(Obj:Category,E:Obj):Category == with rightProductFunctor: Obj -> Obj expFunctor: Obj -> Obj Adjoint(Obj,Obj,rightProductFunctor,expFunctor) define Exponential(Obj:Category):Category == with Exp: (E:Obj) -> Exp(Obj,E) define Hom(Obj:Category):Category == with Hom: (Obj,Obj) -> Obj define Hom?(Obj:Category):Category == with hom?: (Obj,Obj) -> Boolean -- hom?(A,B) answers "Are there any Homs from A to B?" +++ +++ Decategorification +++ define Isomorphic(Obj:Category):Category == with isomorphic?: (A:Obj,B:Obj) -> Boolean Decategorify: Set with { object: Obj -> % } default Decategorify: Set with { object: Obj -> % } == add Rep == Obj object(A:Obj):% == per A (A:%)=(B:%):Boolean == isomorphic? ( rep A, rep B) coerce(A:%):OutputForm == message "[Object]" +++ +++ Cartesian Closed Categories +++ define CartesianClosedCategory(Obj:Category):Category == MathCategory Obj with _ Product Obj with _ Exponential Obj +++ +++ Direct Product of objects and morphisms +++ define Product(Obj:Category):Category == with Product: (A:Obj,B:Obj) -> ( AB:Obj, AB->A, AB->B, (X:Obj)->(X->A,X->B)->(X->AB) ) Product: (A1:Obj,B1:Obj, A2:Obj,B2:Obj) -> (AB1:Obj,AB2:Obj,(A1->A2,B1->B2)->(AB1->AB2)) *:(Obj,Obj)-> with Obj default Product(A1:Obj,B1:Obj,A2:Obj,B2:Obj):(AB1:Obj,AB2:Obj,(A1->A2,B1->B2)->(AB1->AB2)) == (ab1:Obj,pa1:ab1->A1,pb1:ab1->B1, product1: (X:Obj) -> (X->A1,X->B1) -> (X->ab1)) == Product(A1,B1) (ab2:Obj,pa2:ab2->A2,pb2:ab2->B2, product2: (X:Obj) -> (X->A2,X->B2) -> (X->ab2)) == Product(A2,B2) (f:A1->A2)*(g:B1->B2):(ab1->ab2) == product2 ( ab1 )( (x:ab1):A2 +-> f pa1 x, (x:ab1):B2 +-> g pb1 x ) (ab1,ab2,*) (A:Obj)*(B:Obj): with Obj == (AB:Obj,pa:AB->A,pb:AB->B,product:(X:Obj)->(X->A,X->B)->(X->AB)) == Product(A,B) AB add +++ +++ Direct Sum +++ define CoProduct(Obj:Category):Category == with CoProduct: (A:Obj,B:Obj) -> ( AB:Obj, A->AB, B->AB, (X:Obj)->(A->X,B->X)->(AB->X) ) CoProduct: (A1:Obj,B1:Obj, A2:Obj,B2:Obj) -> (AB1:Obj,AB2:Obj,(A2->A1,B2->B1)->(AB2->AB1)) +:(Obj,Obj)-> with Obj default CoProduct(A1:Obj,B1:Obj,A2:Obj,B2:Obj):(AB1:Obj,AB2:Obj,(A2->A1,B2->B1)->(AB2->AB1)) == (ab1:Obj,ia1:A1->ab1,ib1:B1->ab1, sum1: (X:Obj) -> (A1->X,B1->X) -> (ab1->X)) == CoProduct(A1,B1) (ab2:Obj,ia2:A2->ab2,ib2:B2->ab2, sum2: (X:Obj) -> (A2->X,B2->X) -> (ab2->X)) == CoProduct(A2,B2) (f:A2->A1)+(g:B2->B1):(ab2->ab1) == sum2 ( ab1 ) ( (x:A2):ab1 +-> ia1 f x, (x:B2):ab1 +-> ib1 g x ) (ab1,ab2,+) (A:Obj)+(B:Obj): with Obj == (AB:Obj,ia:A->AB,ib:B->AB,product:(X:Obj)->(A->X,B->X)->(AB->X)) == CoProduct(A,B) AB add +++ +++ Multiple Direct Product of a Single Object +++ define MultiProduct(Obj:Category):Category == with Product:(A:Obj,n:Integer) -> (Prod:Obj,Integer->(Prod->A),(X:Obj)->(Tuple (X->A))->(X->Prod)) ^:(Obj,Integer) -> with Obj default (A:Obj)^(n:Integer): with Obj == (Prod:Obj,project:Integer->(Prod->A),product:(X:Obj)->(Tuple (X->A))->(X->Prod)) == Product(A,n) Prod add +++ +++ Multiple Direct Sum of a Single Object +++ define CoMultiProduct(Obj:Category):Category == with CoProduct:(A:Obj,n:Integer) -> ( Sum:Obj,Integer->(A->Sum),(X:Obj)->(Tuple (A->X))->(Sum->X)) ..:(Obj,Integer) -> with Obj default (A:Obj)..(n:Integer): with Obj == (Sum:Obj,insert:Integer->(A->Sum),sum:(X:Obj)->(Tuple (A->X))->(Sum->X)) == CoProduct(A,n) Sum add +++ +++ Quotients +++ define Quotient(Obj:Category):Category == with Quotient: (A:Obj,B:Obj) -> (A->B) -> (Quo:Obj,A->Quo,(X:Obj)->(A->X)->(Quo->X)) /:(A:Obj,B:Obj) -> ((A->B)->Obj) default (A:Obj)/(B:Obj):((A->B)->Obj) == F(f:A->B):Obj == (Q:Obj,insert:A->Q,quo:(X:Obj)->(A->X)->(Q->X)) == Quotient(A,B)(f) Q add F +++ +++ Subobjects (the dual of Quotients) +++ define Subobject(Obj:Category):Category == with Subobject: (A:Obj,B:Obj) -> (B->A) -> (Sub:Obj,Sub->A,(X:Obj)->(X->A)->(X->Sub)) \:(A:Obj,B:Obj) -> ((B->A)->Obj) default (A:Obj)\(B:Obj):(B->A)->Obj == F(f:(B->A)): Obj == (S:Obj,include:S->A,sub:(X:Obj)->(X->A)->(X->S)) == Subobject(A,B)(f) S add F aldor Compiling FriCAS source code from file /var/zope2/var/LatexWiki/categories.as using AXIOM-XL compiler and options -O -Fasy -Fao -Flsp -laxiom -Mno-ALDOR_W_WillObsolete -DAxiom -Y $AXIOM/algebra -I$AXIOM/algebra Use the system command )set compiler args to change these options. #1 (Fatal Error) The file BOOLEAN.ao' is newer than basics.ao'. The )library system command was not called after compilation. Testing aldor#include "axiom" #pile #library lBasics "basics.ao" import from lBasics #library lCategories "categories.ao" import from lCategories A:Arrow(Ring) == Arrow(Ring,Float,Integer,wholePart$Float) add d == domain$A c == codomain$A aldor Compiling FriCAS source code from file /var/zope2/var/LatexWiki/3437562335561908961-25px002.as using AXIOM-XL compiler and options -O -Fasy -Fao -Flsp -laxiom -Mno-ALDOR_W_WillObsolete -DAxiom -Y$AXIOM/algebra -I $AXIOM/algebra Use the system command )set compiler args to change these options. #1 (Fatal Error) The file BOOLEAN.ao' is newer than basics.ao'. The )library system command was not called after compilation. axiom)sh A The )show system command is used to display information about types or partial types. For example, )show Integer will show information about Integer . A is not the name of a known type constructor. If you want to see information about any operations named A , issue )display operations A  axiom)sh d The )show system command is used to display information about types or partial types. For example, )show Integer will show information about Integer . d is not the name of a known type constructor. If you want to see information about any operations named d , issue )display operations d  axiom)sh c The )show system command is used to display information about types or partial types. For example, )show Integer will show information about Integer . c is not the name of a known type constructor. If you want to see information about any operations named c , issue )display operations c sample()$d The function sample is not implemented in NIL . 1()$c The function 1 is not implemented in NIL . arrow(1.1)$A The function arrow is not implemented in NIL . axiomdomain()$A The function domain is not implemented in NIL . codomain()$A The function codomain is not implemented in NIL . ... --Bill Page, Tue, 20 Nov 2007 20:18:38 -0800 replySandBox Aldor Category Theory 3

 Subject:   Be Bold !! ( 15 subscribers )
Please rate this page: