nLab
presentation axiom

Contents

Idea

In the foundations of mathematics, it's interesting to consider the axiom that the Category of Sets Has Enough Projectives; in short: CoSHEP (pronounced /ko:-shep/). This is more commonly known as the presentation axiom: PAx. It is a weak form of the axiom of choice.

Statement

In elementary terms, CoSHEP states

Axiom (CoSHEP)

For every set AA, there exists a set PP and a surjection PAP \to A, such that every surjection XPX \twoheadrightarrow P has a section.

Remark

The full axiom of choice states that every surjection XAX \to A has a section; hence in the above PP may be chosen to be AA itself.

This should be read in view of the definition of projective objects:

Definition

An object PP in a category CC is (externally) projective iff the hom-functor C(P,):CSetC(P, -): C \to Set takes epis to epis. This is the same as saying: given an epi p:BAp: B \to A and a map f:PAf: P \to A, there exists a lift g:PBg: P \to B in the sense that f=pgf = p \circ g.

Accordingly, in a topos the CoSHEP axiom says equivalently

Axiom (CoSHEP)

Every object has a projective presentation. Hence: There are enough projectives.

Borrowing from the philosophy of constructivism, we may also call this a complete presentation.

Remark

The dual axiom, that SetSet has enough injectives (that is, every set admits an [injection into an injective set) is true in every topos: every power object is an injective object, and every object embeds in its power object via the singleton map .]

Justification

Although perhaps not well known in the literature of constructive mathematics, the CoSHEP axiom may be justified by the sort of reasoning usually accepted to justify the axioms of countable choice and dependent choice (which it implies, by Proposition 1 below).

To be explicit, every set AA should have a ‘completely presented’ set of ‘canonical’ elements, that is elements given directly as they are constructed without regard for the equality relation imposed upon them. For canonical elements, equality is identity, so the BHK interpretation of logic justifies the axiom of choice for a completely presented set. This set is PP, and AA is obtained from it as a quotient by the relation of equality on AA. This argument can be made precise in many forms of type theory (including those of Martin-Löf and Thierry Coquand), which thus justify CoSHEP, much as they are widely known to justify dependent choice.

Consequences

The existence of sufficiently many projective presentations plays a central role in homological algebra as a means to construct projective resolutions of objects. Tradtionally one often uses the axiom of choice to prove that categories of modules have enough projectives, on the grounds that the free modules are projective.

But the weaker assumption of CoSHEP is already sufficient for this purpose: while not every free module will be projective, one can still use CoSHEP to find a projective presentation for every free module (and thus for every module). This is discussed in more detail here.

Proposition

The following three conditions on a W-pretopos with enough projectives are equivalent:

  1. The axiom of dependent choice (DC),

  2. The axiom of countable choice (CC),

  3. Projectivity of the singleton (the terminal object) 11.

Note that we normally assume (3) for the category of sets, which is true in any (constructively) well-pointed pretopos and true internally in any pretopos whatsoever, so one normally says that DC and CC simply follow from the existence of enough projectives (CoSHEP). Equivalently, internal DC and internal CC follow from internal CoSHEP.

Proof

Condition 1 easily implies 2. Condition 2 says precisely that the natural numbers object \mathbb{N} is externally projective, and since 11 is a retract of \mathbb{N}, it is projective under condition 2, so 2 implies 3. It remains to show 3 implies 1.

Let XX be inhabited, so there exists an entire relation given by a jointly monic span

1epiUfX,1 \stackrel{epi}{\leftarrow} U \stackrel{f}{\to} X,

and similarly let

Xepiπ 1Rπ 2XX \stackrel{epi \pi_1}{\leftarrow} R \stackrel{\pi_2}{\to} X

be an entire binary relation. Let p:PXp: P \to X be a projective cover. Since 11 is assumed projective, the cover U1U \to 1 admits a section σ:1U\sigma: 1 \to U, and the element fσ:1Xf \sigma: 1 \to X lifts through pp to an element x 0:1Px_0: 1 \to P. Next, in the diagram below, pp lifts through the epi π 1\pi_1 to a map q:PRq: P \to R, and then π 2q\pi_2 q lifts through pp to a map ϕ\phi (since PP is projective):

P ϕ P p q p X π 1 R π 2 X\array{ & & P & \stackrel{\phi}{\to} & P \\ & \swarrow p & \downarrow q & & \downarrow p \\ X & \underset{\pi_1}{\leftarrow} & R & \underset{\pi_2}{\to} & X }

By the universal property of \mathbb{N} (see recursion), there exists a unique map h:Ph: \mathbb{N} \to P rendering commutative the diagram

1 0 s id h h 1 x 0 P ϕ P p q p X π 1 R π 2 X\array{ 1 & \stackrel{0}{\to} & \mathbb{N} & \stackrel{s}{\to} & \mathbb{N} \\ id \downarrow & & \downarrow h & & \downarrow h \\ 1 & \underset{x_0}{\to} & P & \underset{\phi}{\to} & P \\ & \swarrow p & \downarrow q & & \downarrow p \\ X & \underset{\pi_1}{\leftarrow} & R & \underset{\pi_2}{\to} & X }

Clearly ph,phs:X×X\langle p h, p h s \rangle : \mathbb{N} \to X \times X factors through π 1,π 2:RX×X\langle \pi_1, \pi_2 \rangle : R \to X \times X, i.e., n:(ph(n),ph(n+1))R\forall_{n: \mathbb{N}} (p h(n), p h(n+1)) \in R, thus proving that dependent choice holds under CoSHEP.

Example

A topos in which CoSHEP holds but 11 is not projective is Set CSet^C, where CC is the category with three objects and exactly two non-identity arrows abca \to b \leftarrow c. For if U:CSetU: C \to Set is a functor with U(a)={a 0}U(a) = \{a_0\}, U(b)={b 0,b 1}U(b) = \{b_0, b_1\}, and U(c)={c 0}U(c) = \{c_0\}, with U(ab)(a 0)=b 0U(a \to b)(a_0) = b_0 and U(cb)(c 0)=b 1U(c \to b)(c_0) = b_1, then the map U1U \to 1 is epi but has no section, so 11 is not projective. On the other hand, as noted below, every presheaf topos satisfies CoSHEP, assuming that SetSet itself does.

CoSHEP also implies several weaker forms of choice, such as the axiom of multiple choice and WISC. In weakly predicative mathematics, it can be combined with the existence of function sets to show the subset collection axiom.

In a topos

When working in the internal logic of a topos, the “internal” meaning of CoSHEP is “every object is covered by an internally projective object.” (Compare with the internal axiom of choice: every object is internally projective.) As regards foundational axioms for toposes (in the sort of sense that the axiom of choice is regarded as “foundational”), the internal version of the presentation axiom should be taken as the default version.

Proposition

Suppose that 11 is (externally) projective in EE. Then EE satisfies PAx whenever it satisfies internal PAx.

Internal PAx does not follows from external PAx; see Example 3. However, if every object is projective (AC), then every object is internally projective (IAC).

A stronger version of PAx may be worth considering. Say that an object is stably projective if its pullback to any slice category is projective. Then stably projective objects are internally projective (proof?). Similarly, if we say that a topos EE satisfies stable PAx if every object is covered by a stably projective object, then a topos satisfies internal PAx if it satisfies stable PAx.

Example

Every presheaf topos Set C opSet^{C^{op}} has enough projectives, since any coproduct of representables is projective. If in addition CC has binary products, then by this result, Set C opSet^{C^{op}} validates internal PAx.

Counterexample

However, not every presheaf topos validates internal PAx, even though every presheaf topos validates external PAx. As an example, let CC be the category where Ob(C)Ob(C) is the disjoint sum {a,b}\mathbb{N} \cup \{a, b\}, and preordered by taking the reflexive transitive closure of relations nn+1n \leq n+1, nan \leq a, nbn \leq b. The claim is that neither C(,a)C(-, a), nor any presheaf PP that maps epimorphically onto C(,a)C(-, a), can be internally projective. Indeed, consider the presheaf FF defined by F(a)=F(b)=F(a) = F(b) = \emptyset and F(n)=[n,)F(n) = [n,\infty), with F(n+1n)F(n+1 \to n) the evident inclusion. Let GG be the support of FF, so that we have an epi e:FGe \colon F \to G. Then it may be shown that for any PP covering C(,a)C(-, a), the set F P(b)F^P(b) is empty and the set G P(b)G^P(b) is nonempty, so that the map e P:F PG Pe^P \colon F^P \to G^P cannot be epic.

Counterexample

Any topos that violates countable choice, of which there are plenty, must also violate internal PAx.

Example

An interesting example of a topos that has enough projectives and satisfies internal CoSHEP (at least, assuming the axiom of choice in Set), although it violates the full (internal) axiom of choice, is the effective topos, and more generally any realizability topos. The reason for this is quite similar to the intuitive justification for CoSHEP given above. Technically, it results from the fact that realizability toposes are exact completions; an explanation is given in this remark.

Further properties

Since Set is (essentially regardless of foundations) an exact category, if it has enough projectives then it must be the free exact category PSet ex/lexPSet_{ex/lex} generated by its subcategory PSetPSet of projective objects. By the construction of the ex/lex completion PSet ex/lexPSet_{ex/lex}, it follows that every set is the quotient of some “pseudo-equivalence relation” in PSetPSet; i.e., the result of imposing an equality relation on some completely presented set. See SEAR+ε for an application of this idea.

Proposition

CoSHEP as a choice principle added to ZF implies a proper class of regular cardinals.

Proof

Since CoSHEP implies WISC, and WISC has this implication (a result of van den Berg).

References

When Peter Aczel was developing CZFCZF (a constructive predicative version of ZFC), he considered this axiom, under the name of the presentation axiom, but ultimately rejected it.

  • Peter Aczel. The type theoretic interpretation of constructive set theory. Logic Colloquium ‘77 (Proc. Conf., Wroclaw, 1977), pp. 55–66, Stud. Logic Foundations Math., 96, North-Holland, Amsterdam-New York, 1978. Cited in Palmgren, below.

The presentation axiom was, however, adopted by Erik Palmgren in CETCSCETCS (a constructive predicative version of ETCS):

  • Erik Palmgren. Constructivist and Structuralist Foundations: Bishop’s and Lawvere’s Theories of Sets. pdf.

Its relationship to some other weak axioms of choice is studied in

  • Michael Rathjen. Choice principles in constructive and classical set theories.

Revised on August 31, 2014 22:01:01 by David Roberts (129.127.211.139)