Limits
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.
reference
fricas
(1) -> <aldor>
#pile
#include "axiom"
Product2(X:SetCategory,Y:SetCategory): with
construct: (X,Y) -> %
coerce: % -> OutputForm
product: (A:Type, A->X,A->Y) -> (A->%)
project1: (%) -> X
project2: (%) -> Y
== add
Rep == Record(a:X,b:Y)
import from Rep
--
construct(x:X,y:Y):% == per [x,y]
coerce(x:%):OutputForm ==
bracket([coerce(rep(x).a)$X, coerce(rep(x).b)$Y]$List(OutputForm))
project1(x:%):X == rep(x).a
project2(y:%):Y == rep(y).b
product(A:Type,f:A->X,g:A->Y):(A->%) ==
(x:A):% +-> per [f(x),g(x)]
--
Product3(X:SetCategory,Y:SetCategory,Z:SetCategory): with
construct: (X,Y,Z) -> %
coerce: % -> OutputForm
product: (A:Type, A->X,A->Y,A->Z) -> (A->%)
project1: % -> X
project2: % -> Y
project3: % -> Z
== add
Rep == Record(a:X,b:Y,c:Z)
import from Rep
--
construct(x:X,y:Y,z:Z):% == per [x,y,z]
coerce(x:%):OutputForm ==
bracket([coerce(rep(x).a)$X, coerce(rep(x).b)$Y, coerce(rep(x).c)$Z]$List(OutputForm))
project1(x:%):X == rep(x).a
project2(y:%):Y == rep(y).b
project3(z:%):Z == rep(z).c
product(A:Type,f:A->X,g:A->Y,h:A->Z):(A->%) ==
(x:A):% +-> per [f(x),g(x),h(x)]</aldor>
fricas
Compiling FriCAS source code from file
/var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/limits.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.
"/var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/limits.as", line 2:
#include "axiom"
^
[L2 C1] #1 (Error) Could not open file `axiom'.
The )library system command was not called after compilation.fricas
)show Product2(Integer,Float)
The )show system command is used to display information about types
or partial types. For example, )show Integer will show
information about Integer .
Product2 is not the name of a known type constructor. If you want
to see information about any operations named Product2 , issue
)display operations Product2
Integer is not the name of a known type constructor. If you want
to see information about any operations named Integer , issue
)display operations Integer
Float is not the name of a known type constructor. If you want to
see information about any operations named Float , issue
)display operations Float
fricas
)show Product3(Integer,Integer,Integer)
The )show system command is used to display information about types
or partial types. For example, )show Integer will show
information about Integer .
Product3 is not the name of a known type constructor. If you want
to see information about any operations named Product3 , issue
)display operations Product3
Integer is not the name of a known type constructor. If you want
to see information about any operations named Integer , issue
)display operations Integer
Integer is not the name of a known type constructor. If you want
to see information about any operations named Integer , issue
)display operations Integer
Integer is not the name of a known type constructor. If you want
to see information about any operations named Integer , issue
)display operations Integer
Equalizer is a limit. Given two domains X, Y and two functions
f:X->Y, g:X->Y, the Equalizer is a new domain E and a function
eq:E->X for which f eq = g eq such that for any other domain M
and function m:M->X for which f m = g m, there exists a unique
function u:M->E such that u eq = m.
reference
In Spad Equalizer can be defined as a SubDomain as follows:
spad
)abbrev domain EQLZR Equalizer
Equalizer(X:SetCategory,Y:SetCategory,f:X->Y, g:X->Y): SetCategory with
eq: % -> X
== SubDomain(X,f #1 = g #1) add
--
eq(x:%):X == x pretend X
)abbrev package EQLZF EqualizerFunctions
EqualizerFunctions(X:SetCategory,Y:SetCategory,f:X->Y,g:X->Y, M:SetCategory,m:M->X): with
u: M->Equalizer(X,Y,f,g)
== add
--
u(x:M):Equalizer(X,Y,f,g) == m(x) pretend Equalizer(X,Y,f,g)
spad
Compiling FriCAS source code from file
/var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/3871883559109604243-25px003.spad
using old system compiler.
EQLZR abbreviates domain Equalizer
------------------------------------------------------------------------
initializing NRLIB EQLZR for Equalizer
compiling into NRLIB EQLZR
compiling exported eq : % -> X
EQLZR;eq;%X;1 is replaced by x
Time: 0 SEC.
(time taken in buildFunctor: 0)
;;; *** |Equalizer| REDEFINED
;;; *** |Equalizer| REDEFINED
Time: 0 SEC.
Cumulative Statistics for Constructor Equalizer
Time: 0 seconds
finalizing NRLIB EQLZR
Processing Equalizer for Browser database:
--->-->Equalizer(constructor): Not documented!!!!
--->-->Equalizer((eq (X %))): Not documented!!!!
--->-->Equalizer(): Missing Description
; compiling file "/var/aw/var/LatexWiki/EQLZR.NRLIB/EQLZR.lsp" (written 19 NOV 2024 03:44:38 AM):
; wrote /var/aw/var/LatexWiki/EQLZR.NRLIB/EQLZR.fasl
; compilation finished in 0:00:00.004
------------------------------------------------------------------------
Equalizer is now explicitly exposed in frame initial
Equalizer will be automatically loaded when needed from
/var/aw/var/LatexWiki/EQLZR.NRLIB/EQLZR
EQLZF abbreviates package EqualizerFunctions
------------------------------------------------------------------------
initializing NRLIB EQLZF for EqualizerFunctions
compiling into NRLIB EQLZF
compiling exported u : M -> Equalizer(X,Y,f,g)
Time: 0 SEC.
(time taken in buildFunctor: 0)
;;; *** |EqualizerFunctions| REDEFINED
;;; *** |EqualizerFunctions| REDEFINED
Time: 0 SEC.
Cumulative Statistics for Constructor EqualizerFunctions
Time: 0 seconds
finalizing NRLIB EQLZF
Processing EqualizerFunctions for Browser database:
--->-->EqualizerFunctions(constructor): Not documented!!!!
--->-->EqualizerFunctions((u ((Equalizer X Y f g) M))): Not documented!!!!
--->-->EqualizerFunctions(): Missing Description
; compiling file "/var/aw/var/LatexWiki/EQLZF.NRLIB/EQLZF.lsp" (written 19 NOV 2024 03:44:38 AM):
; wrote /var/aw/var/LatexWiki/EQLZF.NRLIB/EQLZF.fasl
; compilation finished in 0:00:00.008
------------------------------------------------------------------------
EqualizerFunctions is now explicitly exposed in frame initial
EqualizerFunctions will be automatically loaded when needed from
/var/aw/var/LatexWiki/EQLZF.NRLIB/EQLZFfricas
)show Equalizer(Float,Float,sin,cos)
Equalizer(Float,Float,theMap(FLOAT;sin;2%;10,655),theMap(FLOAT;cos;2%;12,655)) is a domain constructor.
Abbreviation for Equalizer is EQLZR
This constructor is exposed in this frame.
5 Names for 5 Operations in this Domain.
------------------------------- Operations --------------------------------
?=? : (%, %) -> Boolean coerce : % -> OutputForm
eq : % -> Float latex : % -> String
?~=? : (%, %) -> Boolean
Co-limits
Sum is a co-limit 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.
reference
fricas
p:=[2,3.14]$Product2(Integer,Float)
There are no library operations named Product2
Use HyperDoc Browse or issue
)what op Product2
to learn if there is any operation containing " Product2 " in its
name.
Cannot find a definition or applicable library operation named
Product2 with argument type(s)
Type
Type
Perhaps you should use "@" to indicate the required return type,
or "$" to specify which version of the function you need.
aldor
#pile
#include "axiom"
Sum2(X:SetCategory,Y:SetCategory): with
coerce: % -> OutputForm
inject1: X -> %
coerce: X -> %
inject2: Y -> %
coerce: Y -> %
== add
Rep == Union(a:X,b:Y)
import from Rep, Integer
--
coerce(x:%):OutputForm ==
rep(x) case a => sub(coerce(rep(x).a)$X,outputForm 1)
rep(x) case b => sub(coerce(rep(x).b)$Y,outputForm 2)
never
inject1(x:X):% == per [a==x]
coerce(x:X):% == per [a==x]
inject2(y:Y):% == per [b==y]
coerce(y:Y):% == per [b==y]
-- Note: There is a problem with dependent domains in FriCAS so
-- it is necessary to define 'sum' in a separate package.
Sum2Functions(X:SetCategory,Y:SetCategory,A:SetCategory): with
sum: (X->A,Y->A) -> (Sum2(X,Y) -> A)
-- Given two functions, each with one of the domains in this Sum
-- and having a common co-domain A: returns the unique function with
-- domain Sum and co-domain A
== add
-- Requires same Rep as domain Sum2!
macro rep(x) == x pretend Union(a:X,b:Y)
import from Union(a:X,b:Y)
--
sum(f:X->A,g:Y->A):(Sum2(X,Y)->A) ==
(x:Sum2(X,Y)):A +->
rep(x) case a => f(rep(x).a)
rep(x) case b => g(rep(x).b)
never
--
Sum3(X:SetCategory,Y:SetCategory,Z:SetCategory): with
coerce: % -> OutputForm
inject1: X -> %
coerce: X -> %
inject2: Y -> %
coerce: Y -> %
inject3: Z -> %
coerce: Z -> %
== add
Rep == Union(a:X,b:Y,c:Z)
import from Rep, Integer
--
coerce(x:%):OutputForm ==
rep(x) case a => sub(coerce(rep(x).a)$X,outputForm 1)
rep(x) case b => sub(coerce(rep(x).b)$Y,outputForm 2)
rep(x) case c => sub(coerce(rep(x).c)$Z,outputForm 3)
never
inject1(x:X):% == per [a==x]
coerce(x:X):% == per [a==x]
inject2(y:Y):% == per [b==y]
coerce(y:Y):% == per [b==y]
inject3(z:Z):% == per [c==z]
coerce(z:Z):% == per [c==z]
Sum3Functions(X:SetCategory,Y:SetCategory,Z:SetCategory,A:SetCategory): with
sum: (X->A,Y->A,Z->A) -> (Sum3(X,Y,Z) -> A)
-- Given three functions, each with one of the domains in this Sum
-- and having a common co-domain A: returns the unique function with
-- domain Sum and co-domain A
== add
-- Requires same Rep as domain Sum3!
macro rep(x) == x pretend Union(a:X,b:Y,c:Z)
import from Union(a:X,b:Y,c:Z)
--
sum(f:X->A,g:Y->A,h:Z->A):(Sum3(X,Y,Z)->A) ==
(x:Sum3(X,Y,Z)):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
aldor
Compiling FriCAS source code from file
/var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/colimits.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.
"/var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/colimits.as", line 2:
#include "axiom"
^
[L2 C1] #1 (Error) Could not open file `axiom'.
The )library system command was not called after compilation.fricas
)show Sum2(Integer,Float)
The )show system command is used to display information about types
or partial types. For example, )show Integer will show
information about Integer .
Sum2 is not the name of a known type constructor. If you want to
see information about any operations named Sum2 , issue
)display operations Sum2
Integer is not the name of a known type constructor. If you want
to see information about any operations named Integer , issue
)display operations Integer
Float is not the name of a known type constructor. If you want to
see information about any operations named Float , issue
)display operations Float
fricas
)show Sum2Functions(Integer,Float,Integer)
The )show system command is used to display information about types
or partial types. For example, )show Integer will show
information about Integer .
Sum2Functions is not the name of a known type constructor. If you
want to see information about any operations named Sum2Functions
, issue
)display operations Sum2Functions
Integer is not the name of a known type constructor. If you want
to see information about any operations named Integer , issue
)display operations Integer
Float is not the name of a known type constructor. If you want to
see information about any operations named Float , issue
)display operations Float
Integer is not the name of a known type constructor. If you want
to see information about any operations named Integer , issue
)display operations Integer
fricas
)show Sum3(Integer,Float,String)
The )show system command is used to display information about types
or partial types. For example, )show Integer will show
information about Integer .
Sum3 is not the name of a known type constructor. If you want to
see information about any operations named Sum3 , issue
)display operations Sum3
Integer is not the name of a known type constructor. If you want
to see information about any operations named Integer , issue
)display operations Integer
Float is not the name of a known type constructor. If you want to
see information about any operations named Float , issue
)display operations Float
String is not the name of a known type constructor. If you want
to see information about any operations named String , issue
)display operations String
fricas
)show Sum3Functions(Integer,Float,String)
The )show system command is used to display information about types
or partial types. For example, )show Integer will show
information about Integer .
Sum3Functions is not the name of a known type constructor. If you
want to see information about any operations named Sum3Functions
, issue
)display operations Sum3Functions
Integer is not the name of a known type constructor. If you want
to see information about any operations named Integer , issue
)display operations Integer
Float is not the name of a known type constructor. If you want to
see information about any operations named Float , issue
)display operations Float
String is not the name of a known type constructor. If you want
to see information about any operations named String , issue
)display operations String
Limits and co-limits 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.
fricas
inject1(-1)$Sum2(Integer,Float)
There are no library operations named Sum2
Use HyperDoc Browse or issue
)what op Sum2
to learn if there is any operation containing " Sum2 " in its
name.
Cannot find a definition or applicable library operation named Sum2
with argument type(s)
Type
Type
Perhaps you should use "@" to indicate the required return type,
or "$" to specify which version of the function you need.
fricas
f:Sum2(Integer,Float)->Integer:=sum(abs$Integer,wholePart$Float)
There are no library operations named Sum2
Use HyperDoc Browse or issue
)what op Sum2
to learn if there is any operation containing " Sum2 " in its
name.
Cannot find a definition or applicable library operation named Sum2
with argument type(s)
Type
Type
Perhaps you should use "@" to indicate the required return type,
or "$" to specify which version of the function you need.