This blog has moved to a new location: http://www.abstractmath.org/Word%20Press/
During the move, most links were trashed and so were some posts. Most of the difficulty occurred in a long sequence of posts about turning definitions into mathematical objects. Because of this, I have retained those files here on the old site until I can merge them into one long article. Once I do this, this website will disappear.
All the other articles on the site have been trashed. They are all on the new site. Some of the links in the articles published before 2010 have not yet been repaired.
with the following structure:
and 
of 
and an arrow 
. 
of 
such that for every arrow 
, the diagram below commutes:
(lameval)
, ![lambda(text{eval}circ(gtimestext{Id}[A]))=g](http://s0.wp.com/latex.php?latex=lambda%28text%7Beval%7Dcirc%28gtimestext%7BId%7D%5BA%5D%29%29%3Dg&bg=ffffff&fg=494949&s=0 "lambda(text{eval}circ(gtimestext{Id}[A]))=g")
.
is a natural isomorphism of homsets.
is called currying or partial application. You can curry a multivariable function all the way down to a constant. The inverse process is usually called uncurrying. It constitutes getting rid of entries in the codomain of a function that are function spaces by adding variables to the function. I suggest using blanding instead of “uncurrying”.
that formally picks out the identity arrow of an object.
, the formal set of functions of two variables, in other words arrows of the form 
that picks out the arrow 
itself.
that picks out the source 
of a two-variable function 
, the formal set of curried functions from 
.
and 
that pick out the source and target of a curried function 
that picks out the function space 
, the formal set of composable pairs of arrows in the FL sketch for categories, defined by this pullback diagram:
(Ar2Def)
as defined by this diagram:
(Bsource)
the properties it needs:
(Curry)
(Compreq)
and 
such that
(ret)
is a retract of 
(ReflFSConeBase)
that satisfies Diagram (lameval) above, so the mandatory projections would be to 
, 
and 
. The projection to 
is induced by Diagram (Curry) above, the projection to 
by Diagram (Ar2Def), and the projection to 
follows from the fact that it is the vertex of the product cone shown. The other projections exist by composition.
for “reflexive function space”. Note that all the objects and arrows in this diagram exist in the FL sketch for cartesian closed categories.
of the FL sketch for CCC’s, 
would be the set of reflexive function spaces together with specified inclusion 
has models we can call C-categories. In particular a model for CCCSk in sets is a cartesian closed category. In previous posts I have constructed constructor spaces for categories with finite products and categories with finite limits.
in the FL Cattheory of 
where 1 is the terminal object. 
.
“ means that 
is nonempty.
, the formal set of arrows 
and the formal set of composable pairs of arrows 
, as well as arrows
that formally pick the source and target of an arrow and
that picks out the composite of a pair of arrows.
(Diagram 
)
)
, the formal set of cones of the form 
, the formal set of fill-in diagrams (diagrams of the form of F above).
, that picks out the product cone over a pair of objects.
, that picks out the source cone of a fill-in arrow.
, that picks out the target cone of a fill-in arrow.
, that takes a cone to the unique fill-in diagram that has the cone as source cone.
that formally picks out the fill-in arrow in a fill-in diagram.
and 
.
symbol can mean multiplication of numbers, of matrices, or cross product of vectors.) When I first came across this aspect of mathematics in a matrix theory course at 
, which in a model will become the set of objects – so in our “formal” terminology is the formal set of objects. (This terminology, by the way, is due to 
, the formal set of arrows.
, the formal set of composable pairs of arrows.
, the formal set of composable triples of arrows, needed to state the associative law.
that formally picks the identity arrow of an object
given a composable triple.
and diagrams for associativity and to make the identity arrows behave right. The details are in GLBS (reference [1]), chapter 7.
are diagrams that look like this:
, then the category of models has sortwise products. In most of the references the name “pointwise” is used.
with a finite set 
of finite 
in an FL category 
.
together with a model
with the the property that for any model 
of 
in 
.
are defined in the same way, except that the finite diagrams that the cones are over have to be discrete, and it has properties analogous to those for FL sketches given above. Note that any FP sketch or linear sketch will also have an FL cattheory.
of models of 
.
in 
; 
of objects of a category consists of an object v of the category and one arrow from v to each object in 
in a category. I am specifically not assuming it is commutative. A commutative cone to 
(a)
(b)
(c)
(d)
is a functor from the digraph to 
. The fill-in arrow is an operation on a set of tuples of arrows, but the domain is not the cartesian products of arrow sets; instead it is an equationally defined subset of a cartesian product of arrow sets.
and 
. This is just a technicality although some mathematicians make a big deal out of it. In fact when mathematicians talk about the “category of groups” they don’t usually even say which product cone they mean by 
where G is a digraph and D is a set of 
, is the free category generated by G with the condition imposed that the diagrams in D must become commutative. The digraph morphism 
that takes the nodes and arrows in G to the corresponding objects and arrows of the free category is by definition a 
. G is called the generic model of the sketch.
. The category of models of the cattheory 
.
, where “LS” refers to linear sketches. That is the 
be the digraph at the left. It has one node c and one arrow s, whose source and target are (necessarily) c. A model of this sketch is a set C and a function from C to itself. Any such function determines a cyclic semigroup of transformations of C. For later use, I want to mention the the particular model in which C is the set of natural numbers and s is the successor function: this is the free semigroup on one letter.
in every model in Set. This means we must require that the diagram (in the category of sets) below commute for every model M.
To say that this diagram commutes requires that 
(see Note 1.) 
under M is a commutative diagram in the category of sets. 
consists of a digraph G together with a set 
with the property that M takes every diagram in to a commutative diagram in Set. (Note 2).
and 
.
A sketch is a graph-based specification of a type of mathematical structure. The sketch for directed graphs is shown at the right. It is itself a graph, which is confusing. Get used to it. That is ultimately the key to the idea of form.
and 
of 
and 
of 
to 
is a pair of functions 
and 
for which these diagrams commute:
If you 
is a morphism of directed graphs.
), and many other things. We can go further and sketch special kinds of categories (cartesian closed, toposes, and others) which we will need to do to create forms with more power than sketches. (Note 3).
