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

Edit detail for SandBox Aldor Category Theory 5 revision 7 of 7

 1 2 3 4 5 6 7 Editor: Bill Page Time: 2007/11/21 01:32:50 GMT-8 Note:

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

aldor
```#include "axiom"
#pile
#library    lBasics  "basics.ao"
import from lBasics
#library    lMorphisms  "morphisms.ao"
import from lMorphisms
+++
+++  The Aldor category of mathematical categories
+++
define MathCategory(Obj:Category):Category == Id Obj with Compose Obj with 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)->Domains):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]"```
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.```

SandBox Aldor Category Theory 6