diff --git a/books/bookvol2.pamphlet b/books/bookvol2.pamphlet index da71de9..302dc0c 100644 --- a/books/bookvol2.pamphlet +++ b/books/bookvol2.pamphlet @@ -377,7 +377,111 @@ Roland Backhouse and Marcel Bijsterveld ``Category Theory as Coherently Constructive Lattice Theory'' November 1994 -\chapter{Implementation Details} +\section{Terms to Understand} + +Suppose we wish to join Complex with Polynomial(Integer). +What would elements of this combination look like? + +The union of the two is a co-product of topological spaces. + +The simple combination is not simply adding elements since +\[i + x^2\] +is not a valid combination. + +We need the algebraic co-product, known as the tensor product. +We end up with a domain of Complex(Polynomial(Integer)). + +\begin{verbatim} +-> a:Complex(POLY(INT)):=%i+3*x + + 3x + %i + Type: Complex(Polynomial(Integer)) +-> a::POLY(COMPLEX(INT)) + + 3x + %i + Type: Polynomial(Complex(Integer)) +\end{verbatim} + +\section{Category Definition} +A category has four parts. +We need a set of objects, usually represented as dots. +We need a set of arrows (maps, morphisms), from dot to dot. +We need a way to compose arrows in an associative manner. +We need an identity arrow from a dot to itself. + +The set of all arrows from dot A to dot B is written as $Hom_c(A,B)$ +or, sometimes $C(A,B)$. Notice that the set $C(A,B)$ is disjoint from +$C(A,D)$ since each arrow has a unique domain and co-domain. + +For the example of the category Set, the objects are sets and the +arrows are functions between sets. +For the category Ring, the objects are rings and the arrows are ring +homomorphisms. +Similarly for the category Group, the dots are groups and the arrows +are group homomorphisms. +For a fixed Ring R, the category R-Mod has dots which +are left R-modules and the arrows are R-module homomorphisms. +We can also look at the category Mod-R which has dots of right R-modules +and arrows which are R-module homomorphisms. +For the category K, if K is a field, the dots are K-vector spaces and +the arrows are K-linear transformations. + +In Axiom the dots are Types (such as Integer or Character) and the +arrows are functions between them with signature: +\begin{verbatim} + f : Integer -> Character +\end{verbatim} + +Relations between categories is called a {\bf functor}. +A functor F takes things in category C into things in category D. +We need a function on objects which maps objects of C to objects of D. +We need a function on arrows which take arrows of C to arrows of D. + +The categories C and D well defined structure. +They have a domain and co-domain of arrows. +They have identity arrows. +There is a rule of composition of arrows. These form commutative diagrams. + +First we have to make sure the functor F maintains the domain and co-domain +structure of C. +When we apply functor F to C we need to preserve all of the structure +so F has to be defined on all of these properties. If we look at two +dots in category C and a function f which is an arrow in C +\begin{verbatim} + f + A ----> B +\end{verbatim} +then the functor F has to operate on everything so we get: +\begin{verbatim} + Ff + FA ----> FB +\end{verbatim} +This means that if $dom$ is the domain function in C then the functor +F commutes with $dom$. That is, applying $F(dom(f)) = dom(F(f))$. + +Next we have to make sure the functor F maintains the identity arrow of C. +From the above we know that $F(identity(x)) = identity(F(x))$. + +Finally we have to make sure that the rule for composition of arrows +in C is preserved. So the functor F has to make sure that what composes +in C also composes with the same diagram in D. + +Some standard functors are the identity functor $1_c$ which just maps +C to C. We can form a functor which forgets properties so that the +category Group could map to its underlying set. We can lift a category +by forgetting properties, for example, lifting the category of Abelian +Group C to Group D by ``forgetting'' the commutative property of C. +Similarly the category Ring or the category Module can be mapped to +the underlying Abelian Group. There is also the Constant functor which +maps all of the dots in C to a single dot in D and all of the arrows in +C to the identity arrow in D. + +The category CommutativeRing R can be mapped to a Group with the functor +$GL_n$ which is the group of invertible NxN matrices with entries in +the CommutativeRing R. + + +\chapter{Axiom Implementation Details} \section{Makefile} This book is actually a literate program\cite{2} and can contain executable source code. In particular, the Makefile for this book diff --git a/changelog b/changelog index 0925c8d..b5f35fa 100644 --- a/changelog +++ b/changelog @@ -1,3 +1,5 @@ +20130316 tpd src/axiom-website/patches.html 20130316.03.tpd.patch +20130316 tpd books/bookvol2 category theory notes 20130316 tpd src/axiom-website/patches.html 20130316.02.tpd.patch 20130316 tpd buglist SOLVERAD fix 40043 20130316 tpd books/bookvol10.4 SOLVERAD fix 40043 diff --git a/src/axiom-website/patches.html b/src/axiom-website/patches.html index 02903b9..eee48bb 100644 --- a/src/axiom-website/patches.html +++ b/src/axiom-website/patches.html @@ -4073,5 +4073,7 @@ books/bookvol10.2 CLAGG fixed 40021 books/bookvol10.3 CHAR fix 40022 20130316.02.tpd.patch books/bookvol10.4 SOLVERAD fix 40043 +20130316.03.tpd.patch +books/bookvol2 category theory notes