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 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 nforum 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).

nLab > Latest Changes: Stack semantics

Bottom of Page

1 to 21 of 21

  1.  
    • CommentRowNumber1.
    • CommentAuthorTobyBartels
    • CommentTimeAug 25th 2011

    There is now an extremely stubby stub at stack semantics.

    • CommentRowNumber2.
    • CommentAuthorMike Shulman
    • CommentTimeAug 27th 2011

    Thanks! When I get around to revising that paper this fall, I’ll try to write some about it on the nLab too.

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeAug 27th 2011
    • (edited Aug 27th 2011)

    Don’t forget to explain in the entry why its called stack semantics.

    • CommentRowNumber4.
    • CommentAuthorUrs
    • CommentTimeMay 17th 2012
    • (edited May 17th 2012)

    I am wondering if we cannot give a better Idea-section in the entry stack semantics. The current idea section sounds very complicated and mysterious to the uninitiated, and it emphasizes the problem to be solved over the nature of the actual solution that is the page’s actual topic. If you see what I mean. (?)

    Let me know if I am wrong about the following: my impression is that the simple conceptual idea behind “stack semantics” is clearest if we think not about toposes but about ∞\infty-toposes: then that simple idea is

    Use the object-classifier groupoid object and in fact refine it to the object classifier category object.

    Right?

    For completeness and in case it is not clear what I mean:

    the (κ\kappa-small) object classifier Type κType_\kappa is the thing that classifies the core of the self-indexing/codomain fibration

    H(X,Type κ)≃Core((H /X) κ). \mathbf{H}(X, Type_\kappa) \simeq Core((\mathbf{H}_{/X})_\kappa) \,.

    The starting point of the “stack semantics” thing is – unless I am missing something – essentially the idea that we pass to something that classifies in fact all of (H /X) κ(\mathbf{H}_{/X})_\kappa.

    That thing should be a category object in the ∞\infty-topos H\mathbf{H}.

    And that should — shouldn’t it? – start out looking like this:

    first, the object classifier Type κType_\kappa we may suggestively write as a “complete Segal groupoid object” as

    ⋮ ↓↓↓ [A,B:Type κ⊢(A=B)] ↓↓ Type κ, \array{ \vdots \\ \downarrow \downarrow \downarrow \\ [A,B : Type_\kappa \vdash (A = B)] \\ \downarrow \downarrow \\ Type_\kappa } \,,

    which by univalence I can write more suggestively as

    ⋮ ↓↓↓ [A,B:Type κ⊢(A→≃B)] ↓↓ Type κ, \array{ \vdots \\ \downarrow \downarrow \downarrow \\ [A,B : Type_\kappa \vdash (A \stackrel{\simeq}{\to} B)] \\ \downarrow \downarrow \\ Type_\kappa } \,,

    and looking at this makes us want to (doesn’t it?) say that the “stack semantics classifier” or whatever we call it, is a complete Segal category object that starts out looking as

    ⋮ ↓↓↓ [A,B:Type κ⊢(A→B)] ↓↓ Type κ \array{ \vdots \\ \downarrow \downarrow \downarrow \\ [A,B : Type_\kappa \vdash (A \to B)] \\ \downarrow \downarrow \\ Type_\kappa }

    where the object of morphisms is the function type regarded as a Type×TypeType \times Type-dependent type.

    Ahm, not sure, would be just grateful about some chat about this.

    • CommentRowNumber5.
    • CommentAuthorMike Shulman
    • CommentTimeMay 18th 2012

    Thanks for bringing this up. I’ll try to write something coherent about how I think about stack semantics now (which isn’t exactly how I thought about it at first), either here or at the entry.

    • CommentRowNumber6.
    • CommentAuthorUrs
    • CommentTimeMay 18th 2012
    • (edited May 18th 2012)

    Just an idle thought, only partly related:

    if we define a simplicial object in low degree type theoretically by proceeding as

    ⊢X 0:Type (x,y):X 0×X 0 ⊢X 1(x,y):Type (f,g,h):∑ (x,y,z):X 0×X 0×X 0X 1(x,y)×X 1(y,z)×X 1(x,z) ⊢X 2(f,g,h):Type etc \begin{aligned} & \vdash X_0 : Type \\ (x,y) : X_0 \times X_0 & \vdash X_1(x,y) : Type \\ (f,g,h) : \sum_{(x,y,z) : X_0 \times X_0 \times X_0} X_1(x,y) \times X_1(y,z) \times X_1(x,z) &\vdash\; X_2(f,g,h) : Type \\ & etc \end{aligned}

    then when interpreted in a type-theoretic model category this comes out as a Reedy fibrant+cofibrant (truncated) simplicial diagram: the fibrancy condition on the matching morphisms is the very interpretation of the above dependent types.

    Of course this is still not a full simplicial diagram, because it stops when I stop typing the above lines. But at least the coherence is taken care of to the given degree. For instance the correct maps between two such objects will have the evident naive formulation.

    Just a thought.

    • CommentRowNumber7.
    • CommentAuthorMike Shulman
    • CommentTimeMay 18th 2012

    this comes out as a Reedy fibrant+cofibrant (truncated) simplicial diagram

    Yes, that’s the basic idea of my paper on univalence for inverse diagrams. But you can only get semi-simplicial objects this way, as far as I can tell; the degeneracies are a problem.

    • CommentRowNumber8.
    • CommentAuthorUrs
    • CommentTimeMay 18th 2012

    I see. So now it’s out that I hadn’t read your article carefully. :-/ Actually I did, but got distrated somewhere in the middle.

    But I see it now.

    • CommentRowNumber9.
    • CommentAuthorUrs
    • CommentTimeMay 18th 2012
    • (edited May 18th 2012)

    Hi Mike,

    another idle thought:

    in lowest degree choosing the degeneracy map means equipping X 1→X 0×X 0X_1 \to X_0 \times X_0 with the structure of an algebra over the endofunctor whose initial algebra is the identity type X 0 IX_0^I.

    This sounds vaguely suggestive of something. But I am not sure of what ;-) Maybe somehow the addition of degenracies to a semisimplicial Reedy fibrant diagram can usefully be related to higher inductive types of sorts?

    • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeMay 18th 2012
    • (edited May 18th 2012)

    Here is one more thought (all of this just elementary toying around, I am well aware, but I feel like chatting about it anyway):

    The recursion principle for identity types is closely related to the complete-Segal condition.

    Sorry for the boldface, but when this occured to me I found it charming.

    This will be trivially evident for you, but let me just spell it out anyway, also in case some bystander is listening and wondering about it:

    So the recursion principle for identity types says that if the category-object-to be

    X 1 ↓ X 0×X 0 \array{ X_1 \\ \downarrow \\ X_0 \times X_0 }

    has an identity-assigning map X 0→X 1X_0 \to X_1, then this factors through the path object of X 0X_0 by a compatible morphism

    X 0 I→X 1. X_0^I \to X_1 \,.

    But this is precisely the morphism that the complete-Segal condition will be a condition on: namely it will say that this morphism exhibits the homotopy-full inclusion of elements in X 1X_1 that are equivalences.

    Yeah, hm, this is just a variant of the univalence story. Hm…

    • CommentRowNumber11.
    • CommentAuthorUrs
    • CommentTimeMay 18th 2012
    • (edited May 18th 2012)

    Hm, right. Isn’t that true:

    univalence is equivalently the first degree component in the complete-Segal condition on “the homotopy stack semantics” (the classifier of the codomain fibration). ?!

    • CommentRowNumber12.
    • CommentAuthorMike Shulman
    • CommentTimeMay 18th 2012

    Yes, I think that’s right; univalence means that when you build the internal full subcategory corresponding to the universal dependent type Type˜→Type\widetilde{Type}\to Type, its nerve is a complete Segal object.

    That is nice. I don’t think I’ve seen it stated in that way before…

    • CommentRowNumber13.
    • CommentAuthorMike Shulman
    • CommentTimeMay 18th 2012

    Okay, I completely replaced the stub at stack semantics with a different idea section and a long description of how I see stack-semantics relating to object classifier and universes. What do you think?

    • CommentRowNumber14.
    • CommentAuthorUrs
    • CommentTimeMay 18th 2012

    Thanks, yes, I like that.

    Just to be sure: when you say “stack semantics” you are primarily referring to universe enlargement, and only secondarily to the issue of having a groupoidal or a categorical universe. Is that right?

    Might it make sense to say this right in the first sentence? Something like “Stack semantics is an extension of the internal logic […] essentially corresponding to a universe enlargement.” ?

    • CommentRowNumber15.
    • CommentAuthorMike Shulman
    • CommentTimeMay 19th 2012

    No, I use “stack semantics” to refer to both at once.

    • CommentRowNumber16.
    • CommentAuthorUrs
    • CommentTimeMay 19th 2012
    • (edited May 19th 2012)

    Okay, I see. This could maybe be clearer in the entry. Because where it currently says

    […] should be regarded as a category, or at worst as a groupoid […]

    I got away with thinking that the difference is just meant to be a matter of taste.

    How about if we put that right into the very first sentence and expand what is currently there to something like this:

    The stack semantics is an extension of the internal logic a category (or higher category) C by extending an internal universe to an external universe category object, which allows us to talk about, and quantify over, objects of C. (Such quantification is sometimes called “unbounded” quantification.)

    ?

    By the way, what motivated my questions here is that I wanted to understand what terminology you would prefer for the internal but categorical case, that where we refine the internal universe “Segal-complete groupoid object” (hence equivalently just an object) to an internal category object.

    • CommentRowNumber17.
    • CommentAuthorMike Shulman
    • CommentTimeMay 20th 2012

    Wait, I think I misunderstood your “or”. When you said

    the issue of having a groupoidal or a categorical universe

    I thought you meant the issue of having (1) a groupoidal or categorical universe versus the alternative option (2) of having a set-like universe. I meant that stack semantics means that the universe is groupoidal or categorical, i.e. not set-like.

    But I guess you were asking whether stack semantics means that the universe is groupoidal, or whether it means that it is categorical? It doesn’t really matter; I tried to explain that in the entry. Because the non-invertible morphisms are modeled in the internal language using exponential objects, it doesn’t matter whether the “universe” is a groupoid or a category. You get exactly the same Kripke-Joyal style semantics, which is the original meaning of “stack semantics”.

    • CommentRowNumber18.
    • CommentAuthorUrs
    • CommentTimeMay 20th 2012

    But I guess you were asking whether stack semantics means that the universe is groupoidal, or whether it means that it is categorical?

    Yes! Mainly I am trying to figure out if when I want to express “consider the internal category object corresponding to the small self-indexing” it would be consistent with your use of terminology to say “consider the stack semantics”.

    But I gather the answer to that is “No”, since, as you say, the choice of either universe groupoid or universe category does not affect the logic / semantics.

    Okay, good. If you still have a second: can we find a proposal for a good technical term for the internal category object that should start out as

    (A,B):Type×Type ⊢A→B:Type (f,g,h):∑ (A,B,C):Type×Type×Type(A→B)×(B→C)×(A→C) ⊢(g∘f=h):Type ⋮ ⋮ \begin{aligned} (A, B) : Type \times Type & \;\; \vdash A \to B : Type \\ (f,g,h) : \sum_{(A,B,C) : Type \times Type \times Type} (A \to B) \times (B \to C) \times (A \to C) & \;\;\; \vdash (g \circ f = h): Type \\ \vdots & \vdots \end{aligned}

    ?

    How about “the canonical internal base topos”? Or just “the internal base topos”?

    • CommentRowNumber19.
    • CommentAuthorMike Shulman
    • CommentTimeMay 21st 2012

    Correct, that is not how I would use “stack semantics”.

    I guess “the internal full subcategory on the object classifier” is too long? I’m not immediately enamored of “base topos” because we’re only talking inside of a single topos here, there is no base vs. other.

    • CommentRowNumber20.
    • CommentAuthorMike Shulman
    • CommentTimeMay 21st 2012

    How about the “internal self-indexing”?

    • CommentRowNumber21.
    • CommentAuthorDavidRoberts
    • CommentTimeNov 8th 2019

    Fix broken link. Some programmatic change had turned what may have been an en-dash in the link to Mitchell-Bénabou language to a question mark.

    diff, v8, current

1 to 21 of 21

  1.