login  home  contents  what's new  discussion  bug reports help  links  subscribe  changes  refresh  edit

# Edit detail for SandBox Aldor Category Theory Categories revision 2 of 2

 1 2 Editor: page Time: 2007/11/21 14:24:23 GMT-8 Note: testing

changed:
-define MathCategory(Obj:Category,Hom:(Obj,Obj)->Domains):Category == with
define MathCategory(Obj:Category,Hom:(Obj,Obj)->Domain):Category == with

Testing
\begin{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 \end{aldor} \begin{axiom} )sh A )sh d )sh c sample()$d
1()$c arrow(1.1)$A
\end{axiom}

\begin{axiom}
domain()$A codomain()$A
\end{axiom}


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
+++
Right: ObjB -> ObjA;
}
+++
+++  The left adjoint of Right
+++
Left:  ObjA -> ObjB;
}
+++
+++  Free construction
+++
--     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;
--    if CatA has Initial ObjA then {
--        Zero():ObjB == {
--            LC0:ObjB == Left Zero() 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, _
--    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;
--        }
--    }
--}
-------  this won't work due to bugs in 1.1.12p6
--+++
--+++  Adjoint in general from ObjA to ObjB
--+++
--    Left:  ObjA -> ObjB
--    Right: ObjB -> ObjA
--
--+++
--+++  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)
--    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
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) ==
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]"
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
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)
+++
+++  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)
+++
+++  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)
+++
+++  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)
+++
+++  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)
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)
F
aldor
   Compiling FriCAS source code from file
/var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/categories.as
using Aldor compiler and options
-O -Fasy -Fao -Flsp -lfricas -Mno-ALDOR_W_WillObsolete -DFriCAS -Y $FRICAS/algebra -I$FRICAS/algebra
Use the system command )set compiler args to change these
options.
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/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/3437562335561908961-25px002.as using Aldor compiler and options -O -Fasy -Fao -Flsp -lfricas -Mno-ALDOR_W_WillObsolete -DFriCAS -Y$FRICAS/algebra -I $FRICAS/algebra Use the system command )set compiler args to change these options. The )library system command was not called after compilation. fricas )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  fricas )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  fricas )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
d is not a valid type.

fricas
domain()\$A
A is not a valid type.

SandBox Aldor Category Theory 3