Local lifting properties

For various reasons (one of which was adumbrated in my previous post), I have been thinking about generalising the classical notion of ‘weak factorisation system’ to work better in the intuitionistic context.

The difficulty, really, is in how we understand existence. Let us consider a pair of morphisms, say f : AB and g : CD, in an elementary topos 𝒮. What does it mean to say that f has the left lifting property with respect to g in the internal logic of 𝒮? That is, suppose when given morphisms h : AC, k : BD, if

  • for all a in A, k(f(a)) = g(h(a)),

then there exists a morphism : BC such that

  • for all a in A, (f(a)) = h(a); and
  • for all b in B, g((b)) = k(b).

Interpreted naïvely, this says that f has the left lifting property with respect to g in the ordinary sense. Nonetheless, in the internal logic of 𝒮, the above is true when f is the unique morphism 0 → 1 and g is any epimorphism CD – exactly as in the archetypical topos Set. On the other hand, it is simply not true that epimorphisms induce surjections of global sections! What the above really says is the following: a lifting exists – after base change along an epimorphism!

In light of the preceding discussion, and also bearing in mind the work of Brown, Jardine, Joyal et al. on the homotopy theory of sheaves of simplicial sets, it would appear that the right definition of left/right lifting property in the relative context must be local, in the sense of the following definition.

Definition. Let 𝒮 be a regular category, let ℂ be an 𝒮-indexed category, let J be an object in 𝒮, and let 𝒞J be the fibre of ℂ over J. Given morphisms f and g in 𝒞J, we say f has the local left lifting property with respect to g if, for all morphisms x : IJ in 𝒮 and all morphisms h and k in 𝒞I such that kx*f = x*gh, there exist a regular epimorphism e : EI and a morphism in 𝒞E such that e*x*f = e*h and e*x*g = e*k.

It is easy to verify that the class of morphisms in 𝒞J that have the local left lifting property with respect to g is closed under composition and retracts. It is also closed under finite coproducts and pushouts, provided we restrict attention to those colimits that are stable under reindexing. The distinguishing feature is the descent property: if x : IJ is any regular epimorphism in 𝒮 and f is a morphism in 𝒞J, then f has the local left lifting property with respect to g if and only if x*f has the local left lifting property with respect to x*g.

Whether or not the class is closed under transfinite composition and 𝒮-indexed coproducts seems rather more tricky. If our metatheory has the axiom of choice, then the class is indeed closed under reindexing-stable transfinite composition; the same can be said for reindexing-stable infinite coproducts. It should therefore be unsurprising that there is a connection between the internal axiom of choice in 𝒮 and the question of whether or not the class is closed under 𝒮-indexed coproducts.

Indeed, suppose 𝒮 is an elementary topos, and consider the self-indexing of 𝒮. We earlier observed that 0 → 1 has the local left lifting property with respect to epimorphisms. Thus, if the class of morphisms with the local left lifting property with respect to epimorphisms is closed under 𝒮-indexed coproducts, then an epimorphism g : CD must have the local right lifting property with respect to the unique morphism 0 → D; but this happens if and only if the morphism [D, g] : [D, C] → [D, D] is an epimorphism, i.e. if and only if g : CD has a section in the internal logic of 𝒮.

So, should we accept the definition of ‘local lifting property’ proposed above, and with it, the failure of the basic saturation properties of classes of morphisms with a left/right lifting property? Or should we continue searching for a definition that allows us to carry over more of the classical theory?

Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s