9
$\begingroup$

The following result is well-known in folklore (I think), but I’ve been unable to find a reference in the literature:

Let $T$ be a finitely presented essentially algebraic theory, and $\newcommand{\E}{\mathcal{E}}\E$ an elementary topos with NNO. Then there is an initial model of $T$ internal to $\E$.

(By essentially algebraic I mean the notion also known as a cartesian theory or finite limit theory.)

As with many folklore results, various generalisations of this (to settings weaker than elementary toposes, and giving a monadic left adjoint not just an initial model) should also hold, and are also I think fairly well-known or “clearly straightforward generalisations” to people sufficiently well-versed in the field — I’d be equally interested to hear a reference for any such generalisations.

I’d also be interested if anyone can see a way to deduce this directly from some other result(s) in the literature. Proving this by hand isn’t terribly hard (essentially: take the standard construction of a free set model using syntax, and internalise it to an elementary topos), but there’s a fair bit of careful detail-checking to do there (especially when weakening the setting to less than a topos), and I haven’t managed to find a simpler way to deduce it from results in the literature.

The closest results I’ve found are:

  • Theorem 7.43 of Johnstone 1977 Topos Theory, due to Lesaffre, which is the special case of single-sorted algebraic theories.

  • Ch.VI of Johnstone–Wraith 1978 Algebraic theories in toposes (in Indexed categories and their applications, LNM 661 1978). This gives some very relevant results, for a class of theories nearly as general as EAT’s (and sufficient for my interests), but doesn’t (as far as I can see) give free models or any result which immediately implies their existence, except in the special case of the theory of categories, which is rather easier than the general case.

  • The material in §B2 of Johnstone’s Sketches of an Elephant, particularly Theorem 2.4.6, the indexed special adjoint functor theorem. One can deduce this result from that theorem, but the application requires (among other ingredients) construction of a separating family, which seems to me not much easier than just constructing free models by hand directly (but perhaps I’m overcomplicating something).

Improve this question
$\endgroup$
6
  • 3
    $\begingroup$ Are you sure that you do not need at least a Grothendieck topos or a NNO? $\endgroup$
    – Ivan Di Liberti
    Commented Nov 22, 2019 at 18:28
  • 1
    $\begingroup$ The theory of rings is finitely presented, but does not have an initial object in the elementary topos of finite sets. In fact, existence of such initial objects immediately implies that the elementary topos under consideration is a W-topos. $\endgroup$
    – Dmitri Pavlov
    Commented Nov 22, 2019 at 19:27
  • 1
    $\begingroup$ This is very much compatible with the additional request of a NNO. $\endgroup$
    – Ivan Di Liberti
    Commented Nov 22, 2019 at 19:53
  • 1
    $\begingroup$ @IvanDiLiberti: Sorry, yes, of course an NNO is needed. I’m too used to hanging out in circles where one takes “elementary topos” to always include an NNO. But I certainly don’t want to assume a Grothendieck topos (where this can be done off-the-shelf by adjoint functor theorems). $\endgroup$
    – Peter LeFanu Lumsdaine
    Commented Nov 22, 2019 at 22:13
  • 2
    $\begingroup$ I guess Vickers and Palmgreen "Partial Horn logic ..." core.ac.uk/download/pdf/82110032.pdf qualifies. It gives a completely constructive (and even predicative) proof of the existence of the free model for essentially algebraic theory. Their work clearly applies in every exact locally cartesian closed category with a NNO (in particular elementary toposes with NNO). According to the authors, it also apply within an arithmetic universe (=Pretopos with parametrized list objects) but this is not as clear. But the paper do not develop these internal application explicitly. $\endgroup$
    – Simon Henry
    Commented Nov 22, 2019 at 22:49

1 Answer 1

Reset to default
11
$\begingroup$

If you are willing to accept internal argument instead of purely categorical (external) one, a very good reference for this is Palmgren and Vickers' paper: " Partial Horn Logic and cartesian categories".

They give a construction of the initial model for "partial horn theories" (which are equivalent to cartesian theories) which is constructive and predicative.

They don't completely clarify what framework is needed for their proof, but looking at the paper it seems clear that it can be applied internally in any exact locally cartesian closed category with a natural number objects.

I believe (and Steve Vickers seemed to think it was the case as well last time we spoke) their proof also applies within an "arithmetic universe" (a pretopos with parametrized list object) but that is not so easy to extract from the paper.

In both case it applies in elementary toposes with NNO. This is explicitly claimed in the introduction of the paper : they mentioned it can be applied internally within the "predicative toposes" of Moerdijk and Palmgren, and this includes elementary toposes with NNO.

For the record, I would be quite interested if someone could give a satisfying proof that this construction works in an arithmetic universe.

Improve this answer
$\endgroup$
5
  • $\begingroup$ An external/categorical argument is what I was really hoping for, but in lieu of that, this paper seems the next best thing: they give a clean, self-contained, and foundationally economical presentation of the construction, which makes its internalisability much easier to check. I’ll accept this answer in a day or two, unless anyone finds a better answer in that time. $\endgroup$
    – Peter LeFanu Lumsdaine
    Commented Nov 23, 2019 at 18:01
  • 2
    $\begingroup$ Steve and Erik's paper is my favorite presentation of this topic. $\endgroup$
    – Andrej Bauer
    Commented Nov 30, 2019 at 8:27
  • $\begingroup$ "predicative toposes" of Moerdijk and Palmgren, and this includes elementary toposes with NNO. really? I think you probably need WISC or even M&P's "strong AMC" (as van den Berg calls it) to get the result. vdB says ZF is not enough to prove free algebras of algebraic theories exist. $\endgroup$
    – David Roberts ♦
    Commented Nov 30, 2019 at 11:34
  • 3
    $\begingroup$ @DavidRoberts : we are only talking about finitary theories here. The type of problems you are referring too is for infinitary theories. $\endgroup$
    – Simon Henry
    Commented Nov 30, 2019 at 14:24
  • $\begingroup$ @Simon ah, thanks. I thought it uncharacteristic of you to make such a bold and false statement; I apologise! $\endgroup$
    – David Roberts ♦
    Commented Nov 30, 2019 at 14:38

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .