universal set bundle

[marcbezem]

I'm working on 3.3, Set bundles. I find it difficult to follow the motivation of of the concept of universal set bundle, as it seems only to apply to f : A -> B with B a groupoid. What about the following presentation?

First, we remark that an injection f : A -> B can be called a proposition bundle. Moreover, if B is a set and A is connected, then A is contractible. The proof of this uses that each ap_f is an equivalence.

Second, we show that if f : A -> B is a set bundle, B is a groupoid, and A is simply connected (definition should be added), then A is again contractible. The proof uses that each ap_f : (a = a') -> (f(a) = f(a')) is a proposition bundle, with co-domain (f(a) = f(a')) a set and domain (a=a') connected.

I haven't checked the details, and they go certainly beyond 3.3, but I can imagine that this generalizes to: if f : A -> B is an n-type bundle, B is an (n+1)-type, and A is n-connected, then (conjecture) A is contractible. In the above cases, n=-1 and n=0.

Within the limited context of 3.3, two more questions arise:

1. Why defining "universal set bundle" for any type B instead of only for B a groupoid?
2. Why not defining it with A contractible instead of deriving that from a weaker condition in the case of 1?

[bidundas]

On Jul 24, 2023, at 16:15, Marc Bezem @.***> wrote:

I'm working on 3.3, Set bundles. I find it difficult to follow the motivation of of the concept of universal set bundle, as it seems only to apply to f : A -> B with B a groupoid. What about the following presentation?

First, we remark that an injection f : A -> B can be called a proposition bundle. Moreover, if B is a set and A is connected, then A is contractible. The proof of this uses that each ap_f is an equivalence.

Second, we show that if f : A -> B is a set bundle, B is a groupoid, and A is simply connected (definition should be added), then A is again contractible. The proof uses that each ap_f : (a = a') -> (f(a) = f(a')) is a proposition bundle, with co-domain (f(a) = f(a')) a set and domain (a=a') connected.

I haven't checked the details, and they go certainly beyond 3.3, but I can imagine that this generalizes to: if f : A -> B is an n-type bundle, B is an (n+1)-type, and A is n-connected, then (conjecture) A is contractible. In the above cases, n=-1 and n=0.

It is certainly true that if you have a fibration f:A->B where \pi_i of all fibers vanish for i>n-1, then for j>n-1 \pi_jB=0=> \pi_jA = 0 (and so A is contractible if, for independent reasons, \pi_jA=0 whenever \pi_jB might not be).

Within the limited context of 3.3, two more questions arise:

• Why defining "universal set bundle" for any type B instead of only for B a groupoid? • Why not defining it with A contractible instead of deriving that from a weaker condition in the case of 1?

Whatever the universal set bundle is, it must first and foremost be a set bundle. If you insist that A shall be contractible then saying that A-> B a set bundle is the same as saying that B is a groupoid. To me it sounds weird to define universal set bundles via in a way that only applies to groupoids.

In homotopy theory, the universal covering space of a connected space B is a fibration A->B such that A is simply connected (not necessarily contractible, so for a simply connected B the identity is the universal covering).

— Reply to this email directly, view it on GitHub, or unsubscribe. You are receiving this because you are subscribed to this thread.

[UlrikBuchholtz]

I agree that the discussion at the end of Sec. 3.3 is confusing, partly because it focuses on B being a groupoid. (I may have contributed to this confusion, if so, I apologize.)

Taking a step back, to call something universal, it should have a universal property. I can see how to do that, if we require (in Def. 3.3.1) in addition that f be pointed: In that case, the universal set bundle is the initial object in pointed, connected set bundles. (It's the 0-image factorization of the base point inclusion pt : 1 -> B.)

But what's the universal property with the current definition? (In any case, we restrict to B being pointed in Def. 3.3.11.)

[bidundas]

I’m all for being pointed. Otherwise we get unwanted deck transformations ruining universality (exp:R->S^1 is no longer universal/initial in any sense since it has nontrivial automorphisms)

Bjorn

PS way back I probably also have a share in whatever inconsistencies that may be at this point. Accept my blanket apologies

On Jul 25, 2023, at 10:26, Ulrik Buchholtz @.***> wrote:

I agree that the discussion at the end of Sec. 3.3 is confusing, partly because it focuses on B being a groupoid. (I may have contributed to this confusion, if so, I apologize.)

Taking a step back, to call something universal, it should have a universal property. I can see how to do that, if we require (in Def. 3.3.1) in addition that f be pointed: In that case, the universal set bundle is the initial object in pointed, connected set bundle. (It's the 0-image factorization of the base point inclusion pt : 1 -> B.)

But what's the universal property with the current definition? (In any case, we restrict to B being pointed in Def. 3.3.11.)

— Reply to this email directly, view it on GitHub, or unsubscribe. You are receiving this because you commented.

[marcbezem]

Do we have this decreasing sequence 2-3 of subtypes, with added structure in step 4 (updated after discussion):

2. Set bundles over groupoid B
3. Universal set bundles over groupoid B (the domain A simply connected, A can be proved to be contractible, A pointed by center)
4. Universal set bundles over groupoid B pointed in b:B (a contractible type, even if B is not connected)

Let's discuss this today (= now)

[UlrikBuchholtz]

From our meeting, our preliminary decision was:

• Remove the definition of universal from Def. 3.3.1
• Add definition of universal set bundle as initial pointed set bundle right after 3.3.9/3.3.10, def:RtoS1 (adapt 3.3.11/12, def:universalcover, accordingly)
• Prove then that the exponential set bundle (pointed at 0) is universal, and that the domain of a universal set bundle over a groupoid is contractible
• Prove in Sec. 3.9 that the 0-image of the base point inclusion b : 1 -> B for a general type B is the universal set bundle over (B,b).
• Adapt Sec. 4.12.8 (perhaps separate issue for this?)

[marcbezem]

How to prove that the pointed exponential set bundle is universal without using the results from 3.4? Perhaps use 1->_*B with B a pointed groupoid as a very simple example first?

Here is why I think 3.4 is needed to prove that \sum{x:S1} R(x) is contractible. We know that \sum{x:S1} base=x is contractible. We can also construct a family f(x) of maps of type (base=x) -> R(x) by circle induction. But then tot(f) would be a map between contractible types, so an equivalence, and hence f(x) would be an equivalence for all x:S1, i.e., Thm 3.4.4.

[UlrikBuchholtz]

This is now done!