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 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 internal-categories k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure 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 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).

nLab > Latest Changes: internal set

Bottom of Page

1 to 30 of 30

  1.  
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeSep 12th 2012

    I see we have internal set, while I was just about to make that term redirect to Bishop set.

    That would have read more systematically in the list at internal infinity-categories contents .

    • CommentRowNumber2.
    • CommentAuthorTobyBartels
    • CommentTimeSep 13th 2012

    The usual term used in place of ‘internal set’ is ‘object’ (in a 11-category).

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeSep 13th 2012
    • (edited Sep 13th 2012)

    The usual term used in place of ‘internal set’ is ‘object’ (in a 1-category).

    In fact, no. That’s the whole point: an object in 1 -category is just an internal preset or h-set. To have an internal set one really has to add more information.

    It’s useful to think about this in analogy with ∞\infty-groupoids, where the phenomenon is less degenerate (less truncated) and hence maybe better visible:

    an object XX in an ∞\infty-topos is not actually an internal ∞-groupod. It becomes an internal ∞\infty-gropoid only after being equipped with a notion of elements X 0X_0 and an ∞\infty-equivalence relation X 1→X 0×X 0X_1 \to X_0 \times X_0.

    From this data XX can be recovered. But XX is less than X •X_\bullet. XX may be called an internal “pre ∞\infty-groupoid” whereas X •X_\bullet is the actual internal ∞\infty-groupoid.

    This is how I got into this discussion: in another thread with Karol we were talking about how having a foundation of ∞\infty-category theory in homotopy type theory is analogous to having a foundation of set theory in type theory: in both cases the types are the internal pre-things that we are concerned with, and the actual internal things that we are concerned with are the those pre-things equipped with an equivalence relation.

    • CommentRowNumber4.
    • CommentAuthorUrs
    • CommentTimeSep 13th 2012

    I have added a comment to h-set on this issue, but let’s discuss this in its thread.

    • CommentRowNumber5.
    • CommentAuthorTodd_Trimble
    • CommentTimeSep 13th 2012
    • (edited Sep 13th 2012)

    The usual term is object. Not “internal set” or “internal preset”. I’ve never heard anyone say, “ℤ\mathbb{Z}, considered as an internal preset of AbAb”.

    • CommentRowNumber6.
    • CommentAuthorUrs
    • CommentTimeSep 13th 2012
    • (edited Sep 13th 2012)

    I am not sure if we are all discussing the same thing.

    So in constructive foundations in type theory a type is called a preset, a type with an equivalence relation on it is a set. People say this, you can see it in the references at Bishop set.

    So this is what I am talking about. Now Toby passed to the categorical semantics and claimed that set goes to object. But what goes to objects is the types, hence the presets.

    And as I tried to point out in that remark now at h-set, in fact only the latter terminology is consistent with the more general terminology of internal higher groupoids.

    • CommentRowNumber7.
    • CommentAuthorTodd_Trimble
    • CommentTimeSep 13th 2012

    I see. Sorry, then.

    • CommentRowNumber8.
    • CommentAuthorTobyBartels
    • CommentTimeSep 13th 2012

    The usual term used in place of ‘internal set’ is ‘object’ (in a 1-category).

    In fact, no. That’s the whole point: an object in 1 -category is just an internal preset or h-set.

    That’s a good point.

    Actually, what I said is true: the usual concept of internal set in a 11-category is simply an object. (Compare other internal notions, such as internal monoid.) But there is a better general concept of internal set (particularly in a category viewed as a universe), which can more unambiguously be called ‘internal setoid’.

    And this is what you wanted in your list, so (despite writing a true sentence) I was wrong.

    So in constructive foundations in type theory a type is called a preset, a type with an equivalence relation on it is a set.

    Be careful; sometimes this terminology is used, but other times the words ‘set’ and ‘setoid’ are used in place of ‘preset’ and ‘set’. (There are other combinations, such as ‘type’ and ‘setoid’.) For example, in Coq, Set is really a type of presets.

    • CommentRowNumber9.
    • CommentAuthorTobyBartels
    • CommentTimeSep 13th 2012

    The problem here is that the language of the word ‘internal’ has always been geared towards the category of sets (where sets are, of course, objects) when presets are the more basic concept. So any treatment of categories and higher categories that wants to get at such basic concepts will run into trouble with that language.

    • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeSep 13th 2012
    • (edited Sep 13th 2012)

    Hi Toby,

    yes, thanks. I understand where you both were coming from, I am aware of the different traditions. It was just that I came from all this discussion of Bishop sets, the predicative topos that they form, the tight relation to the question of ∞\infty-category theory internal to homotopy type theory, etc; maybe about half a dozen related threads here. So I thought it was clear which context I am speaking in. But I understand that I should have made it clearer. I should have base changed you to the context in which I was making judgements, first. ;-)

    So this preset/set things is a subtle issue. I find it striking how close it in nature to the subtleties that we were discussing a few months back in the thread on internal ∞\infty-categories. There, too, one runs into these subtle shades of notions, where one needs to distinguish “internal pre-∞\infty-categories” from the “complete” ones, etc.

    I think it’s closely related, that’s why I made that remark in h-set, please check if you haven’t yet, to see if we can agree on this.

    I think this may be relevant: in Benno’s article somewhere he mentions that Bas once asked whether h-sets in HoTT also form a predicative topos. I am not sure about that question, but I think it points to the following important point:

    we know now that the types in HoTT form an ∞\infty-topos (at least a locally cartesian closed category with universe and as many inductive objects as to care to add). But the next central question will be: what do the internal ∞\infty-categories form? I guess they will form a predicative ∞\infty-topos.

    • CommentRowNumber11.
    • CommentAuthorTobyBartels
    • CommentTimeSep 13th 2012

    Yes, I agree with the remark at h-set.

    BTW, I threw in a link to completely presented set (which however currently just redirects to preset) at types and logic - table where it seemed to be needed.

    • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeSep 13th 2012

    at types and logic - table where it seemed to be needed.

    Ah, thanks. I was wondering what to put there. I decided that maybe in the left column the distinction hadn’t been made.

    So how do you decide where to put this? Is the table right that “completely presented set” is a notion in “logic” while “preset” is one in type theory? Maybe we should move “preset” also to the “logic”-column?

    It’s more a question about history than about facts. There were a few other entries in the table where I was hesitating about whether they sit in the right column. (On the other hand that’s of course part of the point of this table, to show that the distinction between the columns is artificial.)

    • CommentRowNumber13.
    • CommentAuthorTobyBartels
    • CommentTimeSep 13th 2012

    Yes, in these rows, it’s often unclear what should be in which column. I just figured that completely presented set was better than set, and you had set in the same column on the next row, while you had preset in a different column in the same row. Since ‘completely presented set’ isn’t simply a synonym for ‘preset’ (although they do correspond in a way), it’s good to have them listed separately (but in the same row); however, which column holds which words is not really clear that far down in the table!

    • CommentRowNumber14.
    • CommentAuthorMike Shulman
    • CommentTimeSep 13th 2012

    But there is a better general concept of internal set (particularly in a category viewed as a universe), which can more unambiguously be called ‘internal setoid’.

    I’m not sure I entirely understand what’s being said here, but I strongly disagree with the idea that an object equipped with an internal equivalence relation is a better notion of “set” internal to a category. It all depends on how you intend to regard the objects of that category. If your category is a 1-topos, for instance, then usually you want to regard its objects as sets in which case they are the good notion of internal set. But if the objects of your category are, say, assemblies, or types in a type theory that lacks quotient types, then you may want to regard its objects instead as presets.

    The same thing is at play in higher dimensions. I would argue that when working internally to an (∞,1)(\infty,1)-topos we usually want to regard its objects as ∞\infty-groupoids internal to its world.

    I agree that the fact that we currently say “internal ∞\infty-groupoid in an (∞,1)(\infty,1)-category” to mean something other than simply “object” would suggest, if we were inventing mathematics out of whole cloth, that “internal set” ought to mean an object equipped with an equivalence relation. However, I think that actually using terminology in that latter way would be extremely confusing, and I would prefer to change it in the other way: say something like “(∞,1)(\infty,1)-congruence” rather than “internal ∞\infty-groupoid”.

    • CommentRowNumber15.
    • CommentAuthorUrs
    • CommentTimeSep 13th 2012

    The thing was that there is no such ambiguity in “internal ∞\infty-category” – and when that is restricted to the invertible case one gets conguences/internal groupoids and not just objects.

    • CommentRowNumber16.
    • CommentAuthorMike Shulman
    • CommentTimeSep 13th 2012
    • (edited Sep 13th 2012)

    (cancel)

    • CommentRowNumber17.
    • CommentAuthorUrs
    • CommentTimeSep 13th 2012

    There are more reasons to stick to the convention that a groupoid in an ∞\infty-topos is not just an object XX, but an object XX with an effective epimorporphism U→XU \to X (an atlas):

    several standard notions in structured groupoid theory, such as etale groupoid mandatorily assume that the atlas U→XU \to X is part of the data. Etaleness is with respect to that atlas, otherwise there is no such notion.

    Similarly, in an cohesive ∞\infty-topos with infinitesimal cohesion we can say what it means for a morphism to be a formally etale morphism. It turns out (Stephan Spahn will have something out on this soon) that in the smooth context an etale ∞\infty-groupoid is an effective epi U→XU \to X such that this morphism is formally etale.

    • CommentRowNumber18.
    • CommentAuthorUrs
    • CommentTimeSep 13th 2012
    • (edited Sep 13th 2012)

    Also the right notion of internal Lie algebroid of an internal groupoid requires the atlas. The “Lie-Rinehart pair”-description of Lie algebroids makes that manifest: we have a base space and a Lie algebra paraeterized over it. This is the differential version of having an atlas U→XU \to X and the group Equiv(U) XEquiv(U)_X.

    • CommentRowNumber19.
    • CommentAuthorMike Shulman
    • CommentTimeSep 13th 2012

    I would argue that in an (∞,2)(\infty,2)-topos, the right notion of “internal (∞,1)(\infty,1)-category” would be just “object”. It’s only when our ambient category is insufficiently endowed with higher morphisms that we have to recourse to building things more explicitly.

    Let me try to be more precise about what I think is going on. I would argue that in an (n+1)(n+1)-exact (n+1)(n+1)-category, the right notion of “internal nn-category” is “object”. (Here nn could be 11, 22, (∞,1)(\infty,1), (∞,2)(\infty,2), etc.) But if you happen to not be in an (n+1)(n+1)-exact (n+1)(n+1)-category, then this doesn’t make sense. So what people often do is pass to the free (n+1)(n+1)-exact (n+1)(n+1)-category generated by whatever category you started with (a.k.a. its (n+1)(n+1)-exact completion), and call the objects of that “internal nn-categories” in the category you started from.

    In particular, the objects of the free 1-exact 1-category generated by a regular 1-category are precisely the internal equivalence relations, and the objects of the free 1-exact 1-category generated by a 1-category with finite limits are the ’pseudo-equivalence relations’ (equivalence ’relations’ that might not be monic). The latter, by the way, are I believe what people working in MLTT usually call ’setoids’, not the former. This is logical because in the absence of bracket types, the category of contexts in type theory is not regular.

    Unfortunately, the formal theory of nn-exact completion for n>1n\gt 1 doesn’t exist yet. But I am pretty confident that, for instance, the objects of the free 2-exact 2-category generated by a 1-exact category will be the internal categories therein, in the classical sense. (Its morphisms will be anafunctors.)

    Of course there is a problem that if you start with an (n+1)(n+1)-exact (n+1)(n+1)-category, then you get two different notions of “internal nn-category” according to whether you remember that it was (n+1)(n+1)-exact, or whether you forget that and take its free (n+1)(n+1)-exact completion. But fortunately, there should also be a more general framework which keeps track of this sort of thing. The right context in which to talk about an “internal nn-category” is a unary (n+1)(n+1)-site, and in that case the meaning of “internal nn-category” is “object of the (n+1)(n+1)-exact completion”. An (n+1)(n+1)-exact (n+1)(n+1)-category should be its own exact completion regarded as a unary (n+1)(n+1)-site with its (n+1)(n+1)-exact topology, while the free (n+1)(n+1)-exact completion of any category corresponds to starting with a trivial topology.

    • CommentRowNumber20.
    • CommentAuthorMike Shulman
    • CommentTimeSep 13th 2012

    Re: #17, I have no problem with the idea that being “etale” is a structure rather than a property.

    • CommentRowNumber21.
    • CommentAuthorUrs
    • CommentTimeSep 13th 2012
    • (edited Sep 13th 2012)

    I have no problem with the idea that being “etale” is a structure rather than a property.

    Not sure what to make of that. Need to think about whether I would agree with this.

    But let’s look at Lie differentiation, where the case is more clear-cut: what is called a “bisection” of a Lie gorupoid is – the atlas U→XU \to X understood – an equivalence

    U →≃ U ↘ ⇙ ↙ X \array{ U &&\stackrel{\simeq}{\to}&& U \\ & \searrow &\swArrow& \swarrow \\ && X }

    The “Lie-Rinehart”-presentation of the Lie algebroid of XX (hence really of U→XU \to X) is the pair (U,Aut(U) X)(U, Aut(U)_X).

    (Also in the more popular description of Lie algebroids via vector bundles over UU, this UU is fixed).

    So Lie differntiation of a Lie groupid means and always meant (though people don’t say this): of a Lie groupoid with atlas.

    With your proposal, there would be no way to say “To a smooth groupoid we can associate its Lie algebroid.” Instead we would have to say “To each way of equipping a smooth groupoid with xyz-structure we can assign a Lie algebroid.”

    (Having said all this: of course I myself kept and keep saying “smooth ∞\infty-groupoid” for an object of Sh ∞(SmthMfd)Sh_\infty(SmthMfd). But I feel something needs to be done about the terminology. Smooth homotopy type is probably better.)

    • CommentRowNumber22.
    • CommentAuthorUrs
    • CommentTimeSep 13th 2012

    re #19: thanks for taking the time to share this. I sure appreciate the reasoning there. What I am not sure yet is to which extent this answers the question of what an internal anything is in homotopy type theory or just reformulates that in different terms.

    I’ll like to continue discussing this. It’s clearly of profound importance. But for tonight I should stop. I badly need to look into something else right now.

    • CommentRowNumber23.
    • CommentAuthorUrs
    • CommentTimeSep 13th 2012

    One more comment, after all (I never listen to myself, it seems ;-)

    Whatever the answer is in these matters here, it’s probably good to keep in mind the case for groups. The fact that Grp(H)Grp(\mathbf{H}) is the collection of pointed connected objects is of course related to those atlases: that point is the “minimal” atlas of a connected object.

    So if we say “internal groupoid” means “type with atlas/type with type of objects”, then it becomes true again that “groups are equivalent to the one-objects internal groupoids” .

    Not sure what this implies. Last thought for tonight on this.

    • CommentRowNumber24.
    • CommentAuthorMike Shulman
    • CommentTimeSep 13th 2012

    The discussion here suggests that the term for “smooth groupoid with xyz-structure” should be something like “0-strict smooth groupoid”.

    • CommentRowNumber25.
    • CommentAuthorMike Shulman
    • CommentTimeSep 14th 2012

    So if we say “internal groupoid” means “type with atlas/type with type of objects”, then it becomes true again that “groups are equivalent to the one-objects internal groupoids” .

    I’m not so sure about that. Even when we define “internal groupoids” in a 1-topos in the most classical way — which are then equivalent to 1-truncated objects of the corresponding (∞,1)(\infty,1)-topos equipped with a 0-truncated cover — and take the morphisms between them to be those that preserve the specified covers (hence internal functors in the classical sense, rather than anafunctors), no one ever requires the natural transformations between them to also preserve the covers (which would reduce them all to triviality).

    • CommentRowNumber26.
    • CommentAuthorMike Shulman
    • CommentTimeSep 14th 2012

    Cf. the definition of natural transformation between strict categories.

    • CommentRowNumber27.
    • CommentAuthorTobyBartels
    • CommentTimeSep 14th 2012

    The right context in which to talk about an “internal nn-category” is a unary (n+1)(n+1)-site, and in that case the meaning of “internal nn-category” is “object of the (n+1)(n+1)-exact completion”.

    Yes, this is true; it’s in my PhD thesis. They’ll take my degree away if I stop believing this.

    An (n+1)(n+1)-exact (n+1)(n+1)-category should be its own exact completion regarded as a unary (n+1)(n+1)-site with its (n+1)(n+1)-exact topology, while the free (n+1)(n+1)-exact completion of any category corresponds to starting with a trivial topology.

    This should settle all discrepancies; it’s just a question of which topology we’re using.

    But it does make things more complicated.

    • CommentRowNumber28.
    • CommentAuthorMike Shulman
    • CommentTimeSep 14th 2012

    @Toby: I’m glad you agree!

    • CommentRowNumber29.
    • CommentAuthorTobyBartels
    • CommentTimeSep 17th 2012
    • (edited Sep 17th 2012)

    it's in my PhD thesis

    (This is exaggerated: only a small part of that in my thesis. But the part where the topology matters is.)

  30. Since then has unalived.

    The passage of time

    diff, v7, current

1 to 30 of 30

  1.