Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration finite foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf sheaves simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorDavidRoberts
    • CommentTimeNov 20th 2012
    • (edited Nov 20th 2012)

    At fully formal ETCS there is the comment that the theory of a topos with NNO can be written as an essentially algebraic theory, and so there are models in any finitely complete category. I was thinking about this recently before I came across this comment, and I was thinking that we would need cartesian closedness as well, so this is a pleasant surprise. (Aside: I should write down the relevant sketch…)

    However, I was wondering if it was possible to consider the internal logic (or the stack semantics) of the canonical internal topos with nno in the finite limit theory of such and recover well-pointedness. This would be, for me at least, a remarkable result. Is this a reasonable thing to expect? Or am I trying to fly by picking myself up?

    • CommentRowNumber2.
    • CommentAuthorTodd_Trimble
    • CommentTimeNov 20th 2012

    Please don’t edit the ETCS article, because I am currently working on it! I plan to make good on that claim about essential algebraicity.

    • CommentRowNumber3.
    • CommentAuthorDavidRoberts
    • CommentTimeNov 20th 2012
    • (edited Nov 20th 2012)

    Don’t worry, I won’t edit it. I just had a look because I saw it was being updated :) Just a quick remark. Near the top you say that AC belongs to coherent logic, and near the bottom it says AC belongs to geometric logic. I guess the former is correct.

    • CommentRowNumber4.
    • CommentAuthorTodd_Trimble
    • CommentTimeNov 20th 2012

    Thanks, yes.

    Much of the rewriting is being done in remembrance of a fairly scathing assessment of the “fully formal” article by Emil Jerabek at MO, who correctly pointed out an omission and a mistake (both easily fixed), but there was a more general critique (that felt to me more like an attack) which definitely called for a response that was essentially impossible to flesh out in those damned comment boxes – too much stuff to explain, and I was too pissed off to even want to explain for his benefit. (I could look up the link, but I don’t much feel like doing so, even months after the fact.) The article at present is in a messy state because there have been a number of edits in the meantime none of which were carried to completion – I really need to go through the whole thing properly now.

    • CommentRowNumber5.
    • CommentAuthorUrs
    • CommentTimeNov 20th 2012

    I have added some more hyperlinks to the first two introductory paragraphs. For instance I hyperlinked the term first-order theory, etc. The entry first-order theory had been minimal. I have now expanded it ever so slightly. But it’s still minimal.

    • CommentRowNumber6.
    • CommentAuthorTobyBartels
    • CommentTimeNov 20th 2012

    Todd, I found that thread with Emil, and it seems to have come to life again earlier this month. I actually agree with Emil about nontriviality. I wrote a comment on MO that I copy here:

    I agree with Emil; nontriviality should be part of the definition of ETCS. It goes along with well-pointedness. It is true, of course, that “there is no rational square root of two” is true in the internal logic of the trivial topos, but if we were interested in founding mathematics on what can be proved in the internal logic of every suitable topos, then we wouldn’t have well-pointedness either. The point of being well-pointed is to make the internal logic line up with the external logic, and this requires nontriviality too.

    See also well-pointed topos.

    • CommentRowNumber7.
    • CommentAuthorTodd_Trimble
    • CommentTimeNov 20th 2012
    • (edited Nov 20th 2012)

    Interesting point, Toby! I wasn’t actually aware of the nondegeneracy requirement on 11 at well-pointed topos; is that standard? But anyway, your point makes sense.

    Edit: I looked in Mac Lane-Moerdijk, and in Lawvere’s article, but a quick glance tells me that neither source includes the nondegeneracy requirement. Is there a source besides the nLab that has this requirement?

    • CommentRowNumber8.
    • CommentAuthorTodd_Trimble
    • CommentTimeNov 20th 2012

    @Urs #5: okay, I was able to reproduce your edits in the editing window I had open, but I would like to ask everyone reading this please not to introduce more edits for at least today or so; it’s just going to screw things up for me. I’ll drop another note when I’m done for the time being.

    • CommentRowNumber9.
    • CommentAuthorUrs
    • CommentTimeNov 20th 2012

    Sorry, Todd, I didn’t understand that you wanted strictly no edits. I thoiught you just didn’t want substantial edits.

    So I guess you are editing the source separately, not in the nLab edit window. Okay, sorry.

    • CommentRowNumber10.
    • CommentAuthorTobyBartels
    • CommentTimeNov 20th 2012

    @Todd #7: I always thought that nontriviality was standard for well-pointedness, but it's the sort of thing that people can easily leave out when they really assume (or sometimes put in when they really don't need it). In Lawvere's article, it follows from Axiom 8. I'm pretty sure that 010 \ncong 1 is stated explicitly as an axiom in Lawvere & Rosebrugh (which is where I learnt ETCSETCS).

    • CommentRowNumber11.
    • CommentAuthorTodd_Trimble
    • CommentTimeNov 20th 2012

    Oh, there it is – thanks very much, Toby!

    • CommentRowNumber12.
    • CommentAuthorMike Shulman
    • CommentTimeNov 20th 2012

    My copy of Mac Lane and Moerdijk says on p275

    to exclude the trivial example for which \mathcal{E} is the category with only one object and one arrow, we will always assume that a well-pointed topos is also nondegenerate, i.e., 010\ncong 1.

    I think nondegeneracy as part of well-pointedness makes more sense when you think about the constructive version of well-pointedness, in which you have to also assume indecomposability and projectivity of 1 explicitly. It’s sort of an accident that those two properties follow in classical logic from 1 being a generator. Just as nondegeneracy is about falsehood, indecomposability is about disjunction and projectivity is about existential quantification.

    • CommentRowNumber13.
    • CommentAuthorMike Shulman
    • CommentTimeNov 20th 2012

    As for David’s original question in #1, I don’t understand what you are asking. Can you elaborate?

    • CommentRowNumber14.
    • CommentAuthorTobyBartels
    • CommentTimeNov 20th 2012

    Maybe to address #1, note that every category is internally well-pointed.

    • CommentRowNumber15.
    • CommentAuthorDavidRoberts
    • CommentTimeNov 20th 2012

    @Toby - that’s right. I was wondering if starting from a topos with nno, we can somehow bootstrap in well-pointedness, by considering the internal logic of the canonical internal topos one gets from the essentially algebraic theory.

    • CommentRowNumber16.
    • CommentAuthorMike Shulman
    • CommentTimeNov 20th 2012

    I’m afraid I still don’t understand. The essentially algebraic theory gives you the “free finitely-complete-category containing an internal well-pointed topos object”. What do you then want to do with that? Where does your starting topos with nno come into the picture?

    • CommentRowNumber17.
    • CommentAuthorDavidRoberts
    • CommentTimeNov 20th 2012

    Where does your starting topos with nno come into the picture?

    Whoops, that’s not what I meant. I meant starting from the topos in the free finitely-complete-category containing an internal well-pointed topos-with-nno object.

    And I was wondering (just now, not before) if this is something like the analogue of a countable model of ZFC, if we assume the existence of an ambient set theory. I mean this in only a very loose way.

    • CommentRowNumber18.
    • CommentAuthorMike Shulman
    • CommentTimeNov 21st 2012

    Okay, starting from there, now you want to do what?

    • CommentRowNumber19.
    • CommentAuthorDavidRoberts
    • CommentTimeNov 21st 2012
    • (edited Nov 21st 2012)

    Well, I’m not sure I really want to do anything in particular, I just find it amazing that one can write down a finite limit sketch, and then from this arises everything one can do in Choice-free, ordinary mathematics. You may wonder why this sort of amazement doesn’t arise when confronted with the finite axiomatisation of ETCS, or the fewer-symbols-but-not-actually-finite axiomatisation of ZF(C). Well, I suppose it’s that topos theory is so rich, and that finite limit sketches are so down-to-earth and concrete, but when written in the patois of traditional logicians, it all looks very much more complex, especially ZF(C) (or, to be fair BZ(C) as this is the directly comparable theory).

    Anyway, I probably shouldn’t have left out an opening disclaimer of ’This is just idle thoughts…’ in my original post. :-)

    • CommentRowNumber20.
    • CommentAuthorTobyBartels
    • CommentTimeNov 23rd 2012

    the finite axiomatisation of ETCS, or the fewer-symbols-but-not-actually-finite axiomatisation of ZF(C)

    Since the axiomatisation of the latter is recursively enumerable, it has a conservative extension whose axiomatisation is finite; the usual example is BNG.

    • CommentRowNumber21.
    • CommentAuthorTom Leinster
    • CommentTimeDec 3rd 2012

    @Todd #7: Definition 9.34 of Johnstone’s Topos Theory includes nondegeneracy in the definition of well-pointedness. It defines a topos to be well-pointed if 1 is a generator and 010 \to 1 is not iso.

    • CommentRowNumber22.
    • CommentAuthorTodd_Trimble
    • CommentTimeDec 4th 2012

    Tom: I accept that this is the standard definition. Thanks.

    • CommentRowNumber23.
    • CommentAuthorTom Leinster
    • CommentTimeDec 4th 2012
    • (edited Dec 4th 2012)

    You’re welcome. I just happened to be reading that page of Topos Theory, remembered this thread, and thought I might as well add it as a data point, in case anyone was keeping track.