* Adjoining intedeterminates to cartesian categories
@ 1997-11-25 13:17 categories
0 siblings, 0 replies; 2+ messages in thread
From: categories @ 1997-11-25 13:17 UTC (permalink / raw)
To: categories
Date: Tue, 25 Nov 1997 10:51:06 +0000
From: Benedict R. Gaster <brg@Cs.Nott.AC.UK>
Hi,
I have a simple question concerning the adjoining of intedeterminates
to cartesian (closed) categories. Before asking the question I
describe the two results I am interested in then state my question.
It is possible to adjoin an intedeterminate arrow X: 1 -> C to a
cartesian (closed) category as follows:
Proposition 1:
If C is a cartesian (closed) category, X: 1 -> C an intedeterminate,
and I: C -> C[X] is cartesian (closed) functor, there exists a unique
cartesian functor G: C[X] -> D, such that G(X) = d and the following
diagram commutes:
I
C -------> C[X]
\ |
\ |
\ |
\ |
\ |
F \ | G
\ |
\ |
\ |
\ |
\ |
D,
where D is a cartesian category, F: C -> D is a cartesian functor, and
d: 1 -> F(C).
The proof of this proposition can be given directly or via an
alternative definition in terms of the reader comonad and the
corresponding Klesli construction (personally I find the later simply
and more intuitive). As far as I am aware these constructions were
originally given by Lambek [lam74], proofing the corresponding
deduction theorem for cartesian closed categories, and revised by
Lambek and Scott [lam&sco86].
Although the above result is well known it seems that the result of
adjoining an intedeterminate object to a cartesian closed category, in
particular it's proof, is not so well known. This result may be stated
as follows:
Proposition 2:
If C is a cartesian (closed) category, X an interterminate, and I: C
-> C[X] is a functor, there exists a unique cartesian (closed) functor
G: C[X] -> D, such that G(X) = D, and the following diagram commutes:
I
C -------> C[X]
\ |
\ |
\ |
\ |
\ |
F \ | G
\ |
\ |
\ |
\ |
\ |
D,
where D is a cartesian (closed) category, F: C -> D is a cartesian
closed functor, and D is in Obj(D).
The problem is that it is not clear how to proof Proposition 2. I
believe that it is possible to use results from the work of Kelly and
various colleagues in the field of Two-dimensional universal algebra
[back89]. However, I was hoping that there may be a more direct route
to proving this result, which does not rely on the Two-dimensional
monad theory.
My question is simply this:
Is there a more direct, and hopefully simpler, proof of Proposition 2?
Thank you for any help you can provide on this subject.
Best wishes
Ben
--------
Benedict R. Gaster.
Languages and Programming Group, University of Nottingham.
A thing of beauty is a joy forever. -- John Keats (1795--1821).
---------------------------------------------------------------------------
References:
[back89]
R. Backwell and G.M. Kelly and A.J. Power
Two-Dimensional Monad Theory
Journal of Pure and Applied Algebra
year = 1989
[lambek74]
J. Lambek
Functional Completeness of Cartesian Categories
Annals of Mathematical Logic}
1974
[lam&sco86]
J. Lambek and P. J. Scott
Introduction to higher order categorical logic
Cambridge University Press
Cambridge studies in advanced mathematics 7
1986
^ permalink raw reply [flat|nested] 2+ messages in thread
* Re: Adjoining intedeterminates to cartesian categories
@ 1997-11-25 18:18 categories
0 siblings, 0 replies; 2+ messages in thread
From: categories @ 1997-11-25 18:18 UTC (permalink / raw)
To: categories
Date: Tue, 25 Nov 1997 10:16:26 -0500 (EST)
From: Peter Freyd <pjf@saul.cis.upenn.edu>
The existence is a quick consequence of the standard adjoint functor
theorems.
^ permalink raw reply [flat|nested] 2+ messages in thread
end of thread, other threads:[~1997-11-25 18:18 UTC | newest]
Thread overview: 2+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
1997-11-25 13:17 Adjoining intedeterminates to cartesian categories categories
1997-11-25 18:18 categories
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).