#topostheory — Public Fediverse posts

this paper is so nice, the sweet spot between cool and accessible, so many gems! #topostheory

https://arxiv.org/abs/2503.04317

I guess I'm becoming a fan of Hora's work

Here's a cute #Puzzle for anyone interested in improving their #ToposTheory

Fix a topological space X. The statement
"the (dedekind) reals are cauchy complete"
internal to the topos of sheaves on X, externalizes to the familiar statement that
"a uniform limit of continuous functions on X is continuous"

1. Do you see why this might be true "on vibes"? Depending on how long you've been doing this, you may find your vibes very easy to turn into an honest proof... or very hard. See, for instance, @tao's old blog post

https://terrytao.wordpress.com/career-advice/theres-more-to-mathematics-than-rigour-and-proofs/

2. Can you do the externalization in order to check this precisely?

You'll want to use a "type theoretic" version of cauchy completeness (using Σ-types rather than ∃-quantifiers) so that the resulting statement stays global. Do you see why using ∃ instead would externalize to a weaker claim (that the limit function only has to be defined locally)?

3. This one is harder. Can you prove, type theoretically, that the dedekind reals are cauchy complete? I don't know a way to do it without getting your hands dirty and building the correct dedekind cuts, but this sounds harder than it actually is.

You can also find a complete proof here if you want inspiration:

https://planetmath.org/1122dedekindrealsarecauchycomplete

---

As always, feel free to boost, and reply to this with ideas and questions! I'm excited to see what people come up with ^_^

#math #CategoryTheory

Is there a constructive definition of 'finite set' which when applied to the topos of ℤ-sets, gives the actions of ℤ on finite sets?

I had a look at the nLab page on finite sets (https://ncatlab.org/nlab/show/finite+set), but I think all of the definitions there consider e.g. {n∈ℕ|n<7} to be finite. Which isn't what I want, because in ℤ-Set that object is the action of ℤ on seven copies of ℤ.

#CategoryTheory #ToposTheory

This Saturday is the grand opening of the Grothendieck Institute https://igrothendieck.org/
The Institute's goal is partly to promote topos theory and its applications, partly to study the still unpublished writings of Alexandre Grothendieck.
(Via Olivia Caramello's blog https://aroundtoposes.com/grothendieck-institute/)
#Grothendieck #ToposTheory

On my #blog , in which I try to write pithy summaries of major papers and books in my field, I attempt to say something meaningful in minimal space about the monumental 'Sketches of an Elephant' https://updatedscholar.blogspot.com/2022/11/discussing-sketches-of-elephant-topos.html #CategoryTheory #ToposTheory #topos #HigherOrderLogic

Didn't manage to get a #blog post up this week. In my defence, these books are hard work, even to skim! #topostheory #categorytheory