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

# Edit detail for SandBox Aldor Category Theory 4 revision 5 of 5

 1 2 3 4 5 Editor: Bill Page Time: 2007/11/21 01:40:41 GMT-8 Note:

added:

\begin{axiom}
)library basics.ao
)show Domains
\end{axiom}


aldor
#include "axiom"
#pile
#library    lBasics  "basics.ao"
import from lBasics
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) ==
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]"
define Morphisms(Obj:Category):Category == Automorphism Obj with Endomorphism Obj
aldor
   Compiling FriCAS source code from file
/var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/morphisms.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
)library basics.ao
fricas
Reading /var/aw/var/LatexWiki/basics.asy
Domain is now explicitly exposed in frame initial
Domain will be automatically loaded when needed from
/var/aw/var/LatexWiki/basics
Set is now explicitly exposed in frame initial
Set will be automatically loaded when needed from
/var/aw/var/LatexWiki/basics
Printable is now explicitly exposed in frame initial
Printable will be automatically loaded when needed from
/var/aw/var/LatexWiki/basics
Preorder is now explicitly exposed in frame initial
Preorder will be automatically loaded when needed from
/var/aw/var/LatexWiki/basics
TotalOrder is now explicitly exposed in frame initial
TotalOrder will be automatically loaded when needed from
/var/aw/var/LatexWiki/basics
associativeProduct is now explicitly exposed in frame initial
associativeProduct will be automatically loaded when needed from
/var/aw/var/LatexWiki/basics
Countable is now explicitly exposed in frame initial
Countable will be automatically loaded when needed from
/var/aw/var/LatexWiki/basics
CountablyFinite is now explicitly exposed in frame initial
CountablyFinite will be automatically loaded when needed from
/var/aw/var/LatexWiki/basics
Monoids is now explicitly exposed in frame initial
Monoids will be automatically loaded when needed from
/var/aw/var/LatexWiki/basics
Groups is now explicitly exposed in frame initial
Groups will be automatically loaded when needed from
/var/aw/var/LatexWiki/basics
MapCategory is now explicitly exposed in frame initial
MapCategory will be automatically loaded when needed from
/var/aw/var/LatexWiki/basics
Map is now explicitly exposed in frame initial
Map will be automatically loaded when needed from
/var/aw/var/LatexWiki/basics
Categorify is now explicitly exposed in frame initial
Categorify will be automatically loaded when needed from
/var/aw/var/LatexWiki/basics
null is now explicitly exposed in frame initial
null will be automatically loaded when needed from
/var/aw/var/LatexWiki/basics
o is now explicitly exposed in frame initial
o will be automatically loaded when needed from
/var/aw/var/LatexWiki/basics
fricas
)show Domains
The )show system command is used to display information about types
or partial types. For example, )show Integer will show
)display operations Domains