nLab
Freyd cover

Idea

The Freyd cover of a category is a special case of Artin gluing. Given a category $𝒯$ and a functor $F:𝒯\to \mathrm{Set}$, the Artin gluing of $F$ is the comma category $\mathrm{Set}\downarrow F$ whose objects are triples $(X,\xi ,U)$ where:

• $X$ is a set
• $U$ is an object of $𝒯$
• $\xi$ is a function $X\to F(U)$.

The Freyd cover is the special case $F=𝒯(1,-)$.

The Freyd cover is sometimes known as the Sierpinski cone or scone, because in topos theory it behaves similarly to the cone on a space, but with the interval $[0,1]$ replaced by the Sierpinski space.

Properties

Relation to the initial topos

One of the first applications of the Freyd cover was to deduce facts about the initial topos? (initial with respect to logical morphisms — also called the free topos). They were originally proved by syntactic means; the conceptual proofs of the lemma and theorem below are due to Freyd.

Lemma

For any category $C$ with a terminal object $1$, the terminal object of the Freyd cover $\hat{C}$ is connected and projective, i.e., the representable $\Gamma =\hat{C}(1,-):\hat{C}\to \mathrm{Set}$ preserves any colimits that exist.

Proof

To check that ${\Gamma }^{\mathrm{op}}:{\hat{C}}^{\mathrm{op}}\to {\mathrm{Set}}^{\mathrm{op}}$ preserves limits, it suffices to check that the composite

$${\hat{C}}^{\mathrm{op}}\stackrel{{\Gamma }^{\mathrm{op}}}{\to }{\mathrm{Set}}^{\mathrm{op}}\stackrel{2^{-}}{\to }\mathrm{Set}$$\widehat{C}^{op} \stackrel{\Gamma^{op}}{\to} Set^{op} \stackrel{2^-}{\to} Set

preserves limits, because the contravariant power set functor $P=2^{-}$ is monadic. But it is easily checked that this composite is the contravariant representable given by $(2,1,2\to \Gamma (1))$.

Theorem

The terminal object in the initial topos $𝒯$ is connected and projective, i.e., $\Gamma =\mathrm{hom}(1,-):𝒯\to \mathrm{Set}$ preserves finite colimits.

Proof

We divide the argument into three segments:

• The hom-functor preserves finite limits, so by general properties of Artin gluing, the Freyd cover $\widehat{𝒯}$ is also a topos. Observe that $𝒯$ is equivalent to the slice $\widehat{𝒯}/M$ where $M$ is the object $(\varnothing ,1,\varnothing \to \Gamma (1))$. Since pulling back to a slice is a logical functor, we have a logical functor

  $$\pi :\widehat{𝒯}\to 𝒯$$\pi \colon \widehat{\mathcal{T}} \to \mathcal{T}

  Since $𝒯$ is initial, $\pi$ is a retraction for the unique logical functor $i:𝒯\to \widehat{𝒯}$.

• We have maps $𝒯(1,-)\to \widehat{𝒯}(i1,i-)\cong \widehat{𝒯}(1,i-)$ (the isomorphism comes from $i1\cong 1$, which is clear since $i$ is logical), and $\widehat{𝒯}(1,i-)\to 𝒯(\pi 1,\pi i-)\cong 𝒯(1,-)$ since $\pi$ is logical and retracts $i$. Their composite must be the identity on $𝒯(1,-)$, because there is only one such endomorphism, using the Yoneda lemma and terminality of $1$.

Finally, since $𝒯(1,-)$ is a retract of a functor $\widehat{𝒯}(1,i-)$ that preserves finite colimits (by the lemma, and the fact that the logical functor $i$ preserves finite colimits), it must also preserve finite colimits.

This is important because it implies that the internal logic of the free topos (which is exactly “intuitionistic higher-order logic”) satisfies the following properties:

• The disjunction property: if “P or Q” is provable in the empty context, then either P is so provable, or Q is so provable. (Note that this clearly fails in the presence of excluded middle.)

• The existence property: if “there exists an $x\in A$ such that $P(x)$” is provable in the empty context, then there exists a global element $x:1\to A$ such that $P(x)$ is provable in the empty context. (Again, this is clearly a constructivity property.)

• The negation property: False is not provable in the empty context.

As a local topos

The Freyd cover of a topos is a local topos, and in fact freely so. Every local topos is a retract of a Freyd cover.

See (Johnstone, lemma C3.6.4).

References

You can find more on Artin gluing in this important (and nice) paper:

• Aurelio Carboni, Peter Johnstone, Connected limits, familial representability and Artin glueing , Mathematical Structures in Computer Science 5 (1995), 441–459

plus

• Aurelio Carboni, Peter Johnstone, Corrigenda to ‘Connected limits…’ , Mathematical Structures in Computer Science 14 (2004), 185–187.

See also section C3.6 of

• Peter Johnstone, Sketches of an Elephant

Some of the above material is taken from

• Tom Leinster, reply at MathOverflow

The argument given above for properties of the free topos is an amplification of

• Freyd and Scedrov, Categories, Allegories, 1.(10)31 (page 192)