Re: Finite product structure.

From: Kindle (kidanei_at_yahoo.com)
Date: 01/18/05 

Date: 18 Jan 2005 08:06:07 -0800

Many thanks for the welll thought out help.

> "let FB is another category made by throwing all the finite
> product of 1" is presumably referring to a syntactic construction
> of the "free category-with-finite-products generated by 1", and
> it is easier to prove what you want by showing that FinSet^{op}
> satisfies the universal property implied by this freeness.

I'm a little bit confused by the definition of the freeness here. Is
this correct to go about it.

Let F: Cat ---> Cat , be a product preserving functor. Conceretely,
it sends X to FX a free category generated by X. So We claim
FinSet^{op} is given by F1.

The freeness condition says;

P: 1 ------> UF1 is universal i.e for any other map q: 1-----> UC
there is a unique map !: F1 ---> C. (with my poor understanding, it
seems to say that F has right adjoint?).

Alternatively, for a given small category C we have via yoneda full
and faith full embeding into [C^op, Set], and exponentials in functor
category (presheafs) are given by yoneda as:

(C)1 \cong Nat{y(1), C}, where y(1) is FinSet^{op}.

Does this make sense?

Thanks again,

>
> In other words, let C be any category with finite products; you
> want to show that the functor which evaluates at the 1-element
> set,
>
> ev_1: Prod(FinSet^{op}, C) --> C,
>
> is an equivalence; here Prod(FinSet^{op}, C) denotes the
> category of product-preserving functors and natural transformations
> between them. In other words, that any object of C is isormorphic
> to one of the form ev_1(F), and that ev_1 is full and faithful.
>
> Given c in C, take F_c to be the functor which sends an n-element
> set to c^n (n-fold product). Then show that given F, G in
> Prod(FinSet^{op}, C), any arrow f: F(1) --> G(1) in C comes
> from a uniquely determined transformation F --> G. (Use the
> universal property of products to show that the component
> F(n) --> G(n) must be of the form f^n: F(1)^n --> G(1)^n.)
>
> Todd Trimble

Quantcast