Theorem. Maximality of the strict downset among proper sieves

Call a direct structure reflecting when every morphism between objects of equal degree is a split epimorphism. In a reflecting direct category, every non-invertible-in-degree morphism strictly raises degree, and the strict downset is as large as a proper sieve can be:

If the direct structure is reflecting, then every proper sieve 𝑆 on π‘₯ refines into the strict downset:

π‘†βŠ†π–²π—π—‹π—‚π–Όπ—π–£π—ˆπ—π—‡(π‘₯).

Suppose π‘“βˆˆπ‘† with 𝑓:𝑦→π‘₯ of equal degree. By reflection 𝑓 has a section 𝑠, and closure under precomposition gives 𝑠⋆𝑓=𝗂𝖽π‘₯βˆˆπ‘†, contradicting properness.

So every morphism in 𝑆 strictly raises degree. That is, every morphism in 𝑆 is also a member of π–²π—π—‹π—‚π–Όπ—π–£π—ˆπ—π—‡(π‘₯).

strict-downset-maximal theorem entries/category/strict-downset-maximal.hel