

last edited 13 years ago by Bill Page 
1 2 3 4 5  
Editor:
Time: 2008/08/14 17:43:50 GMT7 

Note: Products and Sums 
changed:  **Product** is a limit in the sense of category theory. Given a set of domains X, Y, ... it constructs a new domain and a function (called 'project') from the new domain to each domain such that <em>for any other domain A and functions f:A>X, g:A>Y, ... there exists a unique function called their 'product' from A into the new domain which commutes with the project functions</em>. "reference":http://en.wikipedia.org/wiki/Product_%28category_theory%29 \begin{aldor}[limits] #pile #include "axiom" Product(X:Type,Y:Type): with product: (A:Type, A>X,A>Y) > (A>%) project: % > X project: % > Y == add Rep == Record(a:X,b:Y) import from Rep  project(x:%):X == rep(x).a project(x:%):Y == rep(x).b product(A:Type,f:A>X,g:A>Y):(A>%) == (x:A):% +> per [f(x),g(x)]  Product(X:Type,Y:Type,Z:Type): with product: (A:Type, A>X,A>Y,A>Z) > (A>%) project: % > X project: % > Y project: % > Z == add Rep == Record(a:X,b:Y,c:Z) import from Rep  project(x:%):X == rep(x).a project(x:%):Y == rep(x).b project(x:%):Z == rep(x).c product(A:Type,f:A>X,g:A>Y,h:A>Z):(A>%) == (x:A):% +> per [f(x),g(x),h(x)] \end{aldor} **Sum** is a colimit in the sense of category theory. Given a set of domains X, Y, ... it constructs a new domain and a function (called 'inject') from each domain to the new domain such that <em>for any other domain A and functions f:X>A, g:Y>A, ... there exists a unique function called their 'sum' from the new domain into A which commutes with the inject functions</em>. "reference":http://en.wikipedia.org/wiki/Coproduct \begin{aldor}[colimits] #pile #include "axiom" Sum(X:Type,Y:Type): with sum: (A:Type, X>A,Y>A) > (% > A)  Given two functions, each with one of the domains in this Sum  and having a common codomain A: returns the unique function with  domain Sum and codomain A inject: X > % inject: Y > % == add Rep == Union(a:X,b:Y) import from Rep  inject(x:X):% == per [a==x] inject(y:Y):% == per [b==y] sum(A:Type,f:X>A,g:Y>A):(%>A) == (x:%):A +> rep(x) case a => f(rep(x).a) rep(x) case b => g(rep(x).b) never  Sum(X:Type,Y:Type,Z:Type): with sum: (A:Type, X>A,Y>A,Z>A) > (% > A)  Given three functions, each with one of the domains in this Sum  and having a common codomain A: returns the unique function with  domain Sum and codomain A inject: X > % inject: Y > % inject: Z > % == add Rep == Union(a:X,b:Y,c:Z) import from Rep  inject(x:X):% == per [a==x] inject(y:Y):% == per [b==y] inject(z:Z):% == per [c==z] sum(A:Type,f:X>A,g:Y>A,h:Z>A):(%>A) == (x:%):A +> rep(x) case a => f(rep(x).a) rep(x) case b => g(rep(x).b) rep(x) case c => h(rep(x).c) never \end{aldor} Limits and colimits are dual concepts in category theory. Notice in particular how the construction of Product and Sum above implement that duality. I am especially interested in how the duality between 'rep' and 'per' is involved in these constructions.
Product is a limit in the sense of category theory. Given a set of domains
X, Y, ... it constructs a new domain and a function (called project
) from
the new domain to each domain such that for any other domain A and functions
f:A>X, g:A>Y, ... there exists a unique function called their product
from
A into the new domain which commutes with the project functions.
#pile #include "axiom" Product(X:Type,Y:Type): with product: (A:Type, A>X,A>Y) > (A>%) project: % > X project: % > Y == add Rep == Record(a:X,b:Y) import from Rep  project(x:%):X == rep(x).a project(x:%):Y == rep(x).b product(A:Type,f:A>X,g:A>Y):(A>%) == (x:A):% +> per [f(x),g(x)]  Product(X:Type,Y:Type,Z:Type): with product: (A:Type, A>X,A>Y,A>Z) > (A>%) project: % > X project: % > Y project: % > Z == add Rep == Record(a:X,b:Y,c:Z) import from Rep  project(x:%):X == rep(x).a project(x:%):Y == rep(x).b project(x:%):Z == rep(x).c product(A:Type,f:A>X,g:A>Y,h:A>Z):(A>%) == (x:A):% +> per [f(x),g(x),h(x)]
Compiling FriCAS source code from file /var/zope2/var/LatexWiki/limits.as using AXIOMXL compiler and options O Fasy Fao Flsp laxiom MnoAXL_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 ./limits.lsp Issuing )library command for limits Reading /var/zope2/var/LatexWiki/limits.asy Product is now explicitly exposed in frame initial Product will be automatically loaded when needed from /var/zope2/var/LatexWiki/limits
Sum is a colimit in the sense of category theory. Given a set of domains
X, Y, ... it constructs a new domain and a function (called inject
) from
each domain to the new domain such that for any other domain A and functions
f:X>A, g:Y>A, ... there exists a unique function called their sum
from
the new domain into A which commutes with the inject functions.
#pile #include "axiom" Sum(X:Type,Y:Type): with sum: (A:Type, X>A,Y>A) > (% > A)  Given two functions, each with one of the domains in this Sum  and having a common codomain A: returns the unique function with  domain Sum and codomain A inject: X > % inject: Y > % == add Rep == Union(a:X,b:Y) import from Rep  inject(x:X):% == per [a==x] inject(y:Y):% == per [b==y] sum(A:Type,f:X>A,g:Y>A):(%>A) == (x:%):A +> rep(x) case a => f(rep(x).a) rep(x) case b => g(rep(x).b) never  Sum(X:Type,Y:Type,Z:Type): with sum: (A:Type, X>A,Y>A,Z>A) > (% > A)  Given three functions, each with one of the domains in this Sum  and having a common codomain A: returns the unique function with  domain Sum and codomain A inject: X > % inject: Y > % inject: Z > % == add Rep == Union(a:X,b:Y,c:Z) import from Rep  inject(x:X):% == per [a==x] inject(y:Y):% == per [b==y] inject(z:Z):% == per [c==z] sum(A:Type,f:X>A,g:Y>A,h:Z>A):(%>A) == (x:%):A +> rep(x) case a => f(rep(x).a) rep(x) case b => g(rep(x).b) rep(x) case c => h(rep(x).c) never
Compiling FriCAS source code from file /var/zope2/var/LatexWiki/colimits.as using AXIOMXL compiler and options O Fasy Fao Flsp laxiom MnoAXL_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 ./colimits.lsp Issuing )library command for colimits Reading /var/zope2/var/LatexWiki/colimits.asy Sum is now explicitly exposed in frame initial Sum will be automatically loaded when needed from /var/zope2/var/LatexWiki/colimits
Limits and colimits are dual concepts in category theory.
Notice in particular how the construction of Product and
Sum above implement that duality. I am especially interested
in how the duality between rep
and per
is involved in
these constructions.