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

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

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

changed:
-
\begin{aldor}
#include "axiom"
#pile

#library    lBasics  "basics.ao"
import from lBasics
       
+++
+++  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)

+++
+++  Cartesian Closed Categories
+++
define CartesianClosedCategory(Obj:Category):Category == MathCategory Obj with _
                                                              Product Obj with _
                                                          Exponential Obj 
+++
+++  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)   

+++
+++  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:A->B):Obj +-> 
	        (Q:Obj,insert:A->Q,quo:(X:Obj)->(A->X)->(Q->X)) == Quotient(A,B)(f)
		Q add
                
+++
+++   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:(B->A)):Obj +->
	        (S:Obj,include:S->A,sub:(X:Obj)->(X->A)->(X->S)) == Subobject(A,B)(f)
		S add 
+++
+++   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]"
    
\end{aldor}

aldor
#include "axiom" #pile #library lBasics "basics.ao" import from lBasics +++ +++ 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) +++ +++ Cartesian Closed Categories +++ define CartesianClosedCategory(Obj:Category):Category == MathCategory Obj with _ Product Obj with _ Exponential Obj +++ +++ 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) +++ +++ 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:A->B):Obj +-> (Q:Obj,insert:A->Q,quo:(X:Obj)->(A->X)->(Q->X)) == Quotient(A,B)(f) Q add +++ +++ 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:(B->A)):Obj +-> (S:Obj,include:S->A,sub:(X:Obj)->(X->A)->(X->S)) == Subobject(A,B)(f) S add +++ +++ 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/4547353633820463542-25px001.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'
"/var/zope2/var/LatexWiki/4547353633820463542-25px001.as", line 10: 
define MathCategory(Obj:Category):Category == Id Obj with Compose Obj with Morphisms Obj
...........................................................................^
[L10 C76] #3 (Error) There are no suitable meanings for the operator `Morphisms'.
"/var/zope2/var/LatexWiki/4547353633820463542-25px001.as", line 169: 
    Adjoint(Obj,Obj,rightProductFunctor,expFunctor)
....^
[L169 C5] #2 (Error) There are no suitable meanings for the operator `Adjoint'.
   The )library system command was not called after compilation.