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/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