User peter lefanu lumsdaine - MathOverflow

Answer by Peter LeFanu Lumsdaine for Left/right exact functor "in nature" which is not a right/left adjoint

2013-02-22T07:31:10Z

$\newcommand{\C}{\mathbf{C}} \newcommand{\AbGp}{\mathrm{AbGp}} \newcommand{\Psh}{\mathrm{Psh}} \newcommand{\Sh}{\mathrm{Sh}}$Let $\C$ be any site (i.e. small category equipped with a Grothendieck topology). Then the sheafification functor $\AbGp(\Psh(\C)) \to \AbGp(\Sh(\C))$ preserves finite limits, but not in general all limits; so it is a left exact functor without a left adjoint. (It does, however, have a right adjoint — the forgetful functor.)

Non-examples of model structures, that fail for subtle/surprising reasons?

2010-05-02T18:07:59Z

An often-cited principle of good mathematical exposition is that a definition should always come with a few examples and a few non-examples to help the learner get an intuition for where the concept's limits lie, especially in cases where that's not immediately obvious.

Quillen model categories are a classic such case. There are some easy rough intuitions—“something like topological spaces”, “somewhere one can talk about homotopy”, and so on—but various surprising examples show quite how crude those intuitions are, and persuade one that model categories cover a much wider range of situations than one might think at first.

However, I haven't seen any non-examples of model structures written up, or even discussed—that is, categories and classes of maps which one might think would be model structures, but which fail for subtle/surprising reasons. Presumably this is because, given the amount of work it typically takes to construct an interesting model structure, no-one wants to write (or read) three-quarters of that work without the payoff of an actual example at the end. Has anyone encountered any interesting non-examples of this sort?

Background on my motivations: I'm currently working with Batanin/Leinster style weak higher categories, and have a problem which seems amenable to model-theoretic techniques, so I'm trying to see if I can transfer/adapt/generalise the model structures defined by Cisinski et al, Lafont/Métayer/Worytkiewicz, etc. in this area. So I have some candidate (cofibrantly generated) classes of maps, and am trying to prove that they work; and there are lots of good examples around of how to prove that something is a model structure, but it would also be helpful to know what kinds of subtleties I should be looking out for that might make it fail to be.

Answer by Peter LeFanu Lumsdaine for semiring with zero- and nonzero test

2011-07-29T20:26:14Z

I don’t know about your first question; but for the second one, the answer is no — these structures can’t be axiomatised by algebraic identities.

If they could be, then any product of such structures, with the natural induced operations, would again be one. But this is not the case: if $S$, $T$ are any such structures with $0 \neq 1$ in each of them, then the resulting operation $\nu_{S \times T}$ on their product will satisfy $\nu_{S \times T}(0_S,1_T) = (0_S,1_T)$, which is equal to neither $0_{S \times T}$ or $1_{S \times T}$. So $\nu_{S \times T}$ does not satisfy the desired defining property.

The big picture here is Birkhoff’s HSP theorem: a class of algebraic structures, over a fixed language, can be axiomatised by algebraic identities if and only if it is closed under arbitrary products and subobjects (in categorical language: under all limits), and under direct images along homorphisms.

Answer by Peter LeFanu Lumsdaine for Subtler than meets the eye: does x=y imply forall x forall y x=y?

2011-07-29T17:13:48Z

In my experience, Enderton’s definition is far more prevalent. Certainly in categorical logic and the areas of proof theory I’m familiar with, it’s almost always what’s intended.

On the other hand, $\Gamma \vDash \varphi$ is most often used when $\Gamma$ is some theory, i.e. a set of closed formulas, in which case they are equivalent. The difference appears only when $\Gamma$ and $\varphi$ share free variables.

Bilaniuk’s definition (universally closing the two sides separately) is certainly coherent in itself. But Enderton’s definition (universally closing over the whole relation) has various nice properties which Bilaniuk’s lacks:

It corresponds more closely to the “provability” relation $\Gamma \vdash \varphi$. (This is the biggest one!)
The deduction lemma: $\Gamma \vDash \varphi \Rightarrow \psi$ if and only if $\Gamma \cup \{\varphi\} \vDash \psi$.
More general. Any instance of Bilaniuk’s is trivially equivalent to one of Enderton’s (by renaming variables on the right to be disjoint from those on the left).
More intuitive. If I read $\varphi(x,y) \vDash \psi(x,y)$, then it seems natural to expect that the $x$ on the left corresponds somehow to the $x$ on the right, and likewise the $y$. Under Bilaniuk’s reading, the shared variable names are just a red herring.

These are somewhat subjective, of course; I’m sure someone who prefers Bilaniuk’s definition could give some good counter-points.

Answer by Peter LeFanu Lumsdaine for Is there a "disjoint union" sigma algebra?

2011-02-09T20:48:12Z

This does exist, and has a nice explicit description. Treating the sets $A_i$, for convenience, as disjoint subsets of $A$, take a subset $S \subseteq A$ to be measurable exactly if $S \cap A_i$ is a measurable subset of $A_i$, for each $i$. The proof that this is a sigma-algebra making each $\psi_i$ measurable, and is the finest such, is reasonably straightforward.

From a categorical point of view, one can find this description by saying: if such a σ-algebra exists, one would hope that it should make $A$ a coproduct of the $A_i$'s in the category of measurable spaces.

But measurable subsets $S \subseteq A$ must correspond to measurable functions $f \colon A \to 2$ (this holds for any measurable space); hence, by the universal property of $A$, to families of functions $f_i \colon A_i \to 2$; hence to families of measurable sets $S_i \subseteq A_i$; thinking about naturality shows that this correspondence has to be via $S \mapsto (A \cap S_i)_{i \in I}$, and so leads to the description above. (And one can check then that this does indeed give a coproduct.)

One can see this as talking about a duality between the category of measurable spaces and a suitable category of lattices: the coproduct as spaces corresponds to the product of the lattices of measurable subsets.

I have no references, I’m afraid, since I don’t know of any categorically-minded treatments of measure theory. But any such book would surely include this construction; I’m hopeful that there’s one out there that I don’t know of?

Answer by Peter LeFanu Lumsdaine for Is it true that a set is countable if and only if there exists a Turing machine to enumerate all the elements in the set?

2011-03-09T05:17:33Z

No.

Consider the set of all pairs $(x,n,i)$, where: $x$ is the code for a Turing machine $T_x$; $n$ is a natural number; and either $i=1$ and $T_x$ halts on input $n$, or $i=0$ and $T_x$ diverges on $n$.

This set is certainly countable (it’s isomorphic to $\mathbb{N}^2$, just by forgetting the $i$-component). But if we had a Turing machine that enumerated it, then we’d have solved the halting problem: given any code $x$ and input $n$, to work out if it halts, just wait until the machine spits out either $(x,n,0)$ or $(x,n,1)$. (Formally: write a new Turing machine to simulate the running of the first one and “watch” for an appropriate value appearing.)

Generally, subsets of $\mathbb{N}$ that can be given in the manner you describe are called computably enumerable, or recursively enumerable. It’s a fundamental concept of computability theory; it’s a much stronger notion than countability.

Also note that countability is defined as a predicate on abstract sets; it’s not clear what computable enumerability of a set means in the abstract, only for subsets of $\mathbb{N}$ and similarly presented objects.

Answer by Peter LeFanu Lumsdaine for Simple adjective for "of the size of a proper class"?

2011-03-09T04:23:11Z

Proper-class-many.

“We show that if there exist proper class many Woodin cardinals, then the set of reals x for which there is exists an ordinal α with {a ∈ Pω1 (α) | x ∈ L[a]} stationary is countable.” —Paul Larson, Reals constructible from many countable sets of ordinals.

It’s grammatically ugly, but mathematically transparent and unambiguous, and rolls off the tongue reasonably well. I’ve heard it used by and among set theorists, category theorists, and homotopy theorists, without confusion — I’m pretty sure it’s as widely understood as anything will be for this distinction.

Answer by Peter LeFanu Lumsdaine for Topos theory reference suitable for undergraduates

2011-02-19T04:29:28Z

Many people would say this is a terrible suggestion, I think, but depending on your tastes and style, Peter Johnstone’s 1971 book “Topos Theory” might be good.

…true, it’s exceedingly dry, and has been described as “famously impenetrable”, and I certainly wouldn’t recommend it as an only text to try to learn about toposes from. But I actually found it very helpful when I was first learning Topos Theory — first and foremost because it has really, really excellent exercises, with a big range of subjects and difficulties. Secondarily, I also found that once I’d struggled tooth and nail to understand a construction elsewhere, I could come back to Johnstone and appreciate a really clear, neat, perfectly tuned presentation — albeit one I wouldn’t have been able to get anywhere with on its own.

Answer by Peter LeFanu Lumsdaine for The effective topos - by Hyland

2011-02-19T04:05:19Z

Andrew Pitts’ note “Tripos Theory in Retrospect” sheds some useful light on $\mathcal{Eff}$, from a slightly different angle than most other books do. It’s available at his publications page, and also at doi:10.1017/S096012950200364X (paywalled but potentially more durable).

For my part, even as quite a toposophile, $\mathcal{Eff}$ (and realizability toposes in general) took me a while to get comfortable with — a lot longer than any of the other genres, sheaves, syntactic ones, etc. In the end it must have taken about four or five attempts to get to grips with them, over several years — spending a little time getting a little way on each attempt, understanding one step in the construction (e.g.: the tripos-to-topos step in general), then waiting a few months while that sank in, before coming back for another crack at the next step. This certainly isn’t everyone’s experience, of course, but I’ve talked to at least a couple of other people who had a similar time.

Answer by Peter LeFanu Lumsdaine for Game involving 'asking questions about a real'

2011-02-18T17:09:58Z

Partial answer: It is consistent with ZF that Q has a non-deterministic winning strategy.$\newcommand{\R}{\mathbb{R}} \newcommand{\N}{\mathbb{N}}$

First note that if $C(n)$ is ever reduced to a countable set ${x_i\ |\ i \in \N}$, then Q can win just by going through the singletons ${x_i}$ one by one; A must reject each in turn to avoid making $C(n+i)$ a singleton, and so in the end $C(\infty)$ is empty.

Now, suppose that the reals can be expressed as a countable union of countable sets, $\R = \bigcup_{i \in \N}R_i$. (This is consistent with ZF.)

Then Q can start out by listing the sets $R_i$. If A ever chooses $A_i = R_i$, then $C(i)$ is reduced to a subset of $R_i$, so is countable, so by the first note above, Q can win. Otherwise, if A always chooses $A_i = R_i^c$, then since $\R = \bigcup_i R_i$, Q wins in the end as $C(\infty)$ is empty.

Note, however, the non-determinism required: Q cannot choose a full deterministic strategy in advance, since that would require choosing an enumeration of each $R_i$; and this cannot exist, since it would render $\R$ countable.

I suspect that even with choice and looking just at deterministic strategies, it’s consistent that either player has a winning strategy or not. Or, if there is a winner, my money would be strongly on A…

Does this “flipping lexicographic” ordering have a standard name?

2011-02-05T00:34:14Z

I’ve run into the following straightforward variant of lexicographic ordering, and am wondering if it has a standard name. I’ve been calling it the flipping lexicographic ordering, for evident reasons. I could also imagine it getting called the parity lexicographic ordering, but a brief search suggests that that’s used for some slightly different orderings. $\newcommand{\x}{\mathbf{x}} \newcommand{\y}{\mathbf{y}} \newcommand{\N}{\mathbb{N}} \newcommand{\fl}{\mathrm{fl}} \newcommand{\lfl}{\;\sqsubset^\fl\;}$

For sets $\x, \y \in \binom{\N}{m+1}$, write $\x = \{x_0 < \ldots < x_m\}$, $\y = \{y_0 < \ldots < y_m\}$.

Definition. $\x \lfl \y$ if $\x$ and $\y$ differ first in the $i$th place, and

$i$ is even, and $x_i < y_i$; or
$i$ is odd, and $y_i < x_i$. (This is the flip!)

As for ordinary lex, there’s also a nice inductive characterisation: Write $\x = \{x_0\} \cup \x^{\geq 1}$, and $\y = \{y_0\} \cup \y^{\geq 1}$, similarly to above. Then $\x \lfl \y$ if and only if either $x_0 < y_0$, or $x_0 = y_0$ and $\y^{\geq 1} \lfl \x^{\geq 1}$. (Again, note the flip.)

Does this ring any bells with anybody?

(Of course, $\lfl$ has obvious generalisations beyond $\binom{\N}{m+1}$; I’m sticking to that case here partly for definiteness, mainly since that’s the specific case I’m interested in.)

Background: I’ve been playing around with implementing the algorithms from Ross Street’s “The Algebra of Oriented Simplices” (and related papers) in Haskell/Agda, and this ordering turns out to make a computationally convenient stand-in for his $\lhd$ order, in places.

Answer by Peter LeFanu Lumsdaine for Is it possible to construct (without choice, even?) a non-finitely-generated group with no proper non-finitely-generated subgroup?

2011-01-23T04:55:39Z

(CW since this is just expanding on George Lowther’s comment to the question, which could really have been an answer in the first place; if George L wants to convert his answer to a comment himself, I can delete this one.)

For any prime $p$, the Prüfer $p$-group is as desired.

There are several constructions of this; a good one for present purposes is $$\mathbb{Z}[1/p]\ /\ \mathbb{Z}$$ i.e. rationals with denominator a power of $p$, modulo the integers.

To see that this works, note that it is the union of the linearly ordered chain of finitely generated (indeed, cyclic) subgroups $H_i := \{ [a / p^i]\ |\ 0 \leq a < p^i \}$, over $i \in \mathbb{N}$.

Now any element of $H_{i+1}$ not in $H_{i}$ must be of the form $[a/p^{i+1}]$ with $a$ coprime to $p$, and hence generates the whole of $H_{i+1}$. So any subgroup is either equal to some $H_i$, or else contains them all and is the whole group.

On the other hand, the entire group is clearly not finitely generated since any finite set of elements is contained in some $H_i$.

Answer by Peter LeFanu Lumsdaine for Are the axioms for higher category-theory effectively computable?

2011-01-16T18:50:00Z

Yes.

…at least, for Leinster’s reformulation of Batanin’s definition of globular operadic weak ω-category (and hence also for the finite-dimensional versions of this). Showing this is essentially a matter of repeatedly applying one lemma: if $\mathbf{T}$ is an essentially algebraic theory with a computable presentation, then the free $\mathbf{T}$-structure on a computably presented object is again computably presented. By “computably presented”, I mean essentially that the sets of operations and axioms are all computably enumerable.

In the Leinster/Batanin definition, one starts with strict $\omega$-categories (certainly a computably presentable theory, by the standard explicit axiomatisaion); by their observation above, their monad $T$ is computably presentable; from this, one can show that the theory of $T$-operads is computably presentable; similarly, then, the theory of $T$-operads-with-contraction; so the free $T$-operad-with-contraction $L$ is computably presentable.

But now the operations of the theory of weak $\omega$-categories are the elements of $L$; and the axioms are given by elements of “powers” of $L$, in the monoidal structure $\otimes$ built by $T$ and pullbacks; so these sets are all computably enumerable, so we’re done.

From here on I’m a little beyond my comfort zone, and wouldn’t want to swear that the details hold up: someone who knows realizability toposes better than I do can probably tell better whether I’ve missed some subtlety.

A nice way to look at the above argument could be to say: develop the theory of weak $\omega$-categories in $\newcommand{\Eff}{\mathcal{E}\textit{ff}} \Eff$, the effective topos — that is, repeat all the normal definitions in the internal logic of $\Eff$, to get an internal theory $\mathbf{T}^{\Eff}_\omega$. (Possibly $\mathbf{PER}$ or some other category of ‘computably presented sets and functions’ might work better than $\Eff$.)

Now, the global sections functor $\Gamma \colon \Eff \to \mathbf{Sets}$ is a left exact left adjoint, so in particular, it will commute with pullbacks and with most ‘free object’ constructions — so, with all the ingredients used in the definition of the theory of weak $\omega$-categories. So when we hit $\mathbf{T}^{\Eff}\omega$ with $\Gamma$, we just recover the original external theory $\mathbf{T}\omega$. That is, $\mathbf{T}^{\Eff}\omega$ is a computable presentation of $\mathbf{T}_\omega$

Intuitively, we’re ‘shadowing’ every construction we do in $\mathbf{Sets}$ with a computable presentation, by performing the same constructions in parallel up in $\Eff$.

This approach should also work for most other theories of higher categorical structures — power-sets and non-finite exponentiation are the main logical constructions not preserved by $\Gamma$, and off the top of my head, only the definitions of higher categories which involve topological constructions will require these.

Answer by Peter LeFanu Lumsdaine for Why are matrices ubiquitous but hypermatrices rare?

2010-12-02T16:34:56Z

An awfully simplistic answer: we work on two-dimensional paper, so two-dimensional matrices are very convenient to write down and compute with, while higher-dimensional hypermatrices are not.

So while we could represent multilinear forms, tensors, etc. as hypermatrices, we often don’t, because doing so is not nearly as fruitful as representing linear maps, bilinear forms etc. as matrices. Instead, we usually use other notations when working with higher tensors by hand.

In computer algebra, the dimension of the paper is not significant, while some kinds of abstraction are harder, so in this context, higher tensors are much more often represented as hypermatrices.

Answer by Peter LeFanu Lumsdaine for "classes" with no cardinality; "classes" with no equality notion

2010-11-24T20:11:33Z

Classical axiomatic set theories (eg ZFC, NGB) are formulated in first-order logic with equality, so any things you can quantify over (i.e. that you can talk about as actual objects of the language), you can talk about equality of, as a basic given of the language.

In particular, in either ZFC or NGB, you can certainly talk about equality of vector spaces. In ZFC, you can’t talk about beasts as quantify-over-able objects (since they can only be represented as proper classes, not as sets); in NGB, you can, and so you get equality of them.

Cardinality is a bit slipperier: it’s generally considered as a defined rather than a basic notion, and the exact definitions used vary in ways your question will be sensitive to. Most often, an object called the “cardinality” is only specifically defined for sets^[1]; for classes, “C and D have the same cardinality” is considered syntactic sugar for “there is a class-bijection between C and D”. So it’s not quite clear what it means to ask if a class “has cardinality”, but whatever it is depends heavily on having an equality relation on it, to be able to talk about bijections to/from it.

On the other hand, there are some more recent set/type theories in which equality isn’t given, or is a more flexible notion.

In some versions of the Calculus of Constructions, if I remember right, there is a universe of small sets (possibly multiple universes), and an arbitrary product of sets is again a set, possibly in some higher universe (this has to be formulated carefully to avoid inconsistency); and each set has equality on it, but there’s no equality on the universe(s). So there, vector spaces wouldn’t form a set, and wouldn’t have an equality relation; but beasts would form a set (a certain product of hom-sets) so would have an equality relation. (The C of C’s is a little out of what I know, so this may need correcting by someone more knowledgeable.)

Similarly, there are versions of Martin-Löf Type Theory with identity types which address this issue; roughly, identity types can represent something like an ordinary equality relation, but more generally they can also look like the sets/categories of (weak) ismorphisms in a (higher) category. So you can define an object to be 0-categorical^[1] if all its identity types are just truth-values; then an arbitrary product of 0-categorical types is again 0-categorical.

In this setup, the type of all vector spaces within some universe will have identity types, so equality of a sort, but not of the objectionable kind — “equality” of vector spaces will exactly be isomorphism between them. The type of beasts over this universe will now be 0-categorical: we will have equality of beasts in the simplest sense. (Also, in this foundation, all beasts will automatically respect isomorphism!)

[1]: The two main definitions of $\|X\|$ I know are “the least ordinal bijective to $X$” (elegant, but requires choice to be defined for all $X$), or “$\{ Y \in V_\alpha\ |\ Y \cong X \}$, where $\alpha$ is minimal such that this is non-empty” (less transparent but more robust).

[2]: I first heard this definition from Voevodsky, though I’m pretty sure it had been considered by others before as well. He calls this property being a set, but I want to make unambiguous that it’s a restriction of categorical dimension not of size.

Answer by Peter LeFanu Lumsdaine for Sexy vacuity ....

2010-11-14T00:34:20Z

An elementary example, but pedagogically nice: a standard early induction proof example is that you can tile any $2^n \times 2^n$ square with one unit square removed, using L-shaped tiles of three unit squares each.

Surprisingly (to me), many textbooks take the base case as $n=2$. The better ones use $n=1$. But the version in The Book, though, surely starts at $n = 0$!

(Of course, I understand the pedagogy of not starting at 0: it’s usually best to make one point at a time. Trying to use this single example to teach about both induction and vacuity simultaneously would end up confusing most students. But when it’s not needed for the former, it does work nicely for the latter, I think!)

Answer by Peter LeFanu Lumsdaine for What's the name of this flavor of n-category?

2010-11-12T08:10:17Z

Simpson-semistrict $n$-categories could be what you're after: $n$-categories where everything except the unit laws holds strictly, generalising one of the crucial properties of Moore path spaces? It's not a specific definition of $n$-category, but a strictness property which can be applied within various definitions.

Carlos Simpson has conjectured that these are enough to model homotopy types; Moore path space show this in dimension 1. I know very little about the details of this myself, I'm afraid, but what I have read about it is mostly from these sources plus their links and discussions:

Simpson, Homotopy types of strict 3-groupoids.
nlab: semi-strict $\infty$-category
nlab: Simpson’s conjecture (I can't figure out how to link this directly; the single-quote in the url seems to confuse markdown)
n-Category Café: Urs Schreiber, Semistrict Infinity-Categories and ω-Semi-Categories

I believe several people have been making some progress on it recently; eg Makkai mentioned some results along these lines at the latest Octoberfest.

Answer by Peter LeFanu Lumsdaine for compact-open topology

2010-10-31T18:35:28Z

Exactly as you say, adjoint functors are the answer! (Or at least, they're one possible answer.) In particular, for reasonable spaces $X,Y,Z$, there is a natural isomorphism

$\mathrm{Hom} (X \times Y, Z) \cong \mathrm{Hom} (X, [Y,Z])$

where $[Y,Z]$ denotes $\mathrm{Hom}(Y,Z)$ with the compact-open topology. This is exactly the categorical characterisation of an exponential object.

This certainly holds when $X,Y,Z$ are compactly-generated Hausdorff spaces, so the category of such spaces is Cartesian closed. It actually also holds under rather weaker conditions on $X,Y$ and $Z$ individually — I can't recall them off the top of my head though and am in a bit of a rush, so am wiki'ing this answer in hopes someone can fill them in. Now, this also holds if we take weaker conditions on $X$ and $Y$ (just Hausdorffness), and a slightly stronger condition on $Y$ (local compactness). $Z$ may be arbitrary.

Re Mariano's comment: yes, in some sense this is just fancy language for “things we want to converge, converge; things we don't, don't”. But I think this helps explain why we want the things we want to converge, to converge. ☺

Answer by Peter LeFanu Lumsdaine for Locally a topos

2010-10-20T01:15:15Z

The question of local toposes and similar categories was discussed a couple of years ago on the categories list by Peter Johnstone and others, if I recall correctly. I don't know anywhere that they appear in print, but I don't know the topos theory literature nearly well enough to be an authoratitive source on this.

On the local toposes themselves: $\newcommand{\Topos}{\mathbf{Topos}_\mathit{slice}}$one other in-some-sense-trivial example, if I'm not mistaken, is the category $\Topos$, with objects all (small, fsvo small) elementary toposes, and with maps just the geometric morphisms that are (up to equivalence) induced by slicing, modulo natural isomorphism. (If we wanted to cover our tracks a little, we could say “the geometric morphisms whose inverse image functors are logical”; the equivalence of this is shown in Mac Lane and Moerdijk in their chapter on logical morphisms, iirc.)

But this is the universal example: any other local topos $\newcommand{\E}{\mathcal{E}}$has a unique-up-to-equivalence “local equivalence” $\E \to \Topos$, sending $A$ to $\E/A$, and any local equivalence into $\Topos$ must come from a local topos.^[1]

But local equivalences into a fixed category $\newcommand{\C}{\mathcal{C}} \C$, in turn, correspond (up to equivalence-over-$\C$) to functors $\C^\mathrm{op} \to \mathbf{Sets}$. ($F : \mathcal{D} \to \C$ corresponds to the functor taking $C \in \C$ to the set of isomorphism classes of objects of $\mathcal{D}$ over $C$.) Of course, there's a size consideration: whatever size of $\mathbf{Sets}$ we use constrains the essential size of the fibers.

In terms of local toposes seen as categories in their own right, one point of interest is that you can interpret pretty much all the logic in them that you can in toposes (i.e. higher-order type theory; and geometric logic if you go Grothendieck-y)… except that of course you have to abandon the “empty context”, since you don't have a terminal object. (Everything else in the interpretation of logic is purely local.) In a local topos, there is no “global validity”: all truth is relative :-)

[1] The uniqueness issues here are a little subtle: if I'm not mistaken we need to either assume (large) choice, or use anafunctors instead of functors, or restrict the size of $\E$ enough that each slice will itself literally be an object of $\Topos$.

Answer by Peter LeFanu Lumsdaine for Can we define geometric morphisms (between ETCS categories) elementarily?

2010-10-20T01:37:48Z

Yes, it is possible. Precisely, we can write down a first-order theory for which a model is a pair of ETCS-models and a geometric morphism between them (am I right in thinking this is what you're asking for?).

To do this, on top of axiomatising “a pair of models of ETCS”, you add some extra function symbols for the adjunction. The conditions of functoriality, etc. are easily written algebraically; the adjunction can be expressed in various ways, of which the simplest to write down is probably the triangle-inequalities form. “Preserving finite limits”, when you write it out, is also just a scheme of first-order conditions; if you want to reduce it to a finite axiomatisation, note that it's enough to ask for preservation of finite products and equalisers (by the usual proof that all finite limits can be constructed from these).

This said, I disagree somewhat with an implicit premise of your question. You say: “Then one can define the category of ETCS categories…” But to do this, you don't need to show that geometric morphisms can be defined in first-order terms. To talk about “the category of ETCS categories”, you already need to be working in a meta-theory with some sort of notion of set or similar (eg types, etc.); and so don't need the definitions of the morphisms to be first-order.

The foundational advantage of a first-order axiomatisation of widgets is that you can then study a single widget without needing any meta-theory. But to study the collection of all widgets (as a category or whatever else), you still need a meta-theory.

Answer by Peter LeFanu Lumsdaine for Rings with right inverses

2010-10-15T05:17:06Z

Consider the space $\mathbb{Z}^\mathbb{N}$ of integer sequences $(n_0,n_1,\ldots)$, and take $R$ to be its ring of endomorphisms. Then the ``left shift'' operator $$(n_0,n_1,\ldots) \mapsto (n_1,n_2,\ldots)$$ has plenty of right inverses: a right shift, with anything you want dropped in as the first co-ordinate, gives a right inverse.

I recall finding this example quite helpful with the exercise ``two right inverses implies infinitely many'' — taking a couple of the most obvious right inverses in this case, and seeing how one can generate others from them.

Answer by Peter LeFanu Lumsdaine for Axiom of Replacement in Category Theory

2010-10-05T19:54:00Z

There’s one issue underlying a lot of the discrepancies between people’s answers, I think:

How are we defining “$f$ is a function $s \to V$”, where $s$ is a set and $V$ is a (possibly proper) class?

(hence also, how we define subsequent things like “a small-category-indexed diagram of sets”) There are at least two main options here:

$f$ is a class of pairs, such that…
$f$ is a set of pairs, such that…

At least in most traditional presentations, I think it’s defined as the latter, but some people here also seem to be using the former. The answer to this question depends on which we take.

If we take the “a function is just a class” definition, then as suggested in the original question, and as stated in François’ answer, we definitely have some big problems without replacement: Set is no longer complete and co-complete, etc. (nor are the various important categories we construct from it); we can’t easily form categories of presheaves; and so on. Under this approach, we certainly get crippling problems in the absence of replacement.

On the other hand, if we take the “a function must be a set” definition, we get some different problems (as pointed out in Carl Mummert’s comments), but it’s not so clear whether they’re big problems or not. We now can form limits of set-indexed families of sets; presheaf categories work how we’d hope; and so on. The problem now is that we can’t form all the set-indexed families we might expect: for instance, we if we’ve got some construction $F$ acting on a class (precisely: if $F$ is a function-class), we can’t generally form the set-indexed family $\langle F^n(X)\ |\ n \in \mathbb{N} \rangle$.

This is why we still can’t form something like $\bigcup_n \mathcal{P}^n(X)$, or $\aleph_\omega$. On the other hand, such examples don’t seem to come up (much, or at all?) outside set theory and logics themselves! Most mathematical constructions that do seem to be of this form — e.g. free monoids $F(X) = \sum_n X^n$, and so on — can in fact be done without replacement, one way or another.

Now… I seem to remember having been shown an example that was definitely “core maths” where replacement was needed; but I can’t now remember it! So if we take this approach, then we certainly still lose something; but now it’s less clear quite how much we really needed what we lost.

(This approach is very close to the question “What maths can be developed over an arbitrary elementary topos?”.)

Answer by Peter LeFanu Lumsdaine for Strict ordering on natural numbers

2010-09-27T15:48:38Z

With the common set-theoretic approach of defining the order in terms of $\subseteq$ or $\in$, appealing to eg transitivity/ordinality is unavoidable. But if you take a slightly different approach to the definitions, these can certainly be done with just induction and a couple of basic facts about the surrounding set theory; and the end result is in a sense more natural, not depending on the specific implementation of the numbers.

Suppose $N$ is any set, $0 \in N$, and $s: N \to N$, and $(N,0,s)$ satisfy the usual induction principle.

Then firstly, you can bump this up to the recursion principle: that you can define functions on $N$ (in particular, ${0,1}$-valued functions, i.e. predicates) by recursion. This is where you need to use a few things in how the surrounding theory treats functions and so on. (You could also start by saying that recursion, rather than induction, should be the basic defining principle of the natural numbers.)

Now you can define the strict ordering by recursion:

$0 \not < 0$;
$0 < s(n)$;
$s(n) \not < 0$;
$s(n) < s(m)$ iff $n < m$.

Now irreflexivity, transitivity and antisymmetry are all immediate by induction… just divide up into the appropriate cases, and the induction steps fall straight out :-)

Answer by Peter LeFanu Lumsdaine for The "skinnest" object

2010-09-12T14:05:24Z

The common thread in each of these examples seems to be something like:

The “skinniest widget” that you're looking for is the initial widget, if one exists. (Edit: actually, as Tom Goodwillie points out in comments on the OP, it's subtler than this; in some cases you're interested in widgets that aren't quite initial, but are nicer than just a random weakly initial one.)

By the adjoint functor theorem, as you say, the construction can be done in two stages, given the solution-set condition and enough limits. First, take a product of the solution set to get a weakly inital widget $W$.

Then take the intersection of all the sub-widgets of $W$; and this gives the initial widget you want. In the widest generality, this is the “intersection” in the categorical sense of being a limit of various subobjects of a fixed object, i.e. a limit in $\mathrm{Sub}(W)$. But in most common examples, e.g. in any algebraic category over $\mathbf{Sets}$, this'll be intersection in the normal set-theoretic sense (since the forgetful functor down to $\mathbf{Sets}$ preserves/reflects limits).

[I'm not sure whether this is quite what you want! It seems to answer the question you asked… but pretty much everything I say is already implicit in what you've written in the question, so maybe you were after something more?]

Answer by Peter LeFanu Lumsdaine for Need help understanding a topos theory proof (any topos generated by subobjects of 1 in whose subobject lattices are complete and Boolean satisfies AC)

2010-09-12T16:14:20Z

Your approach is absolutely right: apply Zorn's lemma to the poset of pairs $(M,s)$ where $M \subseteq I$ is a subobject and $s: M \to X$ is a partial section of $p$.

As you say, to see that this poset is chain-complete, we just need to show that the least upper bound in $\newcommand{\Sub}{\mathrm{Sub}} \Sub(I)$ of a chain ${M_i}$ is in fact a colimit in $\mathcal{C}/I$, and hence that the sections also extend.

The key point here is that as long as the chain is inhabited, this is a filtered colimit. Filtered colimits are computed in $\Sub(I)$ just as colimits in $\newcommand{\C}{\mathcal{C}}\C$ (Charles Rezk's answer has just appeared, and shows this nicely); and all colimits in $\C/I$ are computed just as colimits in $\C$; so filtered colimits in $\Sub(I)$ are colimits in $\C/I$, and we're done.

…at least modulo the question of the empty chain! but this is easy to fix, in (at least) two ways. The simplest way is just to look at the case of the empty chain separately, and see that it's trivial. A nicer way (to my taste) is to state Zorn's lemma as “any (inhabited chain)-complete poset has a maximal element above any given element”. Neither of these feels quite right to me here — both seem a little ad hoc — but they do at least both work :-)

Answer by Peter LeFanu Lumsdaine for Maximal subcoalgebras of an $F+1$-coalgebra corresponding to an $F$-coalgebra

2010-09-08T14:27:02Z

I think the construction you're looking for can be seen as a right adjoint, and hence the details of the construction can be seen as coming from general transfinite constructions of adjoints.

$\newcommand{\inl}{\mathrm{inl}} \newcommand{\Coalg}{\mathbf{Coalg}}$ There's a functor $\inl^* : F$-$\Coalg \longrightarrow (F+1)$-$\Coalg$; it embeds $F$-coalgebras asthe full subcategory of "error-free" $F+1$-coalgebras, and is induced by the natural transformation $\inl : F \rightarrow F+1$ in an obvious-once-you-write-down-the-diagram way.

Now, if I'm understanding right, the construction you're looking at, the "error-free core" of an $F+1$ coalgebra, is the right adjoint to this.

Moreover, I think there should be theorems that show automagically why this can be computed by the construction you give, as an $\omega$-long limit of pullbacks — but I'm not sure exactly where, I'm afraid. It's almost certainly deducible from the Kelly "Unified treatment of transfinite constructions" paper, well-described by Tom Leinster here; the constructions of that have a very similar flavour.

Possibly relevant well-known constructions to compare (in Kelly and elsewhere): the construction of an algebraically-(co)free (co)monad on an endofunctor; the construction of the free $T$-algebra on a $T$-graph; the free $S$-algebra on a $T$-algebra, given a monad map $S \to T$.

Answer by Peter LeFanu Lumsdaine for Do normal categories have pullbacks?

2010-09-06T01:47:02Z

If I'm not mistaken, the category “vector spaces of dimension $\leq n$” (for any $n > 0$) is a counterexample? The zero object, kernels, cokernels, and the normality of kernels can all be computed as they normally are for vector spaces; but products (and hence pullbacks) are missing for ~~obvious~~ reasons of dimension. [See comments for elaboration.]

The problem is, intuitively, that there's nothing in the definition of “normal” providing a way to build bigger things out of smaller.

On the other hand, I think one can prove “a normal category has pullbacks of monos”; it sounds like that might be what the book is proving here? Maybe that's all that it actually ends up using in the rest of the chapter, and this is just an omission in the statement of the theorem?

Alternatively, if one adds products to the definition of “normal”, then from that together with pullbacks of monos, one can build all pullbacks (the pullback of $f$ and $g$ is the pullback of the appropriate diagonal map (a mono) along $f \times g$).

Answer by Peter LeFanu Lumsdaine for Pushout over a whole diagram

2010-09-03T20:23:27Z

I'd think of it as being the pushout functor along $a$, between co-slice categories: $$a_* \colon\ c\backslash C\ \longrightarrow\ e\backslash C$$

Mac Lane CWM gives a nice treatment of pullback functors, which iirc contains statements dual to everything you mention here.

(So this construction is a lot more general than the example: all that matters is that the diagram involved has an initial object $c$, hence can be seen as living not just in $C$ but in $c \backslash C$. The “joins are colimits” condidition isn't needed; and the pushouts don't have to be computed “successively” — the “two pushouts lemma”, or equivalently the functoriality of $a_*$, shows that computing them successively or all-at-once gives the same result.)

(answer jointly written with Michael Warren)

Answer by Peter LeFanu Lumsdaine for Indecomposable objects in a category

2010-08-17T16:19:46Z

Briefly: there's a simple difference in how they treat 0. That fixed, still neither implies the other in general. In a regular extensive category, a slight modification of the LS definition implies the Elephant one. ~~I suspect they're not fully equivalent in anything short of a topos.~~ As Mike Shulman points out, even in a topos they are not equivalent.

The simple difference: 0 is always indecomposable by Lambek and Scott's definition (since any map into 0 is epi), but never by the Elephant's (since the uniqueness condition won't hold; or by considering when the coproduct decomposition is empty). So, let's temporarily change one of the definitions to fix this. I'd suggest we add “…and the map $0 \to X$ is not epi.” to Lambek and Scott's definition. (As you noted, their binary condition generalises to a $k$-ary one; this is just the case $k=0$.)

In eg Top, however, we can see that the Elephant def still doesn't imply the LS def. $[0,1]$ satisfies the former (it's not decomposable by an iso), but not the latter (it is decomposable by an epi). Even more, it’s decomposable by a regular epi (more on this distinction below).

Conversely, the LS definition doesn't imply the Elephant one either; it fails in eg $\mathbf{Set}^\mathrm{op}$, since in $\mathbf{Set}$, $0$ is co-decomposable by iso ($0 \cong A \times 0$) but not co-decomposable by monos (for any map $(f,g) \colon 0 \to A \times B$, not just one but both of $f$ and $g$ are mono).

When do they imply each other? If we upgrade the LS definition to involve regular epis, then in a regular lextensive category, it implies the Elephant definition, if I'm not mistaken. For this, suppose $X$ is “indecomposable by reg epis”, and suppose $X \cong A + B$ — WLOG $X = A + B$. The coproduct inclusions are then jointly reg epi, so one of them is reg epi. But it's also mono (in a lextensive category, every coproduct inclusion is a pullback of $1 \to 1 + 1$, so is mono); so it's iso. There's a little more fiddly stuff to check involving messing around with $0$, but it's all the same sort of thing.

Edit from Mike Shulman's comments: if moreover we're in a pretopos, all epis are regular, so there the original LS definition will imply the Elephant definition. On the other hand, the Elephant definition doesn't imply the LS even in a topos: the terminal object of $\mathbf{Sh}([0,1])$ is a counterexample, essentially for the same reasons that $[0,1]$ was a counterexample in $\mathbf{Top}$.

However, the two definitions are equivalent for projective objects… and I guess that's how this situation has arisen, since a common use of indecomposable objects in topos theory is the theorem that the indecomposable projectives in a presheaf category are exactly the retracts of representables. (This is useful because it lets us recover the idempotent-completion of $\mathbf{C}$, which is very close to $\mathbf{C}$ itself, from $[\mathbf{C}^\mathrm{op},\mathbf{Set}]$.)

Answer by Peter LeFanu Lumsdaine for A functor that comes from a morphism in a bigger category

2010-08-11T21:03:40Z

If I understand your question right, the term you want is an equivalence (or isomorphism) over Set. Concretely, this means: it's an equivalence in which the categories have (forgetful) functors to Set, the functors of the equivalence commute down to Set, and the natural transformations are identities on underlying sets.

More concisely, it means: an equivalence in the slice 2-category Cat / Set.

(In particular, between categories of algebras, subcategories of these, and most other categories defined over Set, any equivalence over Set has to be an isomorphism, because of the fact that if $1_X$ lifts to a map between two algebra structures on a set $X$, then the structures must be the same.)

Comment by Peter LeFanu Lumsdaine

2013-05-19T23:53:07Z

@msbq: if a function is defined as simply a set of ordered pairs, then indeed your claimed absurdity, “there’s nothing to distinguish them” is one. But if a function is defined as including its domain and codomain, then it’s not an absurdity at all — they’re distinguished by their codomains! Which definition is the right one is clearly a debatable and somewhat subjective question — many people would argue each, and perhaps the right answer is that depending on the field, each can sometimes be more fruitful — but calling this issue an “absurdity” is rather unhelpful.

Comment by Peter LeFanu Lumsdaine

2013-05-03T21:42:02Z

@Oksana Gimmel: very interesting! Can you suggest any references for reading on that last bit? (It’s rather difficult to search about!)

Comment by Peter LeFanu Lumsdaine

2013-04-28T03:25:34Z

In the currently last example, sending $G$ to the discrete graph on $\pi_0(G)$, isn’t there a problem with the unit morphism — edges within each connected component have no edges to map to?

Comment by Peter LeFanu Lumsdaine

2013-03-21T06:34:01Z

@Zhen Lin: true, the internal logic talks about all objects as though they were just unstructured sets. But one can still often re-express external local notions in these terms — see e.g. the internal construction of a sheafification. Talking about local operators, for instance, isn’t tacking on anything extra: they can be described entirely using the internal logic itself, as constructions based on certain elements of $\mathcal{P}(\Omega)$. (From the internal point of view, they’re just Grothendieck topologies on the terminal category.)

Comment by Peter LeFanu Lumsdaine

2013-03-21T06:29:03Z

I’m not sure I follow your second paragraph. The logic of Set certainly can tell the difference between a finite and an infinite set. Of course, it doesn’t do so in a novel way, since the logic of Set is just (a large fragment of) the logic we reason in all the time. But that novelty is exactly what can get more interesting when one moves to a different topos!

Comment by Peter LeFanu Lumsdaine

2013-03-16T23:49:29Z

If a logician said that the interplay of $+$ and $\times$ was not well understood, I would expect them to mean something like this. If an algebraist (or algebraic geometer, number theorist, etc) said it, though, I would expect them to mean something very different. Was the OP referring to comments from a logician, or an algebraist, I wonder?

Comment by Peter LeFanu Lumsdaine

2013-02-03T19:28:01Z

One category-theoretic approach to this is that Kripke models of modal logic can be seen as sheaf/presheaf models, with the modalities often coming from sheafification for some Grothendieck coverage (equivalently, some Lawvere-Tierney closure operator). I can’t off the top of my head remember where is a good source for reading up on this, but hopefully those keywords should at least be useful for searching with.

Comment by Peter LeFanu Lumsdaine

2012-12-16T17:54:28Z

Can you recommend a good reference that gives this proof?

Comment by Peter LeFanu Lumsdaine

2012-12-14T22:22:21Z

Mathoverflow is intended for research-level questions (as per the faq); this question would be better suited to math.stackexchange.com.

Comment by Peter LeFanu Lumsdaine

2012-11-28T22:07:14Z

This has been asked and answered at math.stackexchange.com: [math.stackexchange.com/questions/84436].

Comment by Peter LeFanu Lumsdaine

2012-09-26T13:26:33Z

@usinger: math.stackexchange.com would be a better fit for this question; if you post it there, I’ll answer it unless someone else does first.

Comment by Peter LeFanu Lumsdaine

2012-09-24T02:43:51Z

I don’t think ultrafinitists would accept the arguments in your first two paragraphs: they’re essentially the same as the argument that from 0 and S, one obtains infinitely many natural numbers; and this is exactly the kind of induction instance that ultrafinitists reject. In particular, “$V \in V$” seems no worse than “$0 \leq 0$”, which I’m pretty sure ultrafinitists accept.

Comment by Peter LeFanu Lumsdaine

2012-09-24T02:15:14Z

The statement in this answer is quite true, but unless I’m misunderstanding something, it doesn’t give a counterexample to the question. The two trees intended are, I presume, the ones represented (using the initial-segment ordering on sequences) by {0,00,000,0000,00000,000000,00001,000010}, and by {0,00,000,0000,00000,000000,000000,000001}. These have different numbers of 6-node subtrees (3 and 2 respectively; just lop off the 4-vertex trunk and consider 2-node subtrees), so by Owen’s answer, they will be distinguished by $P$.

Comment by Peter LeFanu Lumsdaine

2012-04-07T22:20:38Z

@Emil: the interest is in the unexpected reason for the answer.

Comment by Peter LeFanu Lumsdaine

2012-02-21T17:19:51Z

Having “honorable mentions” awarded for prizes does not normally mean “all the other submissions were not worth mentioning”. It usually means something more like “these submissions are so good that we would have liked to give them the prize, if there hadn’t been one even better”.