Re: Goldblatt, /Topoi/: definition of exponentiation

On Oct 30, 1:19 pm, Angus Rodgers <twir...@xxxxxxxxxxx> wrote:
On Thu, 30 Oct 2008 20:01:54 +0000, I wrote:
On Thu, 30 Oct 2008 08:44:26 -0700 (PDT),
anonymous.rubbert...@xxxxxxxxx wrote:

So it is
unlikely to cause problems if you write A\times B for a product of
objects A and B in some category, as any other product of A and B will
also be equipped with a unique isomorphism to A\times B. You can even
go further: this isomorphism is "functorial" in the sense that it will
commute with maps of products given by varying A or B.

I must admit that at first I gratuitously misunderstood this
statement, and wasted some time trying to prove it false! My loss
(and fixing my foolish mistake has given me some useful practice
in diagram-chasing, so it has been a gain as well).

More seriously, though, it doesn't address my question, which was as
to the existence of operations like \times - which seem magically
to choose a product for every pair of objects - rather than their
uniqueness up to natural isomorphism.

I'm sorry - I seem to have misunderstood your point on more than
one level! I think your answer does address my question. Choose
any operation \times (using the axiom of choice, or whatever other
foundational magic seems appropriate), and it doesn't matter which
choice one makes, because, as you said, and as I eventually had to
accept, all such choices are naturally isomorphic.

All will be well so long as no subsequent definition (such as that
of exponentiation) depends on any property of one's chosen \times
that isn't possessed by every other bifunctor naturally isomorphic
to it. This means a bit more work, which I haven't done yet, but
I don't have any serious doubt that it will turn out to be true.

(I may not have expressed this very precisely, but in loose terms,
I mean that if a choice of b^a and ev: b^a x a -> b for every a, b
"works" with \times, then it must "work" with every other choice of
an object a * b for every a, b, with projection arrows satisfying
the same universal property. I suppose this does have to be checked
explicitly for every such new definition - or is there some sort of
general guarantee that renders such detailed checking unnecessary?)

i had some of the same concerns when i first studied this

it starts to clear when you start understand
the operational nature of the category language

things that are just assumed identical
in extensional theories like set theory
are usually named separately first in a category
and then proven isomorphic

(this was actually one of plotkin's starting grounds
in his formalisations of operational semantics
and is implicit in the scott-strachey approach
to denotational semantics)

once isomorphism has been proven
though
the objects have identical properties throughout
and are mutually substitutible

it can be disorienting at first
since there are often many different definitions
which eventually through diagram chasing can be shown equivalent

to simplify things
one can always work in a skeletal category
but this tends to obscure the operational approach

they key is how to prove isomorphisms here

that is what these universal constructions provide

universal constructions are ways to develop operationally
what set theory provides in it's quantification
and is the biggest source of isomorphism proving through diagram
chasing

(when category theory is being used descriptively
on mathematical structures analysed through a different language
- like is common to see for the category Set as an example
then isomorphisms can be proved in the other language too
but universal constructions are the main method inside)

so
when you are looking at a product in category
you are basically looking at _the_ product
and similarly with other constructs

as others have pointed out
if they may be performed on every object
universal constructions are functorial

this is the step that makes all of it rigorous
and it is the step that makes the functorial equivalence you are
looking for
between a category and it's skeleton
and is why operational semantics can be done consistently

-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-
galathaea: prankster, fablist, magician, liar
.

Relevant Pages

  • Re: What is the 1st order formal system known as PA?
    ... > about structures within set theory. ... > complete ordered fields, there exists an isomorphism of ordered fields ... > at the object level and Z1 is first order set theory at the meta-level. ...
    (sci.logic)
  • Re: What is the 1st order formal system known as PA?
    ... >> language from set theory but with all its predicates and operation ... >> symbols definable in set theory. ... >> that theory to see how they fare for isomorphism and homomorphism. ... They weren't intended to work in the sense of preserving isomorphism, ...
    (sci.logic)
  • Re: Value (was: Mixing OO and DB)
    ... Lately I am viewing things through the lens of set theory. ... by definition a type must be unique up to isomorphism, ... classes in order to account for this concept of uniqueness up ... equivalence class). ...
    (comp.databases.theory)