Ingo Blechschmidt
-
Member for 11 years, 10 months
-
Last seen more than a week ago
-
GitHub
-
Augsburg, Germany
comment
Reference request about “internal language of categories”
Welcome to MO, Gennaro! I'm not sure I understand the question. Are you familiar that the internal $\wedge$ corresponds to intersection of subobjects, that the internal $\vee$ corresponds to join of subobjects and so on?
comment
The real numbers object in Sh(Top)
Just to confirm, I agree that we don't need sobriety. Without any condition on $Y$, the following notions coincide: (1) continuous maps from $Y$ to the topological space of Dedekind reals, (2) locale-theoretic morphisms from $Y$, now considered as a locale, to the locale of Dedekind reals, (3) geometric morphisms from $\mathbf{Sh}(Y)$ to the topos of Dedekind reals. (If classical logic is available, then this topos coincides with the topos of sheaves over the topological space of Dedekind reals. If not, we can use the classifying topos of Dedekind reals as a substitute for that sheaf topos.)
comment
Construction of the petit Zariski topos out of the gros topos of a scheme
The fpqc and fppf topologies coincide in the case that the site only contains schemes which are (locally) of finite presentation. Without this finiteness condition, not even the big Zariski topos will classify any reasonable theory. That said, the big fppf topos classifies fppf-local rings (Definition 21.4 in the linked notes). Conjecturally, these are the same as algebraically closed local rings. Hence the big fppf topos is the largest subtopos of the big Zariski topos where $\mathbf{A}^1$ is fppf-local. The answer for the Nisnevich topology is to the best of my knowledge unknown.
comment
Construction of the petit Zariski topos out of the gros topos of a scheme
@Dean: The morphisms in $C$ are not what we might expect: Their ring-theoretic parts are required to be isomorphisms instead of local homomorphisms (as would be the case in the category of locally ringed spaces). The Spec functor is indeed an adjoint, if we let it map to the category of locally ringed toposes (objects are pairs $(\mathcal{E},\mathcal{O}_\mathcal{E})$, morphisms are pairs $(f:\mathcal{E}\to\mathcal{F}, f^\sharp:f^{-1}\mathcal{O}_\mathcal{F}\to\mathcal{O}_\mathcal{E})$), see for instance Sect. 12 of these notes.
comment
Classifying Space of "Valuation Ringed Spaces over a Topos"
I'm eagerly following Peter's notes! Is the definition of a condensed scheme already public? I can't find it in the notes.
Loading…
comment
The 'gros' functor from schemes into (strictly) locally ringed topoi
You circumvent this problem by defining schemes to be certain objects in $\mathrm{Sh}(\mathbf{Et})$, but let me remark for the benefit of others that the functor from schemes-as-usually-defined to $\mathrm{Sh}(\mathbf{Et})$ is not fully faithful if $\mathbf{Et}$ is defined, as in your post, using only finitely presented rings. For instance, the functor of points of $\mathrm{Spec}(\mathbb{Q})$ coincides with the functor of points of the empty scheme.
comment
The (co)tangent sheaf of a topological space
Just a comment, in the smooth situation, there is a third sheaf we could consider, namely the sheaf of Kähler differentials (as in algebraic geometry). This sheaf does not coincide with the sheaf of (correct) differential forms, but the dual of that sheaf is $T_X$ (with $\mathcal{O}_X$ the sheaf of smooth functions) and the dual of $T_X$ is the sheaf of (correct) differential forms.
comment
Does this "mixable" property have a standard name in constructive mathematics?
Regarding the history of the term: Already in 1990 Anders Kock used the term "flabby" for the property in question (Algebras for the partial map classifier monad in Category Theory. Proceedings of the International Conference held in Como, Italy, July 22–28, 1990). However, he didn't give an explanation for his choice of terminology. It might be that the connection to flabby sheaves has been known for a long time but never written down.
comment
Does this "mixable" property have a standard name in constructive mathematics?
The argument in your edit is precisely what I had in mind, sorry for not spelling it out on the nLab page. By the way, most applications of Zorn in mathematical practice require a touchup by LEM, that is, they go like this: "By Zorn's lemma, there is a maximal element. Assume that it does not have the desired property. Then by <some-argument>, we can extend it to a larger element. This contradicts maximality." But here no LEM is necessary. This is relevant because if your metatheory satisfies Zorn, then so will any localic topos, while LEM is just false in most localic toposes.
comment
Constructivist defininition of linear subspaces of $\mathbb{Q}^n$?
continued Constructive results are more widely applicable than classical results, for instance because they also hold "in the internal universe of any topos", and your question provides a nice illustration. Namely, the easy theorem "any finitely generated vector space is not not finite dimensional" implies the (morally still easy, but now encumbered with a nontrivial amount of technicalities rendering it not really easy) theorem "any sheaf of finite type over a reduced scheme is finite locally free on a dense open subset". If you are intrigued by this, then let's chat over mail!
comment
Constructivist defininition of linear subspaces of $\mathbb{Q}^n$?
Let me add a comment, employing the terminology of Simon's comment. Over the rationals, we can constructively prove that a subspace is finitely generated iff it is finite dimensional. Over other fields, this might fail; however, it's still the case that any finitely generated subspace is not not finite dimensional. Constructively, this is a strictly weaker statement; it is common that some classical results can be verified constructively if prefixed with a double negation (there are general metatheorems explaining this phenomenon). continuing
comment
Is there any physical or computational justification for non-constructive axioms such as AC or excluded middle?
There are also general metatheorems showing that, for many but not all cases, the axiom of choice and the law of excluded middle are redundant. For instance, we can (constructively) prove that if ZFC proves some number-theoretical statement, then ZF proves it as well; and we can (constructively) prove that if PA proves a statement of the form $\forall\cdots\forall\exists\cdots\exists{:}\,\varphi$, where in $\varphi$ only bounded quantifiers ("$\forall n \leq \cdots$", "$\exists n \leq \cdots$") occur, then HA, the intuitionistic counterpart of HA, does so as well.
comment
Explaining the consistency of PRA and ZF from predicative foundations
Thank you for the insightful answer and the pointers to your papers, Nik. I wasn't aware of them. It seems then that the (apparent) consistency of impredicative systems is an unexplainable mystery from a predicative point of view. Upon further reflection I recognize that maybe this fact shouldn't be too unsettling: After all, formal systems have the tendency to not decide the consistency of formal systems, including that (of course) a system such as ZFC doesn't prove the consistency of ZFC.
comment
Explaining the consistency of PRA and ZF from predicative foundations
@Timothy: I thought so too, but hoped for an answer in the other direction demonstrating that my intuition is off. Maybe I should stress that my question only referred to consistency, not soundness. A priori, the position that PRA is in itself consistent while still proving lots of falsehoods might be a coherent position.
comment
Explaining the consistency of PRA and ZF from predicative foundations
@Not_Here: Ah, okay. I agree, and would appreciate any insight even if it only pertains to the consistency of PRA from the point of view of predicative arithmetic or to the consistency of (I)ZF from the point of view of predicative set theory.
comment
Explaining the consistency of PRA and ZF from predicative foundations
@Not_Here: I agree that the Feferman cogently explains why one could worry about impredicative set theory, in particular, why one might worry about the powerset axiom and why one hence might doubt the consistency of ZF, seeing that it includes a worrisome axiom. But I'm looking for predicative arguments which shed light on (which explain to some degree) the apparent consistency of ZF instead of giving reasons to doubt it.
comment
Explaining the consistency of PRA and ZF from predicative foundations
@David: (cont'd) (However, Gentzen's result doesn't seem to be directly relevant to my question. Predicative arithmetic doubts that primitive recursions terminate, hence doubts Gentzen's result, and predicative set theory has no problems verifying the consistency of PA, since in CZF and IZF we do have the completed set of naturals.) Regarding your second comment: Yes. The existence of such a simulation would satisfactorily explain the consistency of impredicative set theory from a predicative point of view. However, in the absence of such a simulation, there might still be other explanations.