

last edited 14 years ago by Bill Page 
1 2 3 4 5  
Editor: Bill Page
Time: 2008/12/17 08:57:05 GMT8 

Note: Equalizer 
changed: **Product** is a limit in the sense of category theory. Given a set of domains Limits **Product** is a limit in the sense of category theory. Given a set of domains changed: **Sum** is a colimit in the sense of category theory. Given a set of domains **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 <em> 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</em>. "reference":http://en.wikipedia.org/wiki/Equaliser_(mathematics)#In_category_theory In Spad Equalizer can be defined as a 'SubDomain' as follows: \begin{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) \end{spad} \begin{axiom} )show Equalizer(Float,Float,sin,cos) \end{axiom} Colimits **Sum** is a colimit in the sense of category theory. Given a set of domains added:
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" 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)]
Compiling FriCAS source code from file /var/lib/zope2.10/instance/axiomwiki/var/LatexWiki/limits.as using AXIOMXL compiler and options O Fasy Fao Flsp laxiom MnoALDOR_W_WillObsolete DAxiom Y $AXIOM/algebra I $AXIOM/algebra Use the system command )set compiler args to change these options. #1 (Warning) Could not use archive file `libaxiom.al'. #2 (Warning) Could not use archive file `libaxiom.al'. "/usr/local/aldor/linux/1.1.0/include/axiom.as",line 4: import from AxiomLib; ............^ [L4 C13] #3 (Error) No meaning for identifier `AxiomLib'.
"/usr/local/aldor/linux/1.1.0/include/axiom.as",line 15: import { true: %, false: % } from Boolean; ..................................^ [L15 C35] #4 (Error) No meaning for identifier `Boolean'.
"/usr/local/aldor/linux/1.1.0/include/axiom.as",line 17: string: Literal > %; ........................^.......^ [L17 C25] #5 (Error) No meaning for identifier `Literal'. [L17 C33] #6 (Error) There are no suitable meanings for the operator `>'.
"/usr/local/aldor/linux/1.1.0/include/axiom.as",line 18: } from String; .......^ [L18 C8] #8 (Error) No meaning for identifier `String'.
"/var/lib/zope2.10/instance/axiomwiki/var/LatexWiki/limits.as",line 21: Product3(X:SetCategory, Y:SetCategory, Z:SetCategory): with ...........^ [L21 C12] #9 (Error) No meaning for identifier `SetCategory'.
"/var/lib/zope2.10/instance/axiomwiki/var/LatexWiki/limits.as",line 22: construct: (X, Y, Z) > % ..................^.^ [L22 C19] #12 (Error) There are 0 meanings for `Y' in this context. The possible types were: Y: SetCategory, a local The context requires an expression of type Tuple(Type). [L22 C21] #10 (Error) There are 0 meanings for `Z' in this context. The possible types were: Z: SetCategory, a local The context requires an expression of type Tuple(Type).
"/var/lib/zope2.10/instance/axiomwiki/var/LatexWiki/limits.as",line 27: project3: % > Z ................^ [L27 C17] #11 (Error) There are no suitable meanings for the operator `>'. [L27 C17] #13 (Fatal Error) Too many errors (use `M emax=n' or `M noemax' to change the limit).
The )library system command was not called after compilation.
)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
)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.
In Spad Equalizer can be defined as a SubDomain
as follows:
)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)
Compiling FriCAS source code from file /var/lib/zope2.10/instance/axiomwiki/var/LatexWiki/387188355910960424325px003.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.01 SEC.
(time taken in buildFunctor: 0)
;;; *** Equalizer REDEFINED
;;; *** Equalizer REDEFINED Time: 0 SEC.
Cumulative Statistics for Constructor Equalizer Time: 0.01 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 31 JUL 2013 03:11:54 PM):
; /var/aw/var/LatexWiki/EQLZR.NRLIB/EQLZR.fasl written ; compilation finished in 0:00:00.018  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((eq (X %))): Not documented!!!! >>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 31 JUL 2013 03:11:54 PM):
; /var/aw/var/LatexWiki/EQLZF.NRLIB/EQLZF.fasl written ; compilation finished in 0:00:00.013  EqualizerFunctions is now explicitly exposed in frame initial EqualizerFunctions will be automatically loaded when needed from /var/aw/var/LatexWiki/EQLZF.NRLIB/EQLZF
)show Equalizer(Float,Float, sin, cos)
Equalizer(Float,Float, theMap(FLOAT;sin;2$;13, 303), theMap(FLOAT;cos;2$;15, 303)) is a domain constructor. Abbreviation for Equalizer is EQLZR This constructor is exposed in this frame.  Operations 
?=? : (%,%) > Boolean coerce : % > OutputForm eq : % > Float hash : % > SingleInteger latex : % > String ?~=? : (%, %) > Boolean hashUpdate! : (HashState, %) > HashState
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.
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. q:=[2, 3.14, "abc"]$Product3(Integer, Float, String)
There are no library operations named Product3 Use HyperDoc Browse or issue )what op Product3 to learn if there is any operation containing " Product3 " in its name.
Cannot find a definition or applicable library operation named Product3 with argument type(s) Type Type Type
Perhaps you should use "@" to indicate the required return type,or "$" to specify which version of the function you need. r:=["a", "b", "c"]$Product3(String, String, String)
There are no library operations named Product3 Use HyperDoc Browse or issue )what op Product3 to learn if there is any operation containing " Product3 " in its name.
Cannot find a definition or applicable library operation named Product3 with argument type(s) Type Type Type
Perhaps you should use "@" to indicate the required return type,or "$" to specify which version of the function you need. project3 r
There are no library operations named project3 Use HyperDoc Browse or issue )what op project3 to learn if there is any operation containing " project3 " in its name.
Cannot find a definition or applicable library operation named project3 with argument type(s) Variable(r)
Perhaps you should use "@" to indicate the required return type,or "$" to specify which version of the function you need.
#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 codomain A: returns the unique function with  domain Sum and codomain 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 codomain A: returns the unique function with  domain Sum and codomain 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
Compiling FriCAS source code from file /var/lib/zope2.10/instance/axiomwiki/var/LatexWiki/colimits.as using AXIOMXL compiler and options O Fasy Fao Flsp laxiom MnoALDOR_W_WillObsolete DAxiom Y $AXIOM/algebra I $AXIOM/algebra Use the system command )set compiler args to change these options. #1 (Warning) Could not use archive file `libaxiom.al'. #2 (Warning) Could not use archive file `libaxiom.al'. "/usr/local/aldor/linux/1.1.0/include/axiom.as",line 4: import from AxiomLib; ............^ [L4 C13] #5 (Error) No meaning for identifier `AxiomLib'.
"/usr/local/aldor/linux/1.1.0/include/axiom.as",line 15: import { true: %, false: % } from Boolean; ..................................^ [L15 C35] #6 (Error) No meaning for identifier `Boolean'.
"/usr/local/aldor/linux/1.1.0/include/axiom.as",line 17: string: Literal > %; ........................^.......^ [L17 C25] #7 (Error) No meaning for identifier `Literal'. [L17 C33] #8 (Error) There are no suitable meanings for the operator `>'.
"/usr/local/aldor/linux/1.1.0/include/axiom.as",line 18: } from String; .......^ [L18 C8] #10 (Error) No meaning for identifier `String'.
"/var/lib/zope2.10/instance/axiomwiki/var/LatexWiki/colimits.as",line 33: macro rep(x) == x pretend Union(a:X, b:Y) ..............^ [L33 C15] #3 (Warning) Definition of macro `rep' hides an outer definition.
"/var/lib/zope2.10/instance/axiomwiki/var/LatexWiki/colimits.as",line 42: Sum3(X:SetCategory, Y:SetCategory, Z:SetCategory): with .......^ [L42 C8] #11 (Error) No meaning for identifier `SetCategory'.
"/var/lib/zope2.10/instance/axiomwiki/var/LatexWiki/colimits.as",line 46: inject2: Y > % .............^ [L46 C14] #14 (Error) There are 0 meanings for `Y' in this context. The possible types were: Y: SetCategory, a local The context requires an expression of type Tuple(Type).
"/var/lib/zope2.10/instance/axiomwiki/var/LatexWiki/colimits.as",line 48: inject3: Z > % .............^.^ [L48 C14] #12 (Error) There are 0 meanings for `Z' in this context. The possible types were: Z: SetCategory, a local The context requires an expression of type Tuple(Type). [L48 C16] #13 (Error) There are no suitable meanings for the operator `>'.
"/var/lib/zope2.10/instance/axiomwiki/var/LatexWiki/colimits.as",line 73: macro rep(x) == x pretend Union(a:X, b:Y, c:Z) ..............^ [L73 C15] #4 (Warning) Definition of macro `rep' hides an outer definition. [L73 C15] #15 (Fatal Error) Too many errors (use `M emax=n' or `M noemax' to change the limit).
The )library system command was not called after compilation.
)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
)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
)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
)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 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.
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. inject2(1.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. inject3("c")$Sum3(String, String, String)
There are no library operations named Sum3 Use HyperDoc Browse or issue )what op Sum3 to learn if there is any operation containing " Sum3 " in its name.
Cannot find a definition or applicable library operation named Sum3 with argument type(s) Type Type Type
Perhaps you should use "@" to indicate the required return type,or "$" to specify which version of the function you need.
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. f(1)
There are no library operations named f Use HyperDoc Browse or issue )what op f to learn if there is any operation containing " f " in its name.
Cannot find a definition or applicable library operation named f with argument type(s) Integer
Perhaps you should use "@" to indicate the required return type,or "$" to specify which version of the function you need. f(3.14)
There are no library operations named f Use HyperDoc Browse or issue )what op f to learn if there is any operation containing " f " in its name.
Cannot find a definition or applicable library operation named f with argument type(s) Float
Perhaps you should use "@" to indicate the required return type,or "$" to specify which version of the function you need.