|
|
|
last edited 16 years ago by Bill Page |
Edit detail for SandBox Aldor Category Theory 5 revision 5 of 7
| 1 2 3 4 5 6 7 | ||
|
Editor: Bill Page
Time: 2007/11/20 20:49:16 GMT-8 |
||
| Note: | ||
changed: -\begin{aldor} \begin{aldor}[categories]
aldor#include "axiom" #pile #library lBasics "basics.ao" import from lBasics #library lMorphisms "morphisms.ao" import from lMorphisms #library lAdjoints "adjoints.ao" import from lAdjoints +++ +++ 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)->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]"
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-AXL_W_WillObsolete -DAxiom -Y $AXIOM/algebra
Use the system command )set compiler args to change these
options.
#1 (Warning) Deprecated message prefix: use `ALDOR_' instead of `_AXL'
Compiling Lisp source code from file ./categories.lsp
Issuing )library command for categories
Reading /var/zope2/var/LatexWiki/categories.asy
Isomorphic is now explicitly exposed in frame initial
Isomorphic will be automatically loaded when needed from
/var/zope2/var/LatexWiki/categories
Hom? is now explicitly exposed in frame initial
Hom? will be automatically loaded when needed from
/var/zope2/var/LatexWiki/categories
Hom is now explicitly exposed in frame initial
Hom will be automatically loaded when needed from
/var/zope2/var/LatexWiki/categories
Exponential is now explicitly exposed in frame initial
Exponential will be automatically loaded when needed from
/var/zope2/var/LatexWiki/categories
Pushout is now explicitly exposed in frame initial
Pushout will be automatically loaded when needed from
/var/zope2/var/LatexWiki/categories
Pullback is now explicitly exposed in frame initial
Pullback will be automatically loaded when needed from
/var/zope2/var/LatexWiki/categories
CoEqualizer is now explicitly exposed in frame initial
CoEqualizer will be automatically loaded when needed from
/var/zope2/var/LatexWiki/categories
Equalizer is now explicitly exposed in frame initial
Equalizer will be automatically loaded when needed from
/var/zope2/var/LatexWiki/categories
Final is now explicitly exposed in frame initial
Final will be automatically loaded when needed from
/var/zope2/var/LatexWiki/categories
Initial is now explicitly exposed in frame initial
Initial will be automatically loaded when needed from
/var/zope2/var/LatexWiki/categories
Compose is now explicitly exposed in frame initial
Compose will be automatically loaded when needed from
/var/zope2/var/LatexWiki/categories
Id is now explicitly exposed in frame initial
Id will be automatically loaded when needed from
/var/zope2/var/LatexWiki/categories
MathCategory is now explicitly exposed in frame initial
MathCategory will be automatically loaded when needed from
/var/zope2/var/LatexWiki/categories
Exp is now explicitly exposed in frame initial
Exp will be automatically loaded when needed from
/var/zope2/var/LatexWiki/categories... --Bill Page, Tue, 20 Nov 2007 20:47:45 -0800 reply
[SandBox Aldor Category Theory 6]?