Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
People around me use a concrete definition of morphisms between pro-objects via the representatives. I will sketch this later this afternoon, but it is well-known and obvious. But if one passes from
Pro−C(F,G)=limdcolimcHomC(Fc,Gd)to representatives ([sc,d])d, which are threads of germs then one notices that such a representative if written explicitly is in fact involving a choice of a function d↦cd, hence to describe the maps as threads of germs one seems to need an axiom of choice. So suppose we do not have an axiom of choice. Do we have then two non-equivalent categories of pro-objects ?
In fact I do not like the Pro-C or pro−C kind of notation from pro-object. I mean I see no point in dash here, and ProC or Pro(C) find better.
I wrote some references into pro-object and struggle with writing up the derivation of the elementary definition, using axiom of choice. Sorry, wait a bit until it is a correct version.
Here we are (this is now extended central part of pro-object where I have written the explicit description):
The objects of pro-C are diagrams F:D→C where D is a small cofiltered category. The set of morphisms between F:D→C and G:E→C is
pro-C(F,G)=lime∈Ecolimd∈DC(Fd,Ge)The limit and colimit is taken in the category of sets; we know that cofiltered limits there are “threads” and filtered colimits are germs (classes of equivalences). Thus a representative of s∈proC(F,G) is a thread whose each component is a germ:
s=(germe(s))e∈E which can be more concretely written as ([sde,e])e; thus [sde,e]∈colimd∈DC(Fd,Ge) where sde,e∈C(Fde,Ge) is some representative of the class; there is at least one de for each e; if the domain E is infinite, we seem to need an axiom of choice in general to find a function e↦de which will choose one representative in each class germe(s). Thus s is given by the following data
function e↦de
correspondence e↦sde,e∈C(Fde,Ge)
such that ([sde,e])e is a thread, i.e. for any γ:e→e′ we have an equality of classes (germs) [G(γ)∘sde,e]=[sde′,e′]. This equality holds if there is a d′ and morphisms δe:d′→de, δe′:d′→de′ such that G(γ)∘sde,e∘Fδe=sde′,e′∘Fδe′. (Usually in fact people consider the dual of D and the dual of C as filtered domains). Now if we chose a different function e↦˜de instead then, ([sde,e])e=([s˜de,e])e, hence by the definition od classes, for every e there is a d″∈D and morphisms σe:d″→de, ˜σe:d″→˜de such that s˜de,e∘F(˜σe)=sde,e∘F(σe).
Now the composition !
pro-C(F,G)=lime∈Ecolimd∈DC(Fd,Ge)Seek for a map
limb∈Bcolima∈EC(Ga,Hb)×lime∈Ecolimd∈DC(Fd,Ge)→limb∈Bcolimd∈DC(Fd,Hb)It is easy to write it down in terms of germs and threads, but now I look to see it from general nonsense point of view (I mean first principles), before writing it up into the entry.
In the absence of AC I would just use an entire relation instead of a function.
Thanks, Mike, I will think about your advice!
Continuing old story … just for the record.
In terms of threads and germs (just for the record): s∈proC(F,G), t∈proC(G,H) is are given by functions e↦de, b↦ab, and representatives ([sde,e])e, ([tab,b])b where sde,e∈C(Fde,e) and tab,b∈C(Gab,Hb). We need another function b↦db and ([(t∘s)db,b)b and this is clearly the composition b↦ab↦dab. Furthermore,
(t∘s)dab,b=sdab,ab∘tab,b.Now one needs to show that this is well defined and that indeed it defines a thread of germs, more precisely a well defined element
([sdab,ab∘tab,b])b∈limb∈Bcolimd∈DC(Fd,Hb).There are two things to check: first that one indeed has a thread (compatibility relation for all morphisms b→b′), and then that the definition does not depend on various choices.
1 to 7 of 7