Earlier this week my friend Shane and I took a day and just did a bunch of computations. In the morning we did some differential geometry, where he told me some things about what he’s doing with symplectic lie algebroids. We went to get lunch, and then in the afternoon we did some computations in derived algebraic geometry. I already wrote a blog post on the differential geometry, and now I want to write one on the derived stuff too! I’m faaaaar from an expert in this stuff, and I’m sure there’s lots of connections I could make to other subjects, or interesting general theorem statements which have these computations as special cases… Unfortunately, I don’t know enough to do that, so I’ll have to come back some day and write more blog posts once I know more! I’ve been interested in derived geometry for a long time now, and I’ve been sloooowly chipping away at the prerequisites – $\infty$-categories and model categories, especially via dg-things, “classical” algebraic geometry (via schemes), and of course commutative and homological algebra. I’m lucky that a lot of these topics have also been useful in my thesis work on fukaya categories and TQFTs, which has made the time spent on them easy to justify! I’ve just started reading a book which I hope will bring all these ideas together – Towards the Mathematics of Quantum Field Theory by Frédéric Paugam. It seems intense, but at least on paper I know a lot of the things he’s planning to talk about, and I’m hoping it makes good on its promise to apply its techniques to “numerous examples”. If it does, I’m sure it’ll help me understand things better so I can share them here ^_^. In this post we’ll do two simple computations. In both cases we have a family of curves where something weird happens at a point, and in the “clasical” case this weirdness manifests as a discontinuity in some invariant. But by working with a derived version of the invariant we’ll see that at most points the classical story and the derived story agree, but at the weird point the derived story contains ~bonus information~ that renders the invariant continuous after all! Ok, let’s actually see this in action! First let’s look at what happens when we intersect two lines through the origin. This is the example given in Paugam’s book that made me start thinking about this stuff again. Let’s intersect the $x$-axis (the line $y=0$) with the line $y=mx$ as we vary $m$. This amounts to looking at the schemes $\text{Spec}(k[x,y] \big / y)$ and $\text{Spec}(k[x,y] \big / y-mx)$. Their intersection is the pullback and so since everything in sight is affine, we can compute this pullback in $\text{Aff} = \text{CRing}^\text{op}$ as a pushout in $\text{CRing}$: Pushouts in $\text{CRing}$ are given by (relative) tensor products, and so we compute which is $k$ when $m \neq 0$ and is $k[x]$ when $m=0$, so we’ve learned that: When $m \neq 0$ the intersection of \(\{y=0\}\) and \(\{y=mx\}\) is $\text{Spec}(k)$ – a single point1. When $m = 0$ the intersection is $\text{Spec}(k[x])$ – the whole $x$-axis. This is, of course, not surprising at all! We didn’t really need any commutative algebra for this, since we can just look at it! The fact that the dimension of the intersection jumps suddenly is related to the lack of flatness in the family of intersections $k[x,y,m] \big /(y, y-mx) \to k[m]$. Indeed, this doesn’t look like a very flat family! We can also see it isn’t flat algebraically since tensoring with $k[x,y,m] \big / (y, y-mx)$ doesn’t preserve the exact sequence2 In the derived world, though, things are better. It’s my impression that here flatness is a condition guaranteeing the “naive” underived computation agrees with the “correct” derived computation. That is, flat modules $M$ are those for which $M \otimes^\mathbb{L} -$ and $M \otimes -$ agree for all modules $X$! I think that one of the benefits of the derived world is that we can pretend like “all families are flat”. I would love if someone who knows more about this could chime in, though, since I’m not confident enough to really stand by that. In our particular example, though, this is definitely true! To see this we need to compute the derived tensor product of $k[x,y] \big / (y)$ and $k[x,y] \big / (y-mx)$ as $k[x,y]$-algebras. To do this we need to know the right notion of “projective resolution” (it’s probably better to say cofibrant replacement), and we can build these from (retracts of) semifree commutative dg algebras in much the same way we build projective resolutions from free things! Here “semifree” means that our algebra is a free commutative graded algebra if we forget about the differential. Of course, “commutative” here is in the graded sense that $xy = (-1)^{\text{deg}(x) \text{deg}(y)}yx$. For example, if we work over the base field $k$, then the free commutative graded algebra on $x_0$ (by which I mean an element $x$ living in degree $0$) is just the polynomial algebra $k[x]$ all concentrated in degree $0$. Formally, we have elements $1, \ x_0, \ x_0 \otimes x_0, \ x_0 \otimes x_0 \otimes x_0, \ldots$, and the degree of a tensor is the sum of the degrees of the things we’re tensoring, so that for $x_0$ the whole algebra ends up concentrated in degree $0$. If we look at the free graded $k$-algebra on $x_1$, we again get an algebra generated by $x_1, \ x_1 \otimes x_1, \ x_1 \otimes x_1 \otimes x_1, \ldots$ except that now we have the anticommutativity relation $x_1 \otimes x_1 = (-1)^{1 \cdot 1} x_1 \otimes x_1$ so that $x_1 \otimes x_1 = 0$. This means the free graded $k$-algebra on $x_1$ is just the algebra with $k$ in degree $0$, the vector space generated by $x$ in degree $1$, and the stipulation that $x^2 = 0$. In general, elements in even degrees contribute symmetric algebras and elements in odd degrees contribute exterior algebras to the cga we’re freely generating. What does this mean for our example? We want to compute the derived tensor product of $k[x,y] \big / y$ and $k[x,y] \big / y-mx$. As is typical in homological algebra, all we need to do is “resolve” one of our algebras and then take the usual tensor product of chain complexes. Here a resolution means we want a semifree cdga which is quasi-equivalent to the algebra we started with, and it’s easy to find one! Consider the cdga $k[x,y,e]$ where $x,y$ live in degree $0$ and $e$ lives in degree $1$. The differential sends $de = y$, and must send everything else to $0$ by degree considerations (there’s nothing in degree $-1$). This cdga is semifree as a $k[x,y]$-algebra, since if you forget the differential it’s just the free graded $k[x,y]$ algebra on a degree 1 generator $e$! So this corresponds to the chain complex where $de = y$ is $k[x,y]$ linear so that more generally $d(pe) = p(de) = py$ for any polynomial $p \in k[x,y]$. If we tensor this (over $k[x,y]$) with $k[x,y] \big / y-mx$ (concentrated in degree $0$) we get a new complex where the interesting differential sends $pe \mapsto ey$ for any polynomial $p \in k[x,y] \big / y-mx$. Some simplification gives the complex whose homology is particularly easy to compute! $H_0 = k[x] \big / mx$ $H_1 = \text{Ker}(mx)$ We note that $H_0$ recovers our previous computation, where when $m \neq 0$ we have $H_0 = k$ is the coordinate ring of the origin3 and when $m=0$ we have $H_0 = k[x]$ is the coordinate ring of the $x$-axis. However, now there’s more information stored in $H_1$! In the generic case where $m \neq 0$, the differential $mx$ is injective so that $H_1$ vanishes, and our old “classical” computation saw everything there is to see. It’s not until we get to the singular case where $m=0$ that we see $H_1 = \text{Ker}(mx)$ becomes the kernel of the $0$-map, which is all of $k[x]$! The version of “dimension” for chain complexes which is invariant under quasi-isomorphism is the euler characteristic, and we see that now the euler characteristic is constantly $0$ for the whole family! Next let’s look at some kind of “hidden smoothness” by examining the singular curve $y^2 =x^3$. Just for fun, let’s look at another family of (affine) curves $y^2 = x^3 + tx$, which are smooth whenever $t \neq 0$. We’ll again show that in the derived world the singular fibre looks more like the smooth fibres. Smoothness away from the $t=0$ fibre is an easy computation, since we compute the jacobian of the defining equation $y^2 - x^3 - tx$ to be $\langle -3x^2 - t, 2y \rangle$, and for $t \neq 0$ this is never $\langle 0, 0 \rangle$ for any point on our curve4 (We’ll work in characteristic 0 for safety). Of course, when $t=0$ $\langle -3x^2, 2y \rangle$ vanishes at origin, so that it has a singular point there. To see the singularity, let’s compute the tangent space at $(0,0)$ for every curve in this family. We’ll do that by computing the space of maps from the “walking tangent vector” $\text{Spec}(k[\epsilon] \big / \epsilon^2)$ to our curve which deform the map from $\text{Spec}(k)$ to our curve representing our point of interest $(0,0)$. Since everything is affine, we turn the arrows around and see we want to compute the space of algebra homs so that the composition with the map $k[\epsilon] \big / \epsilon^2 \to k$ sending $\epsilon \mapsto 0$ becomes the map $k[x,y] \big / (y^2 - x^3 - tx) \to k$ sending $x$ and $y$ to $0$. Since $k[x,y] \big / (y^2 - x^3 - tx)$ is a quotient of a free algebra, this is easy to do! We just consult the universal property, and we find a hom $k[x,y] \big / (y^2 - x^3 - tx) \to k[\epsilon] \big / \epsilon^2$ is just a choice of image $a+b\epsilon$ for $x$ and $c+d\epsilon$ for $y$, so that the equation $y^2 - x^3 - tx$ is “preserved” in the sense that $(c+d\epsilon)^2 - (a+b\epsilon)^3 - t(a+b\epsilon)$ is $0$ in $k[\epsilon] \big / \epsilon^2$. Then the “deforming the origin” condition says that moreover when we set $\epsilon = 0$ our composite has to send $x$ and $y$ to $0$. Concretely that means we must choose $a=c=0$ in the above expression, so that finally: The tangent space at the origin of $k[x,y] \big / (y^2 - x^3 - tx)$ is the space of pairs $(b,d)$ so that $(d \epsilon)^2 - (b \epsilon)^3 - t(b \epsilon) = 0$ in $k[\epsilon] \big / \epsilon^2$. Of course, this condition holds if and only if $tb=0$, so that: When $t \neq 0$ the tangent space is the space of pairs $(b,d)$ with $b=0$, which is one dimensional. When $t = 0$ the tangent space is the space of pairs $(b,d)$ with no further conditions, which is two dimensional! Since we’re looking at curve, we expect the tangent space to be $1$-dimensional, and this is why we say there’s a singularity at the origin for the curve $y^2 = x^3$….. But what happens in the derived world? Now we want to compute the derived homspace. As before, a cofibrant replacement of our algebra is easy to find, it’s just $k[x,y,e]$ where $x$ and $y$ have degree $0$, $e$ has degree $1$ and and $de = y^2 - x^3 - tx$. Note that in our last example we were looking at quasifree $k[x,y]$-algebras, but now we just want $k$-algebras! So now this is the free graded $k$-algebra on 3 generators $x,y,e$, and our chain complex is: We want to compute the derived $\text{Hom}^\bullet(-,-)$ from this algebra to $k[\epsilon] \big / \epsilon^2$, concentrated in degree $0$. The degree $0$ maps are given by diagrams that don’t need to commute5! Of course, such maps are given by pairs $(a + b \epsilon, c + d \epsilon)$, which are the images of $x$ and $y$. As before, since we want the tangent space at $(0,0)$ we need to restrict to those pairs with $a=c=0$ so that $\text{Hom}^0(k[x,y] \big / y^2 - x^3 - tx, \ k[\epsilon] \big / \epsilon^2) = k^2$, generated by the pairs $(b,d)$. Next we look at degree $-1$ maps, which are given by diagrams which are given by a pair $r + s\epsilon$, the image of $e$. Again, these need to restrict to the $0$ map when we set $\epsilon=0$, so that $r=0$ and we compute $\text{Hom}^{-1}(k[x,y] \big / y^2 - x^3 - tx, \ k[\epsilon] \big / \epsilon^2) = k$, generated by $s$. So our hom complex is where the interesting differential sends degree $0$ to degree $-1$ and is given by $df = d_{k[\epsilon] \big / \epsilon^2} \circ f - f \circ d_{k[x,y] \big / y^2-x^3-tx}$. So if $f$ is the function sending $x \mapsto b \epsilon$ and $y \mapsto d \epsilon$ then we compute So phrased purely in terms of vector spaces we see our hom complex is (living in degrees $0$ and $-1$): So we compute $H^0 = \text{Ker} ((-t \ 0))$ $H^{-1} = \langle s \rangle \big / \text{Im}((-t \ 0))$ When $t \neq 0$, our map is full rank so that $H^0$ are the pairs $(b,d)$ with $b=0$ – agreeing with the classical computation. Then $H^{-1} = 0$, so again we learn nothing new in the smooth fibres. When $t=0$, however, our map is the $0$ map so that $H^0$ is the space of all pairs $(b,d)$ is two dimensional – again, agreeing with the classical computation! But now we see the $H^{-1}$ term, which is $1$ dimensional, spanned by $s$. Again, in the derived world, we see the euler characteristic is constantly $1$ along the whole family! There’s something a bit confusing here, since there seem to be two definitions of “homotopical smoothness”… On the one hand, in the noncommutative geometry literature, we say that a dga $A$ is “smooth” if it’s perfect as a bimodule over itself. On the other hand, though, I’ve also heard another notion of “homotopically smooth” where we say the cotangent complex is perfect. I guess it’s possible (likely?) that these should be closely related by some kind of HKR Theorem, but I don’t know the details. Anyways, I’m confused because we just computed that the curve $y^2 = x^3$ has a perfect tangent complex, which naively would make me think its cotangent complex is also perfect. But this shouldn’t be the case, since I also remember reading that a classical scheme is smooth in the sense of noncommutative geometry if and only if it’s smooth classically, which $y^2 = x^3$ obviously isn’t! Now that I’ve written these paragarphs and thought harder about things, I think I was too quick to move between perfectness of the tangent complex and perfectness of the cotangent complex, but I should probably compute the cotangent complex and the bimodule resolution to be sure… Unfortunately, that will have to wait for another day! I’ve spent probably too many hours over the last few days writing this and my other posts on lie algebroids. I have some kind of annoying hall algebra computations that are calling my name, and I have an idea about a new family of model categories which might be of interest… But checking that something is a model category is usually hard, so I’ve been dragging my feet a little bit. Plus, I need to start packing soon! I’m going to europe for a bunch of conferences in a row! First a noncommutative geometry summer school hosted by the institute formerly known as MSRI, then CT of course, and lastly a cute representation theory conference in Bonn. I’m sure I’ll learn a bunch of stuff I’ll want to talk about, so we’ll chat soon ^_^. Take care, all! In fact we know more! This $k$ is really $k[x,y] \big / (x=0,y=0)$, so we know the intersection point is $(0,0)$. ↩ Indeed after tensoring we get since here $k \cong k[m] \big / (m)$. But then we can simplify these to and indeed the leftmost map (multiplication by $m$) is not injective! The kernel is generated by $x$. ↩ Again, if you’re more careful with where this ring comes from, rather than just its isomorphism class, it’s $k[x,y] \big / (x,y)$, the quotient by the maximal ideal $(x,y)$ which represents the origin. ↩ The only place it could possibly be $\langle 0, 0 \rangle$ is when $y=0$, but the points on our curve with this property satisfy $x^3-tx=y^2=0$ so that when $t \neq 0$ the solutions are $(x,y) = (0,0), \ (\sqrt{t}, 0), \ (-\sqrt{t}, 0)$. But at all three of these points $\langle -3x^2 - t, 2y \rangle \neq \langle 0, 0 \rangle$. ↩ This is a misconception that I used to have, and which basically everyone I’ve talked to had at one point. Remember that dg-maps are all graded maps! Not just those which commute with the differential! The key point is that the differential on $\text{Hom}^\bullet(A,B)$ sends a degree $n$ map $f$ to so that $df = 0$ if and only if $d_B f = (-1)^n f d_A$ if and only if $f$ commutes with the differential (in the appropriate graded sense). This means that, for instance, $H^0$ of the hom complex recovers from all graded maps exactly $\text{Ker}(d) \big / \text{Im}(d)$, which are the maps commuting with $d$ modulo chain homotopy! ↩

While doing a computation with my friend Shane the other day, we realized we needed to explicitly compute a local chart near the identity of $SL_2(\mathbb{R})$. It took us longer than I’d like to admit to figure out how to do this (especially since it’s so geometrically obvious in hindsight), and so I want to write down the process for future grad students looking to just do a computation! If you want to see what Shane and I were actually interested in, you can check out the main post here. Ok, let’s hop right in! Say you have a $2$-manifold in $\mathbb{R}^3$ to start1: If we think of the purple manifold $M$ as being an open disk, representing a small neighborhood of some possibly larger 2-manifold, then we can see the projection onto the $xy$-plane is a diffeomorphism onto its image (an open disk in $\mathbb{R}^2$) while the projections onto the $yz$ and $xz$ planes are not open in $\mathbb{R}^2$! This is because the normal to $M$ is parallel to the $z$ axis inside $M$, (indeed, at the “top of the hill”) so the tangent plane at that point degenerates and projects to a line whenever we project onto a coordinate plane containing the $z$-direction. For a more computational example, let’s try the hyperboloid $x^2 + y^2 - z^2 = 1$, and let’s see what happens near a few points. The tangent plane at a point is controlled by the jacobian of the defining equation, which for us is $\langle 2x, 2y, -2z \rangle$. This gives us three (disconnected) charts: \(\{2x \neq 0\}\), \(\{2y \neq 0\}\), and \(\{-2z \neq 0\}\), which we can see visually here (and we also drop the unnecessary scalars): These turn into 6 honest-to-goodness charts where we turn the disconnected condition \(\{x \neq 0\}\) into the pair of connected conditions \(\{x \gt 0\}\) and \(\{x \lt 0\}\). Indeed it’s easy to see that the 6 connected components in the above pictures are all diffeomorphic to an open subset of $\mathbb{R}^2$, and we can see this algebraically by projecting onto the plane avoiding the nonzero coordinate. On \(\{x \gt 0 \}\), for example, we have an open set of the $yz$-plane, shown here in orange: Algebraically, we compute this chart by noting on \(\{x \gt 0 \}\), we can solve for $x$ and (using the positive square root, since $x \gt 0$) write our surface locally as which is diffeomorphic in the obvious way to its projection onto the $yz$-plane so this is one of our charts! Similarly, we can look at \(\{z \gt 0\}\), solve for $z$ and locally write our surface as which is diffeomorphic to \(\{ (x,y) \mid x^2 + y^2 \gt 1 \}\) – another chart. On the intersection of these charts, \(\{x, z \gt 0 \}\), it’s now easy to write down our transition maps (if one is so inclined): Here our charts are the diffeomorphisms so it’s easy to compose them to see our transition maps between these charts are As a (fun?) exercise, compute the \(\{y \gt 0 \}\) chart, and the other two transition maps. For another example, let’s take a look at $SL_2(\mathbb{R})$, which is defined to be \(\left \{ \begin{pmatrix} a & b \\ c & d \end{pmatrix} \mid ad-bc = 1 \right \} \subseteq \mathbb{R}^4\). Then the jacobian of our defining map is $\langle d, -c, -b, a \rangle$, and we get charts corresponding to \(\{d \neq 0 \}\), \(\{-c \neq 0 \}\), \(\{ -b \neq 0 \}\), and \(\{ a \neq 0 \}\). In the \(\{d \neq 0\}\) chart, for instance, our defining equation looks like $a = \frac{1+bc}{d}$, so that $SL_2(\mathbb{R})$ looks locally like In the main post you can see how my friend Shane and I used this to compute the anchor map for a certain lie algebroid. Again, it makes a nice exercise to explicitly write out the various charts and transition maps What about a codimension 2 example? Let’s go back to our happy little hyperboloid, and intersect it with the surface $xyz = 1$. That is, we want to consider the manifold This is the levelset of the map $\mathbb{R}^3 \to \mathbb{R}^2$ sending $(x,y,z) \mapsto (x^2 + y^2 - z^2, \ xyz)$ taking value $(1,1)$. So we compute the jacobian and our charts are all the ways this matrix can have full rank. These conditions are: $2x \neq 0$ and $xz \neq 0$ $2x \neq 0$ and $xy \neq 0$ $2y \neq 0$ and $yz \neq 0$ $2y \neq 0$ and $xy \neq 0$ $-2z \neq 0$ and $yz \neq 0$ $-2z \neq 0$ and $xz \neq 0$ If we look at the \(\{2x \neq 0, \ xz \neq 0\}\) chart, we can ask sage to solve for $x$ and $z$ as functions of $y$: So as in the previous hyperboloid example, we need to break this into four charts, depending on whether $x$ and $z$ are positive or negative. Following the sage computation, in the \(\{x \gt 0, z \gt 0\}\) chart, we can write our curve as which, by projecting out the $y$ coordinate, is diffeomorphic to the open subset of $\mathbb{R}$ where all these square roots are defined. Ok, thanks for reading, all! This was extremely instructive for me, and hopefully it’s helpful to some of you as well! Sometimes it’s nice to just do some computations. Talk soon! That’s right. I finally bought an ipad. This has already dramatically improved my paper-reading experience (I love you Zotero) and my remote teaching experience, and I’m so glad that the example-drawing experience is shaping up to be everything I wanted it to be as well! ↩

The other day my friend Lucas Salim was asking me some questions about categorical logic and constructive math, and he mentioned he’d never seen a proof that there’s no constructive proof of the intermediate value theorem before. I showed him the usual counterexample, and since my recent blog post about choice was so quick to write I decided to quickly write up a post about this too, since I remember being confused by it back when I was first learning it. The key fact is Soundness and Completeness of the topos semantics of constructive logic. This says that there is a way of interpreting the usual syntax of mathematics into a topos in such a way that (Soundness) If you can constructively prove a statement, then its interpretation in every topos is true (Completeness) If a statement is interpreted as true in every (elementary1) topos, then there must exist a constructive proof For a proof, see Chapter II of Lambek and Scott’s Introduction to Higher Order Categorical Logic or Section D4.3 of The Elephant. This means that as long as we’re careful to avoid choice and excluded middle, anything we prove will be true when interpreted in any topos we like! Then there’s a mechanical procedure that lets us convert this interpretation into a corresponding statement in the “real world2”, and this gives us lots of “theorems for free” for each individual constructive theorem! A nice case study is given by the Wierstrass Approximation Theorem, which I gave a talk on years ago3. Since this theorem is constructively provable4… by interpreting it in the effective topos we learn there’s a computer program $\mathtt{Approx}$ which takes as input a function $f : [0,1] \to \mathbb{R}$5 and an $\epsilon \gt 0$ and outputs the coefficients of a polynomial approximating $f$. by interpreting it in a sheaf topos $\text{Sh}(\Theta)$ we learn that for any continuous family of functions $f_\theta(x) : \Theta \times [0,1] \to \mathbb{R}$, there’s locally6 a polynomial $p_\theta(x)$ whose coefficients are continuous functions of $\theta$ which approximates each $f_\theta(x)$ etc. If you’re interested in learning how to externalize a statement in a topos to a statement about the real world, I highly recommend Ingo Blechschmidt’s excellent paper Exploring mathematical objects from custom-tailored mathematical universes which gives a high level overview of the topic, while still giving enough details to let you externalize a few statements of your own! But where were we? The usual proofs of the intermediate value theorem aren’t constructive. See, for instance, Bauer’s Five Stages of Accepting Constructive Mathematics or Section 1 of Taylor’s A Lambda Calculus for Real Analysis for a discussion of how some common proofs fail (as well as great lists of constructively provable alternatives). Since the usual proofs seem to fail, we might guess that IVT is not provable constructively… but how could we prove this? Say, towards a contradiction, that there were a constructive proof of the intermediate value theorem. Then it would be true in every topos, and thus its various externalizations would all be true in the real world. So to show that there isn’t a constructive proof, all we have to do is find a topos which doesn’t think it’s true! Following many who came before me7, we’re going to use the topos of sheaves on $(-1,1)$. It’s been a minute since we’ve externalized a statement together, so let’s do it now! In full symbolic glory, the IVT says So now using the forcing language for $\text{Sh}((-1,1))$ (check out Theorem $1$ in Chapter VI.7 of Mac Lane and Moerdijk’s Sheaves in Geometry and Logic if you’re not sure what this means), we compute: We cash out the universal quantifiers to get “for every open $U \subseteq (-1,1)$, and for every continuous $f : U \times \mathbb{R} \to \mathbb{R}$, $a : U \to \mathbb{R}$, $b : U \to \mathbb{R}$, we have…” Next, cashing out the implication gives “for every open $U \subseteq (-1,1)$, and for every continuous $f : U \times \mathbb{R} \to \mathbb{R}$, $a : U \to \mathbb{R}$, $b : U \to \mathbb{R}$, so that for all $t \in U$ we know $a(t) \lt b(t)$, $f(t,a(t)) \lt 0$, and $f(t,b(t)) \gt 0$, we have…” Finally, cashing out the existential quantifer and the stuff inside it we get the external statement: The IVT is true inside $\text{Sh}((-1,1))$ if and only if the following is true externally: For every open $U \subseteq (-1,1)$ What a mouthful! Of course, we’re trying to prove this fails, so all we have to do is find an open set $U$ and functions $f$, $a$, and $b$ satisfying the assumptions so that the conclusion fails. We’ll choose $U = (-1,1)$ to be the whole set, $a(t) = -2$ and $b(t) = 2$ to be constant functions, and $f(t,x) : (-1,1) \times \mathbb{R} \to \mathbb{R}$ to be Then we see that, indeed, $f(t,a) \lt 0$ and $f(t,b) \gt 0$ for all $t \in (-1,1)$, so to prove the IVT fails in this topos we just need to show there’s no open cover on which $x(t)$ with $f(t,x(t)) = 0$ can be chosen continuously. The idea is that no matter how hard we try, $x(t)$ cannot be continuous in a neighborhood of $t=0$. Indeed, here’s an animation showing how $x(t)$ changes as we change $t$: You can see that when $t=0$ the root $x(t)$ jumps between $\pm 1$! Indeed, if we plot $x(t)$ we get: and it’s obvious that this is not the graph of a continuous function in any neighborhood of $t=0$. As long as we’re showing pretty graphics, you can also visualize this whole function $f$ as a surface over the strip $(-1,1) \times \mathbb{R}$. Then choosing a $t$ amounts to choosing a “slice” of the surface, and we can see that where that slice intersects the $(t,x)$-plane jumps suddenly as we cross $t=0$. In this example the axes are labeled $x$ and $y$ rather than $x$ and $t$: So where did we start, and where did we end? If the IVT were constructively provable, it would be true inside $\mathsf{Sh}((-1,1))$ and thus for our $f(t,x)$ we could find an open cover on which the zero $x(t)$ varies continuously in $t$. But this can’t possibly happen in a neighborhood of $t=0$, so we learn there is no constructive proof! Buuuuut, all is not lost! Usually classical theorems do have constructive analogues, either by adding new assumptions, weakening the conclusion, or by finding a different statement of the theorem that’s more positive. Andrej Bauer’s paper Five Stages of Accepting Constructive Mathematics lists many possibilities. For instance, one way to weaken the conclusion is to prove that for any $\epsilon$ you like, there’s an $x$ with $|f(x)| \lt \epsilon$. In our example, if we plot those $x$ so that $|f(t,x)| \lt \epsilon$ we get and it’s easy to fit the graph of a continuous selection function $x(t)$ inside this thickened region. Another approach is to recognize that the problem comes from $f$ “hovering” at $0$ when $t=0$. If we forbid this hovering, for instance by assuming $f$ is strictly monotone, then we can constructively prove the IVT (See Bauer’s Five Stages paper again). There’s yet another version, coming from Abstract Stone Duality, where we say that whenever $f(a) \lt 0 \lt f(b)$, the compact subspace $Z_f = { x \in [a,b] \mid f(x) = 0 }$ is occupied (Cor 13.11 in A Lambda Calculus for Real Analysis). This is a condition that’s weaker than inhabited but stronger than nonempty, which you can read about in Section 8 of the same paper. I don’t understand this condition very well, because I haven’t spent as much time thinking about ASD as I would like. Hopefully sometime soon I’ll find some time to work through some examples! Ok, thanks for reading, all! It’s nice to get a few quick posts up while I’m working on some longer stuff. I’m still thinking a lot about a cool circle of ideas involving Fukaya Categories, Skein Theory and T(Q)FTs, and Hall Algebras, and I’m slowly making progress on writing posts about all these fun things. Now, though, I have to go run a review session for a calculus class, haha. I’ll try to resist telling them about the fascinating subtleties that show up when you try to do everything constructively. Stay safe, and we’ll talk soon 💖 Usually on this blog when I talk about topoi I mean grothendieck topoi, but for this completeness result we really do need to allow more general elementary topoi with NNO. Indeed there are statements true in all grothendieck topoi that are not constructively provable (since they fail in some elementary topos). See here for a partial list. I would actually love to know if there’s a reference for what one has to add to IHOL to get something sound and complete for grothendieck topoi… I spent some time looking, but the only thing I found was Topological Completeness for Higher-Order Logic by Awodey and Butz, but it seems like they use $1+1$ in place of $\Omega$, so this isn’t the usual interpretation of logic in a grothendieck topos (which is also where the classical completeness comes from). ↩ Maybe “base topos” would be less philosophically charged ↩ I was really fumbling around with topos theory back then, haha. I’m much more confident now, and in the last few years I’ve just worked through a lot more examples and done more computations and read more papers and generally just learned a lot. Rereading that post was surprisingly… nostalgic isn’t the right word… but it’s fun to see how much I’ve grown! ↩ The usual proof with bernstein polynomials works if we’re careful to check some constructively relevant details. I’ll copy it here in case the wikipedia article changes someday: Fix $\epsilon > 0$. We write $b_{k,n}(x) = \binom{n}{k} x^k (1-x)^{n-k}$, and note that: $\sum_{k=0}^n b_{k,n} = 1$ $\sum_{k=0}^n \left ( x - \frac{k}{n} \right )^2 b_{k,n} = \frac{x(1-x)}{n}$ These are all provable by just expanding the left hand side, which is constructive. We also fix a $\delta$ so that whenever $|x-y| \lt \delta$ we have $|f(x) - f(y)| \lt \epsilon$. This is because, constructively, every continuous function on a compact sublocale of $\mathbb{R}$ is uniformly continuous. Note that here we crucially need to be working with locales! (see, eg, Thm 10.7 in Taylor’s A Lambda Calculus for Real Analysis) Lastly, we fix $M$ an upper bound for $\lvert f \rvert$. This is possible since $[0,1]$ is compact, overt, and inhabited (see Rmk 10.4 in Bauer and Taylor’s The Dedekind Reals in Abstract Stone Duality) thus the continuous $\lvert f \rvert$ admits a maximum (Thm 12.9 in A Lambda Calculus for Real Analysis). Now let $B_n f = \sum_{k=0}^n f(k/n) b_{k,n}$. We compute: In step (a) we use (1), and in step (b) we use the fact that $\forall x \in \mathbb{R} . x \lt \delta \lor x \gt \frac{\delta}{2}$ is constructively true (since the intervals overlap we don’t need excluded middle here!) But we can bound the first sum by noticing in this region $|x-k/n| \lt \epsilon$ so that (using (1) again) And since $\lvert f(x) - f(k/n)\rvert \leq \lvert f(x) \rvert + \lvert f(k/n) \rvert \leq 2M$, we compute: In step (c) we use $|x - k/n| \gt \frac{\delta}{2}$ to say that $\left ( \frac{\delta}{2} \right )^{-2} \left ( x - \frac{k}{k} \right )^2 \geq 1$, so that we can multiply through by it and make our sum bigger. In step (d) we use (2), and at the end we use the fact that $x(1-x) \leq \frac{1}{4}$ on $[0,1]$. Now since $\mathbb{R}$ is constructively archimedian (Defn. 1.1 in The Dedekind Reals in Abstract Stone Duality) we see $\exists n \in \mathbb{N} . \frac{2M}{\delta^2n} \lt \epsilon$. Since these bounds were uniform in $x$, we learn that as desired. ↩ A real number $x$ in this topos is a program that eats a natural number $n$ and outputs a rational number $x(n)$. We think about this as a sequence of rational approximations $x(n)$ converging to some real number $x$. So a function $[0,1] \to \mathbb{R}$ in this topos is a program that takes as input a program $x$ (outputting rational approximations between $0$ and $1$) and outputs a new program $f(x)$ which outputs rational approximations. ↩ Because our statement of Weierstrass $\forall \epsilon . \forall f . \exists p . \lVert f - p \rVert_\infty \lt \epsilon$ includes an existential quantifier there’s no way to get around the fact that the $p$ we build is only defined locally on an open cover. If you were more careful and gave a type theoretic proof that $\prod_\epsilon \prod_f \sum_p \lVert f - p \rVert_\infty \lt \epsilon$ then you could take $p$ to be a single polynomial defined on the whole of $\Theta$… I haven’t thought very hard about how possible this is (mainly because I haven’t spent much time thinking about what theorems about locales are provable in type theory), but I’m sure a talented undergraduate could figure it out. ↩ The earliest version of this example which I’ve seen comes from Stout’s Topological Properties of the Real Numbers Object in a Topos back in 1976. I think basically every other paper I’ve cited in this post gives some version of this example too, so it’s very well trodden ground! ↩

A few days ago I saw a cute question on mse asking about a particularly non-intuitive failing of the axiom of choice. I remember when I was an undergrad talking to a friend of mine about various statements equivalent to choice, and being particularly hung up on the same statement that OP asks about – The product of nonempty sets is nonempty. I understood that there were models where the axiom of choice fails, and so in those models we must have some family of nonempty sets whose product is, somehow, empty! Now that I’m older and I’ve spent much more time thinking about these things, this is less surprising to me, but reading that question reminded me how badly I once wanted a concrete example, and so I’ll share one here! This should be a pretty quick post, since I’ll basically just be fleshing out my answer to that mse question. But I think it’ll also be nice to have here, since these things can be hard to find when you’re first getting into logic and topos theory! Let’s get to it! First, let’s remember that for any group $G$ the category $G\text{-}\mathsf{Set}$ of sets equipped with a $G$-action is a topos. Indeed you can see it as a presheaf topos, since $G\text{-}\mathsf{Set}$ is equivalent to the category of functors from $G \to \mathsf{Set}$ (viewing $G$ as a one-object category). We’ve talked about this topos before, and it’s wild to think how far I’ve come since writing that post! The basic idea of $G\text{-}\mathsf{Set}$ as a topos is that any set theoretic construction we do to some $G$-sets again gives us $G$-sets! For instance, any (co)limits of $G$-sets will have a natural $G$-action. If $X$ is a $G$-set then its powerset $\mathcal{P}(X)$ has a $G$-action where if $A \in \mathcal{P}(X)$ we define \(g \cdot A = \{g \cdot a \mid a \in A \}\), which is another element of $\mathcal{P}(X)$. If $X$ and $Y$ are $G$-sets then the set of functions $X \to Y$ is again a $G$-set where we say $(g \cdot_{X \to Y} f)(x) = g \cdot_Y f(g^{-1} \cdot_X x)$. In particular, we can recover the “$G$-equivariant” constructions as the global elements! So even though $\mathcal{P}(X)$ contains all subsets of $X$ (not just the $G$-invariant subsets), if we look at the global elements (that is the maps $1 \to \mathcal{P}(X)$) we do get exactly the $G$-invariant subsets. Similarly while the set of functions $X \to Y$ sees all functions, the global elements of this set will pick out exactly the $G$-equivariant functions. But $G\text{-}\mathsf{Set}$ has a coreflective subcategory given by those $G$-sets all of whose orbits are finite. The coreflector takes a $G$-set and just deletes all the infinite orbits, so we have an adjunction which gives us a comonad $\iota R$ on $G\text{-}\mathsf{Set}$. This comonad is idempotent, and its category of coalgebras is equivalent to \(G\text{-}\mathsf{Set}_\text{finite orbits}\). Then since $\iota$ is left exact (and so is $R$, since it’s a right adjoint), we see that \(G\text{-}\mathsf{Set}_\text{finite orbits}\) is the category of coalgebras for a lex comonad on a topos, thus is itself a topos! As a cute exercise, check that $\iota$ really is left exact! Now doing computations in this topos is pretty easy! Finite limits and arbitrary colimits are computed as in $G\text{-}\mathsf{Set}$ since $\iota$ preserves these. Arbitrary limits and exponentials $Y^X$ come from coreflecting – that is $Y^X$ as computed in \(G\text{-}\mathsf{Set}_\text{finite orbits}\) is just what we get by removing the infinite orbits from $Y^X$ as computed in $G\text{-}\mathsf{Set}$, and similarly for limits. The subobject classifier is just the usual set of truth values \(\{ \top, \bot \}\) with the trivial $G$-action1. In particular this topos is boolean, so set theory inside it is particularly close to the usual ZF set theory. Now with this in mind, we can prove the main claim of this post: In $\mathbb{Z}\text{-}\mathsf{Set}_\text{finite orbits}$, let $C_n$ be $\mathbb{Z}/n$ with its obvious $\mathbb{Z}$-action. Then each $C_n$ is inhabited2 in the sense that $\exists x . x \in C_n$, and yet \(\prod_n C_n = \emptyset\)! So this topos shows explicitly how, in the absence of choice, you can have a family of nonempty sets3 whose product is somehow empty! The computation is actually quite friendly! To compute $\prod_n C_n$ in this topos, we first compute the product in the category of all $\mathbb{Z}$-sets, then throw away any infinite orbits. But it’s easy to see that every orbit is infinite! Any element of the product will contain an element from every $C_n$, so that in any finite number of steps some large entry in this tuple won’t be back where it started. Ok, this one was actually quite quick, which I’m happy about! My parents are visiting soon, and I’m excited to take a few days to see them ^_^. I have another shorter post planned which another grad student asked me to write, and I’ve finally actually started the process of turning my posts on the topological topos into a paper. I’m starting to understand TQFTs better, and it’s been exciting to learn a bit more physics. Hopefully I’ll find time to talk about all that soon too, once I take some time to really organize my thoughts about it. Thanks for hanging out, all! Stay safe, and we’ll talk soon. In case $G = \mathbb{Z}$ then it’s a kind of cute fact that this topos is equivalent to the topos of continuous (discrete) $\widehat{\mathbb{Z}}$-sets, where $\widehat{\mathbb{Z}}$ is the profinite completion of $\mathbb{Z}$. See, for instance, Example A2.1.7 on page 72 of the elephant. This gives another computationally effective way to work with this topos! I’m pretty sure I convinced myself that more generally the category of $G$-sets all of whose orbits are finite should be equivalent to the category of continuous discrete $\widehat{G}$-sets, but I haven’t thought hard enough about it to say for sure in a blog post. ↩ Of course, there’s no global points for $n \neq 1$, since maps $1 \to C_n$ correspond to fixed points. But existential quantification is local, so that the topos models $\exists x \in C_n . \top$ if there’s some surjection $V \twoheadrightarrow 1$ and a map $V \to C_n$. We can take $V = \mathbb{Z}$ with its left multiplication action on itself, and there is a map from $\mathbb{Z} \to C_n$. If you’re more used to type theory, we don’t have $\Sigma_{x : C_n} \top$, since that would imply a global element. But despite this, we do have the propositional truncation $\lVert \Sigma_{x : C_n} \top \rVert$, so that an element of $C_n$ merely exists. ↩ Since this topos is boolean, nonempty and inhabited are actually synonyms here. Moreover, this “nonempty” is closer to how a lot of working mathematicians speak, so it felt right to use this wording here. ↩