Re: sketch theory

Re: sketch theory

[Steve Lack]

On 25/05/09 3:03 PM, "John Baez" <john.c.baez@gmail.com> wrote:

> Steve Lack writes:
>
> You ask about a sketch for cartesian closed categories. Have a look at
>> at the paper "A presentation of topoi as algebraic relative to categories
>> or
>> graphs (Dubuc-Kelly, J. Alg. 81: 420-433, 1983). This describes something
>> even tighter: the category of cartesian closed categories is monadic over
>> the category of graphs.
>>
>
> Thanks!
>
> And thanks to everyone else for their helpful comments.  I'm behind on
> answering my emails.
>
> In this approach, does each pair of objects in a ccc come with a chosen
> product and exponential? Are the morphisms of ccc's are required to preserve
> these on the nose?

Yes, that's right on both counts, but see below.

>
> At first I was a bit shocked to hear of a sketch for ccc's, because the
> internal hom is contravariant in one variable.  But I guess that as long as
> we treat ccc's purely 1-categorically that's no problem.  But then I guess
> we pay the price of "undue strictness".  Right?

As you say, if you work 1-categorically, you are stuck with undue
strictness. And as you imply, there is an impediment to a fully
2-categorical approach because of the contravariance of the internal hom.
But there is a way around this. You work 2-categorically, but not over the
2-category Cat, but over the 2-category of categories, functors, and natural
_isomorphisms_. (Kelly & co call this 2-category Cat_g, with g presumably
standing for groupoidal, since this is not just enriched in Cat but in
groupoids.) Then the internal hom does indeed become a 2-functor
Cat^2_g-->Cat_g.

Having these invertible 2-cells now allows you to consider pseudomorphisms
of algebras, which preserve structure up to isomorphism, thus alleviating
the problem of undue strictness. It doesn't completely solve it - since we
only have invertible 2-cells, we don't have a notion of lax morphism; or,
more precisely, the notion of lax morphism we get is just that of
pseudomorphism. Similarly, some constructions might not give what we hoped
for. For example, the cotensor C^2 in Cat_g is not the category of arrows in
C, it's the category of invertible arrows in C.

All the best,

Steve.





[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: sketch theory

[John Baez]

Steve Lack writes:

You ask about a sketch for cartesian closed categories. Have a look at
> at the paper "A presentation of topoi as algebraic relative to categories
> or
> graphs (Dubuc-Kelly, J. Alg. 81: 420-433, 1983). This describes something
> even tighter: the category of cartesian closed categories is monadic over
> the category of graphs.
>

Thanks!

And thanks to everyone else for their helpful comments.  I'm behind on
answering my emails.

In this approach, does each pair of objects in a ccc come with a chosen
product and exponential? Are the morphisms of ccc's are required to preserve
these on the nose?

At first I was a bit shocked to hear of a sketch for ccc's, because the
internal hom is contravariant in one variable.  But I guess that as long as
we treat ccc's purely 1-categorically that's no problem.  But then I guess
we pay the price of "undue strictness".  Right?

Best,
jb

Re: sketch theory

[Zinovy Diskin]

Let me make a few clarifying remarks

On Fri, May 22, 2009 at 8:44 PM,  <Andre.Rodin@ens.fr> wrote:

> I came across this recent paper by Diskin&Wolter
>
> http://www.cs.toronto.edu/~zdiskin/Pubs/ACCAT-07.pdf
>
> where the authors propose a version of sketch-based syntax for Computer Science
> purposes. The main idea here (as far as I understood the paper) is to use
> sketches as arities of predicates. I heard about similar ideas from Rene
> Guitart in private conversations (but Rene's approach is algebraic rather than
> logical).

our version of sketches is intended for use in software engineering,
not only in computer science. The difference between them is like the
difference between, say, electrical engineering and physics.

Predicate arities may be objects of any a priori chosen good category,
e.g., sketches built in a previous step, but this is not the main
idea. Relation of Makkai's generalized sketches to classical sketches
is, roughly, like relation of a general first-order theory a la Tarski
to a particular family of theories like, e.g., lattice theory. The
former provide a general framework, in which the user can define any
theory she likes. The latter is a family of particular instantiations
of the framework. The fact that this family is expressive enough to
specify any structure is another story.

A first-order signature contains operation and predicate symbols.
Similarly, a generalized sketch signature may contain operation
symbols too (whose arities are In-Out spans). Definitions and some
details can be found in Report referenced as [6] in the paper above.

ZD



Looking at GBLS briefly I couldn't immediately grasp if your and
> Atish Bagchi's approach to graph-based logic is based on similar ideas or your
> approach is quite different. I certainly should read GBLS more carefully for
> discussing it but I would grateful for a hint.
>
> Andrei
>
>
>
> Selon Charles Wells <charles@abstractmath.org>:
>
>> I have not kept up with the field very well, but I can recommend these
>> works:
>>
>> Peter Johnstone, *Sketches of an Elephant*, Vol. 2, OUP 2003: the chapter on
>> sketches.  (I am in rural Wisconsin at the moment asnd don't have access to
>> the book.  If OUP would make its pages available to look at on Amazon I
>> could have told you the exact page.)
>>
>> Bagchi and Wells, *Graph Based Logic and Sketches*, here:
>>
>> http://arxiv.org/PS_cache/arxiv/pdf/0809/0809.3023v1.pdf
>>
>> Also Kinoshita, et al 1997, referred to in GBLS.  There might be relevant
>> papers since 1993 mentioned in the Elephant, too.
>>
>> Category people:  If you can suggest other papers that should be included,
>> let me know soon, and I will revise the sketches paper to include them (and
>> the ones I mentioned above).
>>
>> Charles Wells
>>
>>
>
>

Re: sketch theory

[Steve Lack]

Dear John,

You ask about a sketch for cartesian closed categories. Have a look at
at the paper "A presentation of topoi as algebraic relative to categories or
graphs (Dubuc-Kelly, J. Alg. 81: 420-433, 1983). This describes something
even tighter: the category of cartesian closed categories is monadic over
the category of graphs.

If you look at the description given in that paper, it clearly contains a
sketch for cartesian closed categories (this depends heavily paper on the
paper Algebres Graphique of Albert Burroni). In fact the Dubuc-Kelly paper
also describes a notion of presentation for finitary monads on Cat; this was
later developed by Kelly and Power into a fully-fledged theory of
presentations for finitary enriched monads on locally finitely preseentable
categories, in their paper " Adjunctions whose counits are coequalizers, and
presentations of finitary enriched monads" (JPAA 89:163-179, 1993).

Regards,

Steve Lack.


On 22/05/09 5:43 AM, "John Baez" <john.c.baez@gmail.com> wrote:

> Dear Categorists -
>
> Andrei Rodin pointed out this paper by Charles Wells:
>
> http://www.cwru.edu/artsci/math/wells/pub/pdf/sketch.pdf
>
> I took a look.  In section 4.1 it mentions that people have given a finite
> limits sketch for cartesian closed categories.  I'm curious about how this
> works,  Unfortunately the list of references given here is quite long.  Can
> anyone help me find a reference on a sketch for CCC's?
>
> Best,
> jb
>
>

Re: sketch theory

[Zinovy Diskin]

Dear Andrei,
   Speaking about research programmes,  Makkai's generalized sketches
should definitely be mentioned. An easy introduction can be found in

A Diagrammatic Logic for Object-Oriented Visual Modeling
Zinovy Diskin and Uwe Wolter
DOI Bookmark:	10.1016/j.entcs.2008.10.041

It provides references to Makkai's papers and some other sources, and
briefly describes some history and motivations. You may skip all
sentiments about engineering applications, or do just the opposite --
pay attention to them -- at least, this is what granting agencies
like.

There are two distinctions from Makkai's sketches: a signature of
diagram predicates is a category rather than a set, and semantics is
given in terms of functors into sketches rather than from them.

ZD

2009/5/20 Andre.Rodin <Andre.Rodin@ens.fr>:
> Dear Charles and others:
>
> this
>
> http://www.cwru.edu/artsci/math/wells/pub/pdf/sketch.pdf
>
> is your very useful overview of Sketch theory dated back to 1993. I wonder how
> much it omits today: are there significant research programmes in this field
> emerged during last 15 years? What should I look at first of all? Many thanks
> in advance.
>
> Andrei
>
>
>
>

Re: sketch theory

[Andre.Rodin]

many thanks, Charles, somehow I forgot that the Elephant is also about Sketches.
I came across this recent paper by Diskin&Wolter

http://www.cs.toronto.edu/~zdiskin/Pubs/ACCAT-07.pdf

where the authors propose a version of sketch-based syntax for Computer Science
purposes. The main idea here (as far as I understood the paper) is to use
sketches as arities of predicates. I heard about similar ideas from Rene
Guitart in private conversations (but Rene's approach is algebraic rather than
logical). Looking at GBLS briefly I couldn't immediately grasp if your and
Atish Bagchi's approach to graph-based logic is based on similar ideas or your
approach is quite different. I certainly should read GBLS more carefully for
discussing it but I would grateful for a hint.

Andrei



Selon Charles Wells <charles@abstractmath.org>:

> I have not kept up with the field very well, but I can recommend these
> works:
>
> Peter Johnstone, *Sketches of an Elephant*, Vol. 2, OUP 2003: the chapter on
> sketches.  (I am in rural Wisconsin at the moment asnd don't have access to
> the book.  If OUP would make its pages available to look at on Amazon I
> could have told you the exact page.)
>
> Bagchi and Wells, *Graph Based Logic and Sketches*, here:
>
> http://arxiv.org/PS_cache/arxiv/pdf/0809/0809.3023v1.pdf
>
> Also Kinoshita, et al 1997, referred to in GBLS.  There might be relevant
> papers since 1993 mentioned in the Elephant, too.
>
> Category people:  If you can suggest other papers that should be included,
> let me know soon, and I will revise the sketches paper to include them (and
> the ones I mentioned above).
>
> Charles Wells
>
>

Re: sketch theory

[Charles Wells]

I have not kept up with the field very well, but I can recommend these
works:

Peter Johnstone, *Sketches of an Elephant*, Vol. 2, OUP 2003: the chapter on
sketches.  (I am in rural Wisconsin at the moment asnd don't have access to
the book.  If OUP would make its pages available to look at on Amazon I
could have told you the exact page.)

Bagchi and Wells, *Graph Based Logic and Sketches*, here:

http://arxiv.org/PS_cache/arxiv/pdf/0809/0809.3023v1.pdf

Also Kinoshita, et al 1997, referred to in GBLS.  There might be relevant
papers since 1993 mentioned in the Elephant, too.

Category people:  If you can suggest other papers that should be included,
let me know soon, and I will revise the sketches paper to include them (and
the ones I mentioned above).

Charles Wells



On Wed, May 20, 2009 at 4:23 PM, <Andre.Rodin@ens.fr> wrote:

> Dear Charles and others:
>
> this
>
> http://www.cwru.edu/artsci/math/wells/pub/pdf/sketch.pdf
>
> is your very useful overview of Sketch theory dated back to 1993. I wonder
> how
> much it omits today: are there significant research programmes in this
> field
> emerged during last 15 years? What should I look at first of all? Many
> thanks
> in advance.
>
> Andrei
>
>

Re: sketch theory

[Steve Vickers]

Dear John,

Barr & Wells "Toposes, Triples and Theories", Section 4.4, give some
examples of LE-sketches (= finite limit sketches) that includes sketches
for the theories of finite limit categories and of elementary toposes.
They don't include CCCs, but you should at least get the idea. The basic
trick (corresponding to the logical one of Freyd's "essentially
algebraic" theories) is to think of these theories as being given
algebraically with some of the operators (e.g. composition, pairing)
being partial and with domain of definition described by equations. You
then introduce those domains of definitions as nodes in the sketch, with
arrows, diagrams and cones constraining them to be finite limits in a
way that corresponds to the equations.

Incidentally, Palmgren and I recently came up with a new logical
characterization of finite limit theories, using a logic of partial
terms. It leads to a neat proof of the initial model theorem. However, I
also believe there is a specific but non-obvious advantage of sketches
over logical syntax in that sketches do not rely on having canonical
finite limits. Suppose a sketch has two distinct nodes a and b, and
manages to constrain them both to be finite limits of the same diagram.
In a model, a and b can be interpreted as different objects (though, of
course, they have to be isomorphic).

Regards,

Steve Vickers.

John Baez wrote:
> Dear Categorists -
>
> Andrei Rodin pointed out this paper by Charles Wells:
>
> http://www.cwru.edu/artsci/math/wells/pub/pdf/sketch.pdf
>
> I took a look.  In section 4.1 it mentions that people have given a finite
> limits sketch for cartesian closed categories.  I'm curious about how this
> works,  Unfortunately the list of references given here is quite long.  Can
> anyone help me find a reference on a sketch for CCC's?
>
> Best,
> jb
>
>

Re: sketch theory

[Charles Wells]

That is carried out (rather sketchily :)) on page 48 of Graph Based Logic
and Sketches by Bagchi and Wells, here:

http://arxiv.org/PS_cache/arxiv/pdf/0809/0809.3023v1.pdf

This post

http://sixwingedseraph.wordpress.com/2009/05/08/turning-definitions-into-mathematical-objects/

is the first of a projected series to explain the Bagchi-Wells paper in a
more how-to-think-about-it style.

Charles Wells



On Thu, May 21, 2009 at 2:43 PM, John Baez <john.c.baez@gmail.com> wrote:

> Dear Categorists -
>
> Andrei Rodin pointed out this paper by Charles Wells:
>
> http://www.cwru.edu/artsci/math/wells/pub/pdf/sketch.pdf
>
> I took a look.  In section 4.1 it mentions that people have given a finite
> limits sketch for cartesian closed categories.  I'm curious about how this
> works,  Unfortunately the list of references given here is quite long.  Can
> anyone help me find a reference on a sketch for CCC's?
>
> Best,
> jb
>

Re: sketch theory

[John Baez]

Dear Categorists -

Andrei Rodin pointed out this paper by Charles Wells:

http://www.cwru.edu/artsci/math/wells/pub/pdf/sketch.pdf

I took a look.  In section 4.1 it mentions that people have given a finite
limits sketch for cartesian closed categories.  I'm curious about how this
works,  Unfortunately the list of references given here is quite long.  Can
anyone help me find a reference on a sketch for CCC's?

Best,
jb

sketch theory

[Andre.Rodin]

Dear Charles and others:

this

http://www.cwru.edu/artsci/math/wells/pub/pdf/sketch.pdf

is your very useful overview of Sketch theory dated back to 1993. I wonder how
much it omits today: are there significant research programmes in this field
emerged during last 15 years? What should I look at first of all? Many thanks
in advance.

Andrei