nLab Freyd cover

Contents

Contents

Idea

The Freyd cover 𝒯¯\overline{\mathcal{T}} of a topos 𝒯\mathcal{T}, or more generally of a category with a terminal object, is a way to turn 𝒯\mathcal{T}, viewed as an ‘abstract’ category, into a ‘concrete’ category of structured sets by sewing it together with Set along the global section functor.

As 𝒯¯\overline{\mathcal{T}} comes equipped with two well-behaved projection functors the resulting category has many good logical properties making the construction an important tool in type theory and theoretical computer science.

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][0,1] replaced by the Sierpinski space.

Definition

Let 𝒯\mathcal{T} be a category with a terminal object and Γ=𝒯(1,)\Gamma = \mathcal{T} (1, -) the global section functor . The Freyd cover of 𝒯\mathcal{T} is the category 𝒯¯\overline{\mathcal{T}} whose objects are triples (X,ξ,U)(X, \xi, U) where:

  • XX is a set
  • UU is an object of 𝒯\mathcal{T}
  • ξ\xi is a function XΓ(U)X \to \Gamma (U)

A morphism from (X,ξ,U)(X,\xi, U) to (Y,η,V)(Y,\eta , V) is a pair of morphisms (φ:XY,t:UV)(\varphi :X\to Y, t:U\to V) with φSet\varphi\in Set and t𝒯t\in \mathcal{T} such that ηφ=Γ(t)ξ\eta\varphi=\Gamma(t)\xi.

Remark

The construction is a special case of Artin gluing: i.e. 𝒯¯\overline{\mathcal{T}} is the comma category SetΓSet \downarrow \Gamma with Γ=𝒯(1,)\Gamma = \mathcal{T} (1, -).

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 CC with a terminal object 1\mathbf{1}, the terminal object of the Freyd cover C^\widehat{C} is small-projective, i.e., the representable Γ=C^(1,):C^Set\Gamma = \widehat{C}(1, -) \colon \widehat{C} \to Set preserves any colimits that exist.

Proof

To check that Γ op:C^ opSet op\Gamma^{op} \colon \widehat{C}^{op} \to Set^{op} preserves limits, it suffices to check that the composite

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

Theorem

The terminal object in the initial topos 𝒯\mathcal{T} is connected and projective in the sense that Γ=hom(1,):𝒯Set\Gamma = \hom(1, -) \colon \mathcal{T} \to 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{\mathcal{T}} is also a topos. Observe that 𝒯\mathcal{T} is equivalent to the slice 𝒯^/M\widehat{\mathcal{T}}/M where MM is the object (,1,Γ(1))(\emptyset, \mathbf{1}, \emptyset \to \Gamma(\mathbf{1})). Since pulling back to a slice is a logical functor, we have a logical functor

    π:𝒯^𝒯\pi \colon \widehat{\mathcal{T}} \to \mathcal{T}

    Since 𝒯\mathcal{T} is initial, π\pi is a retraction for the unique logical functor i:𝒯𝒯^i \colon \mathcal{T} \to \widehat{\mathcal{T}}.

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

Finally, since 𝒯(1,)\mathcal{T}(1, -) is a retract of a functor 𝒯^(1,i)\widehat{\mathcal{T}}(1, i-) that preserves finite colimits (by the lemma, and the fact that the logical functor ii 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 xAx\in A such that P(x)P(x)” is provable in the empty context, then there exists a global element x:1Ax\colon 1\to A such that P(x)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.

  • All numerals in the free topos are “standard”, i.e., the global sections functor Γ=hom(1,):𝒯Set\Gamma = \hom(1, -): \mathcal{T} \to Set preserves the natural numbers object NN (because NN can be characterized in terms of finite colimits and 11, by a theorem of Freyd).

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).

As a fibration

The Freyd cover 𝒯¯\overline{\mathcal{T}} is fibered over 𝒯\mathcal{T} as it arises equivalently by change of base of the codomain fibration of Set along the global section functor Γ\Gamma.

See (Jacobs, p.57).

References

Some of the above material is taken from

The following two n-café blog posts provide an introductory discussion of the scone construction from a geometric and a logical perspective:

  • Mike Shulman, Discreteness, Concreteness, Fibrations, and Scones , November 2011. (link)

  • Mike Shulman, Scones, Logical Relations, and Parametricity , April 2013. (link)

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) pp.441-459.

plus

See also section C3.6 of

The following paper studies logical properties of the Freyd cover:

  • Ieke Moerdijk, On the Freyd Cover of a Topos , Notre Dame J. Formal Logic 24 no.4 (1983) pp.517-526. (pdf)

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

For more on the free topos and the first appearance in print of Freyd’s observation see

  • J. Lambek, P. J. Scott, Intuitionist Type Theory and the Free Topos , JPAA 19 (1980) pp.215-257.

Last revised on December 31, 2018 at 21:30:27. See the history of this page for a list of all contributions to it.