Dirk Thierbach:

> Followup-exercise, if you're still interested: Show the same
> for products. That is, if P is a product for A and B, and P' is also
> a product for A and B, then P and P' must be isomorphic. 

and:

> Assuming you
> mean by "mediating arrows" the isomorphisms between P and P', of
> course one goes from P to P', and one from P' to P.


A diagram:


http://www.xmission.com/~thant/cat_theory_exercise_1.pdf

Figure 1 shows <f,g> : P -> P' such that P' is AxB.

Figure 2 shows <f',g'> : P' -> P such that P is AxB.

We know that:

PiA o <f,g> = f

and

PiA' o <f',g'> = f'


Figure 3 just overlays the two previous diagram such that:

f  = PiA'
f' = PiA
g  = PiB'
g' = PiB

But I don't see why I'm allowed to assume e.g. that f = PiA', and worse, 
even if I am, I still don't see why this shows that <f,g> and <f',g'> 
form an isomorphism between P and P'. We know that by definition <f,g> 
and <f',g'> are unique, but that alone doesn't prove they form an 
isomorphism, right?

Do I now at least understand the problem?

-thant

Thant Tessman wrote:

[...]

> Figure 3 just overlays the two previous diagram such that:
> 
> f  = PiA'
> f' = PiA
> g  = PiB'
> g' = PiB
> 
> But I don't see why I'm allowed to assume e.g. that f = PiA'

Actually, rereading Pierce's definition of product, I think I'm allowed 
to simply assert it. The only thing that matters is that we know they 
exist, which we do by the definition of product and the problem statement.

Thinking...

-thant

Thant Tessman wrote:
> 
> Dirk Thierbach:
> 
>> Followup-exercise, if you're still interested: Show the same
>> for products. That is, if P is a product for A and B, and P' is also
>> a product for A and B, then P and P' must be isomorphic. 
> 
> and:
> 
>> Assuming you
>> mean by "mediating arrows" the isomorphisms between P and P', of
>> course one goes from P to P', and one from P' to P.
> 
> 
> A diagram:
> 
> 
> http://www.xmission.com/~thant/cat_theory_exercise_1.pdf
> 
> Figure 1 shows <f,g> : P -> P' such that P' is AxB.
> 
> Figure 2 shows <f',g'> : P' -> P such that P is AxB.
> 
> We know that:
> 
> PiA o <f,g> = f
> 
> and
> 
> PiA' o <f',g'> = f'
> 
> 
> Figure 3 just overlays the two previous diagram such that:
> 
> f  = PiA'
> f' = PiA
> g  = PiB'
> g' = PiB
> 
> But I don't see why I'm allowed to assume e.g. that f = PiA'

Ah, but if I'm allowed to do this, then:

	f' o <f,g> = f

and

	f o <f',g'> = f'

Substituting:

	f o <f',g'> o <f,g> = f

which means

	<f',g'> o <f,g> = idendity for P

Substitute the other way, and we get the identity for P'.

Therefore <f',g'> and <f,g> form an isomorphism between P and P'.

Right?

-thant

Thant Tessman <adm@standarddeviance.com> wrote:
> Thant Tessman wrote:

>> http://www.xmission.com/~thant/cat_theory_exercise_1.pdf

I'm reading offline, so I just ignored that :-)

>> Figure 1 shows <f,g> : P -> P' such that P' is AxB.
>> Figure 2 shows <f',g'> : P' -> P such that P is AxB.
>> 
>> We know that:
>> 
>> PiA o <f,g> = f
>> 
>> and
>> 
>> PiA' o <f',g'> = f'
>> 
>> 
>> Figure 3 just overlays the two previous diagram such that:
>> 
>> f  = PiA'
>> f' = PiA
>> g  = PiB'
>> g' = PiB
>> 
>> But I don't see why I'm allowed to assume e.g. that f = PiA'

> Actually, rereading Pierce's definition of product, I think I'm allowed
> to simply assert it. The only thing that matters is that we know they
> exist, which we do by the definition of product and the problem statement.

Yes (assuming you have the diagram right). The definition of the product
says that we have (a) objects A and B; (b) the product P and projections
onto A and B; and (c) given any object X and morphisms f : X -> A, 
g : X -> B; then (d) there exists a unique arrow X -> P that makes the
diagram commute. So given (a) and (b), you can just choose anything
for (c) you want.

It's actually easier if you just write \pi_A for f' etc. 

> Ah, but if I'm allowed to do this, then:
> 
>        f' o <f,g> = f
> 
> and
> 
>        f o <f',g'> = f'
> 
> Substituting:
> 
>        f o <f',g'> o <f,g> = f
> 
> which means
> 
>        <f',g'> o <f,g> = idendity for P

The last step can also be written "if f o h = f o id, then h = id" for
h = <f',g'> o <f,g>. You can only do that if you know that f (or
rather, \pi_A') is an epimorphism. I am actually not sure if that is
always the case (though it might), so if it is not proved in any of your
books, you still have to show that. Or you can also prove directly
that <f',g'> and <f,g> compose to the identity, using the same trick
as for initial objects.

- Dirk

Dirk Thierbach wrote:
> Thant Tessman <adm@standarddeviance.com> wrote:

[...]

>> Ah, but if I'm allowed to do this, then:
>>
>>        f' o <f,g> = f
>>
>> and
>>
>>        f o <f',g'> = f'
>>
>> Substituting:
>>
>>        f o <f',g'> o <f,g> = f
>>
>> which means
>>
>>        <f',g'> o <f,g> = idendity for P
> 
> The last step can also be written "if f o h = f o id, then h = id" for
> h = <f',g'> o <f,g>. You can only do that if you know that f (or
> rather, \pi_A') is an epimorphism. 

If the problem is that I've only shown 'id-ness' in one direction, is 
there something about the fact that we could go both ways that would 
save me? That is, we also have:

	f' o <f,g> o <f',g'> = f'

So we really have:

	<f,g> o <f',g'> = id for P'

and

	<f',g'> o <f,g> = id for P


Actually, the reason *I* was uncomfortable with that last step was that 
I only showed 'id-ness' with respect to f. It's not clear to me that f 
is *any* arrow P -> A. (In my diagram, I think I labeled P and P' 
backwards from your intuition.) It's just the one we chose to satisfy 
our criteria for product. There's nothing in the definition of product 
that tells me there can't be other arrows P -> A that have nothing to do 
with what Pierce calls the 'mediating arrow.'

This is definitely something I'm not clear on with respect to this example.

-thant

Thant Tessman <adm@standarddeviance.com> wrote:
> Dirk Thierbach wrote:

>> The last step can also be written "if f o h = f o id, then h = id" for
>> h = <f',g'> o <f,g>. You can only do that if you know that f (or
>> rather, \pi_A') is an epimorphism. 

Sorry, I didn't think. You of course need f to be a *monomorphism* here,
and that's just plain not the case.

> If the problem is that I've only shown 'id-ness' in one direction, is 
> there something about the fact that we could go both ways that would 
> save me? 

The problem is that you haven't shown "id-ness" at all :-) And not,
the other variants of this by themselves don't help.

> Actually, the reason *I* was uncomfortable with that last step was that 
> I only showed 'id-ness' with respect to f. 

Yes, and you cannot show equality "with respect to" some other
function. Example for real-valued functions: Take h(x) = -x, and
f(x) = x^2. Then f o h = f o id, but nevertheless h /= id. Just doesn't
work.

> This is definitely something I'm not clear on with respect to this example.

Which trick did you use for the initial objects to show that the 
functions you defined to compose to the identity?

- Dirk

Dirk Thierbach wrote:
> Thant Tessman <adm@standarddeviance.com> wrote:

[...]

>> Actually, the reason *I* was uncomfortable with that last step was that 
>> I only showed 'id-ness' with respect to f. 
> 
> Yes, and you cannot show equality "with respect to" some other
> function. Example for real-valued functions: Take h(x) = -x, and
> f(x) = x^2. Then f o h = f o id, but nevertheless h /= id. Just doesn't
> work.

Yeah, I understood that. I'd have to show for *every* f

	f o <f',g'> o <f,g> = f

and for *every* f'

	f' o <f,g> o <f',g'> = f'

Then I'd have it, right?


> Which trick did you use for the initial objects to show that the 
> functions you defined to compose to the identity?

In the initial objects case I knew there was only one self arrow which 
by the definition of groups had to be the identity arrow. This meant 
that if two arrows composed to form a self arrow for an initial object, 
it had to be the identity arrow.

I'm not sure I see the parallel to this situation. I know by the 
definition of product that <f,g> and <f',g'> are unique. I don't see how 
this by itself guarantees that their composition forms the identity arrow.

-thant