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

Discussion Tag Cloud

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: terminology for modal types etc.

Bottom of Page

1 to 17 of 17

  1.  
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeMar 18th 2015

    I am still after getting a more fine-grained idea of how to best and systematically attach words (notions) to the pluratily of structures encoded by adjoint pairs of modal operators.

    Over in the GoogleGroup “nLab talk” Mike and I were discussing this in the thread called “modal and co-modal”, I am now moving this to here.

    This issue is to a large extent just a linguistic one, and so should maybe better be ignored by readers with no tolerance for that.

    Myself, I may be very slow in discussing this, as I come back to the question every now and then when something strikes me. For the moment I am just looking more closely at our examples to explore further what in their known situation is natural terminology.

    Here is one random thought:

    given a sharp modality, then we look for the “concrete” objects XX for which the unit X↪♯XX \hookrightarrow \sharp X is a monomorphism. In a sense the anti-modal objects for which ♯X≃*\sharp X\simeq \ast are at the “opposite extreme” of these where a concrete object is all “supported on points”, a sharp-anti-modal object is maximally not supported on points.

    By the way, regarding just the terminology for this special case: I have come to think that this is what should be referred to by “intensive quantity” and “extensive quantity”. In modern language an extensive quantity in thermodynamics is a differential form in positive degree (e.g. the mass density 3-form on Euclidean 3-space) while an intensive quantity is a 0-form, hence a function (for instance a temperature function on Euclidean 3-space).

    Now the sheaf of functions ℝ\mathbb{R} is indeed such that ℝ↪♯ℝ\mathbb{R}\hookrightarrow \sharp \mathbb{R}, while the sheaves Ω p\mathbf{\Omega}^p of differential forms in positive degree are indeed such that ♯Ω p≃*\sharp \mathbf{\Omega}^p \simeq \ast. The objects XX with ♯X≃*\sharp X\simeq \ast are “extensive” in the literal sense that they “extend further than a single point”. This is much the “extension” by which also Grassmann’s Ausdehnungslehre refers to his forms.

    A related random thought: so given any modal operator ◯\bigcirc we should probably be looking at objects XX such that X→◯XX \to \bigcirc X is a mono, or is nn-truncated for general nn.

    For instance the “separated objects” for the constant *\ast-modality are the mere propositions. Generally, the nn-truncated objects are maybe more naturally thought of as being part of what the *\ast-modality encodes. From this perspective the nn-truncation monads on the one hand and the monads appearing in cohesion on the other play somewhat different roles in the whole system, which maybe explains some of the terminological mismatch (if that’s what it was) that Mike and I were struggling with in the earlier thread.

    • CommentRowNumber2.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 18th 2015

    Had you settled there about whether to use comodal/modal for idempotent comonad/monad?

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeMar 18th 2015
    • (edited Mar 18th 2015)

    While I am still undecided of what the best terminology really is on absolute grounds, I don’t want to be trouble, understanding that Mike has been and is probably currently writing about this. I am fine with all his suggestions.

    What I am after here is maybe something a bit outside of mathematics, maybe some connection to linguistics, some “Arbeit am Begriff”, which probably most readers here, maybe including Mike, would rather not like to be bothered with.

    What troubles me is that in the examples of the adjoint modalities appearing in graded differential cohesion, I know how to attach lots of well-fitting notions to the various structures they encode, but I am unsure as to what a systematic rule for doing that would be.

    For instance when you know what the ♭⊣♯\flat \dashv \sharp adjunction does in practice, then it seems exceedingly clear that, yes, this expresses an opposition between completely discrete and completely continuous, and yes, jointly this encodes key aspects of quantity (notably discrete quantity such as cardinality on the left and continuous quantity on the right), and yes, moreover (as in #1) it neatly distinguishes between extensive and intensive quantity. Moreover, I think with what Mike said about “real cohesion” induced by Dedekind reals, this even captures well the concept of number as something appearing in the force field between these two opposites.

    This is most enjoyable, in its way. But I want to understand more systematically what it is that makes this terminology fit, such that I may then carry this rule to the other 5+2 adjoint modalities in graded differential cohesion.

    • CommentRowNumber4.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 19th 2015

    Looking back at the Google Group discussion, I think I’m confused about what you’re after. Evidently it’s systematicity in naming. But is it to be of the form, irrespective of which is left-right adjoint, that for any adjoint modality, it essentially expresses the relation between the modal types of one and the anti-modal types of the other?

    • CommentRowNumber5.
    • CommentAuthorUrs
    • CommentTimeMar 19th 2015

    Thanks, so I am already stuck with systematically assigning terminology to the various qualities expressed by

    1. ♭⊣♯\flat \dashv \sharp

    2. ∅⊣*\emptyset \dashv \ast.

    If we could figure out just that, this would be a step in the right direction.

    So recall that in the first case we have

    • the objects sent by the operators to themselves, these are the discrete and the absolutely continuous or codiscrete ones.

    • the objects whose ♯\sharp-unit is a mono. These are the concrete objects or “intensive quantities”. Conceptually opposed to them are the objects which are sent to the terminal object by either of ♭\flat or ♯\sharp, the “extensive quantities”.

    The first item is clear, the second requires work, as far as I am concerned.

    Let’s match this to ∅⊣*\emptyset \dashv \ast. Here:

    • the objects sent by the operators to themselves are the empty object and the uniquely inhabited object.

    • the objects whose *\ast-unit is a mono are the mere propositions, the objects sent by ∅\emptyset to the point are non-existent, while the objects sent by *\ast to the point are all objects.

    Again, the first item is clear, the second seems to require more thinking. Here it is the anti-modal types of the two operators which seem to be in natural opposition (“none” versus “all”), while it is unclear to me how the mere propositons are “in opposition” to anything here.

    What’s a nice systematic way to look at this such that both these cases work analogously, as far as the terminology is concerned?

    • CommentRowNumber6.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 19th 2015

    Do you not buy into Mike’s suggestion that it should be

    the objects which HAVE THE SAME IMAGE AS the terminal object by either of ♭\flat or ♯\sharp, the “extensive quantities”.

    So then

    the objects which HAVE THE SAME IMAGE AS the terminal object by either of ∅\empty or *\ast, everything.

    At least that makes the latter coincide.

    As for the other point, why is the unit privileged? What does the adjunction [X,*]≃[∅,X][X, \ast] \simeq [\empty, X] do to the monos on the left side?

    Should we expect some asymmetry?

    • CommentRowNumber7.
    • CommentAuthorUrs
    • CommentTimeMar 19th 2015

    Which suggestion by Mike is this referring to? I seem to have missed this. I just checked my email, but maybe I am not looking for the right thing now. Could you give the link or the full quotation? Sorry if I am being stupid here, maybe I am too distracted by other things.

    • CommentRowNumber8.
    • CommentAuthorUrs
    • CommentTimeMar 19th 2015

    Oh, you mean the last message here?

    • CommentRowNumber9.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 19th 2015

    Yes, that’s it.

    • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeMar 19th 2015
    • (edited Mar 19th 2015)

    Hm, maybe, but why?

    Here is a thought: that condition with the monos must be related to the “pieces-have-points axioms” (the Nullstellensatz) which in its dual incarnation says that all discrete objects are concrete, hence that the composite

    ♭X⟶X⟶♯X \flat X \longrightarrow X \longrightarrow \sharp X

    is a monomorphism. (Let’s maybe consider 1-toposes for the time being.)

    So every XX sits in between its two versions of opposing pure quality (pure discreteness and pure continuity in this case) and the total map is a mono. So then it is natural to ask that the factorization via XX is again by monos. In this sense the “intensive quantities” are “genuinely in between” the opposites of discreteness and continuity:

    ♭X↪X↪♯X \flat X \hookrightarrow X \hookrightarrow \sharp X

    (that the left morphism here is a mono, too, if the right one is, follows from pieces-have-points and the cancellation property of monos).

    Now maybe we should hit that with (∅⊣*)(\emptyset \dashv \ast) to get a square

    ♭∅ = ∅ = ♯∅ ↓ ↓ ↓ ♭X ↪ X ↪ ♯X ↓ ↓ ↓ ♭* = * = ♯* \array{ \flat \emptyset &=& \emptyset &=& \sharp \emptyset \\ \downarrow && \downarrow && \downarrow \\ \flat X &\hookrightarrow& X &\hookrightarrow& \sharp X \\ \downarrow && \downarrow && \downarrow \\ \flat \ast &=& \ast &=& \sharp \ast }

    and then …

    • CommentRowNumber11.
    • CommentAuthorUrs
    • CommentTimeMar 19th 2015
    • (edited Mar 19th 2015)

    (In the minutes that it takes my browser to re-typeset the entry_geometry of physics – homotopy types_ that I am working on, I easily write a few more messages here. A great incentive for procrastination…)

    I should draw the above diagram the way I actually said it in words, like this:

    ∅ = ∅ = ∅ ↓ ↓ ↓ ♭X ⟶ X ⟶ ♯X ↓ ↓ ↓ * = * = * \array{ \emptyset &=& \emptyset &=& \emptyset \\ \downarrow && \downarrow && \downarrow \\ \flat X &\longrightarrow& X &\longrightarrow& \sharp X \\ \downarrow && \downarrow && \downarrow \\ \ast &=& \ast &=& \ast }

    (where one should read ∅=∅(...)\emptyset = \emptyset (...) etc.).

    Then we see a bit better the opposing forces here:

    1. asking the middle horizontal maps to be monos gives intensive quantities;

    2. asking the left and right vertical maps to be monos gives extensive quantities;

    3. asking both to be monos implies asking XX to be a mere proposition, hence is a strong condition witnessing that the tendencies for 1) and 2) sort of oppose each other (in that it’s “hard to have both”).

    Maybe we are getting somewhere here?

    • CommentRowNumber12.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 19th 2015

    What would happen if you do this for other modal adjoints? Should we use the adjunction of the level below, rather than ∅\emptyset/*\ast always? I mean is there something aufhebung-like going on?

    • CommentRowNumber13.
    • CommentAuthorMike Shulman
    • CommentTimeMar 19th 2015

    I still need to read through this whole thread, but back at the beginning:

    given a sharp modality, then we look for the “concrete” objects XX for which the unit X↪♯XX \hookrightarrow \sharp X is a monomorphism. In a sense the anti-modal objects for which ♯X≃*\sharp X\simeq \ast are at the “opposite extreme” of these where a concrete object is all “supported on points”, a sharp-anti-modal object is maximally not supported on points.

    I would probably argue that the “opposite extreme” of the anti-modal objects (“maximally not supported on points”) would not be the concrete objects which are “supported on points”, but rather the modal/codiscrete objects (X=♯XX=\sharp X) which are “maximally supported on points”.

    • CommentRowNumber14.
    • CommentAuthorMike Shulman
    • CommentTimeMar 19th 2015

    Is “Hm, maybe, but why?” in #10 asking “why” about my proposal that

    a type X is antimodal for a comodality □ if □X = □∗

    ? I would say, because □∗ is the terminal object of the category of modal types. In other words, the antimodal types are indeed “the ones sent to the terminal object”, but we have to consider the codomain of □\square to be the category of modal types rather than the category of all types, so that by “the terminal object” we mean the terminal object in that category.

    • CommentRowNumber15.
    • CommentAuthorUrs
    • CommentTimeMar 19th 2015
    • (edited Mar 19th 2015)

    Mike, yes, that’s what I meant. Please bear with me, but I am still left wondering why that is the the condition to consider for expressing which aspect.

    In an attempt to make progress by pattern recognition, I am testing various ways of arranging the available data. This may or may not be useless, but in calling it a day and on a leisurely note, here is a pretty mandala:

    notbeing ∅ extensive↙ ↓ ↘ extensive discrete ♭X ⟶intensive X ⟶intensive ♯X continuous extensive↘ ↓ ↙ extensive * purebeing \array{ & && not\;being \\ & && \emptyset \\ & & {}^{\mathllap{extensive}}\swarrow & \downarrow & \searrow^{\mathrlap{extensive}} \\ discrete & \flat X &\stackrel{intensive}{\longrightarrow}& X & \stackrel{intensive}{\longrightarrow} & \sharp X & continuous \\ & & {}_{\mathllap{extensive}}\searrow & \downarrow & \swarrow_{\mathrlap{extensive}} \\ & && \ast \\ & && pure\;being }

    Here the labels express the kind of quality exhibited by the terms of type XX if

    1. for labels at an object: the morphism to/from that object is an equivalence;

    2. for labels at a morphism: the morphism is a mono

    (The repetition of the labels “intensive”/”extensive” goes away if we think of the diagram as being really a 3-dimensional pyramid viewed from above. Then all the “extensive” labels sit at the base and the “intensive” labels above that.)

    • CommentRowNumber16.
    • CommentAuthorMike Shulman
    • CommentTimeMar 20th 2015

    I am still left wondering why that is the the condition to consider for expressing which aspect.

    Well, the terminal object is “triviality”. More abstractly, it’s the “basepoint” in the sense of a map out of the terminal object in a category of categories-with-finite-limits, so the types sent to the terminal object are the “fiber”. And it seems to do the right thing in examples. Let’s keep sight of the mathematics. (-:

    • CommentRowNumber17.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 20th 2015

    What would the pyramid (#15) look like with entries taken from further up the ladder of modalities?

1 to 17 of 17

  1.