Not signed in (Sign In)

Start a new discussion

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 galois-theory 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 manifolds 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 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 string string-theory subobject superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory 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).
    • starting a sidebar contents for set theory, could add a lot more to this list


      v1, current

    • Inspired by a discussion with Martin Escardo, I created taboo.

    • adding some skeleton to this previously empty entry, no real content yet

      diff, v2, current

    • In looking for texts that would address the question “What is computation?” and arrive at an answer vaguely akin to path lifting/transport, I found (and have now added pointer to) this text:

      which gets pretty close, in particular in and around their Figure 1.

      diff, v12, current

    • a stub entry, for the moment just in order to make the link work

      v1, current

    • I have made some trivial edits to the wording, hoping to make it flow more nicely.

      By the way, this entry is linking (at least now that I adjusted the plural redirect) to recursive function. This is only natural, but – unfortunately – our entry recursive function is empty (and always has been)!

      Much of the material needed there is at partial recursive function. We should either put redirects or (better) add a little bit of content to recursive function.

      diff, v7, current

    • starting page on endomorphism monoid objects, to generalize endomorphism monoids and endomorphism rings


      v1, current

    • fix minor typo ’Bair space’ -> ’Baire space’

      Jack Crawford

      diff, v16, current

    • while bringing some more structure into the section-outline at comma category I noticed the following old discussion there, which hereby I am moving from there to here:

      [begin forwarded discussion]

      +–{.query} It's a very natural notation, as it generalises the notation (x,y)(x,y) (or [x,y][x,y] as is now more common) for a hom-set. But personally, I like (fg)(f \rightarrow g) (or (fg)(f \searrow g) if you want to differentiate from a cocomma category, but that seems an unlikely confusion), as it is a category of arrows from ff to gg. —Toby Bartels

      Mike: Perhaps. I never write (x,y)(x,y) for a hom-set, only A(x,y)A(x,y) or hom A(x,y)hom_A(x,y) where AA is the category involved, and this is also the common practice in nearly all mathematics I have read. I have seen [x,y][x,y] for an internal-hom object in a closed monoidal category, and for a hom-set in a homotopy category, but not for a hom-set in an arbitrary category.

      I would be okay with calling the comma category (or more generally the comma object) E(f,g)E(f,g) or hom E(f,g)hom_E(f,g) if you are considering it as a discrete fibration from AA to BB. But if you are considering it as a category in its own right, I think that such notation is confusing. I don’t mind the arrow notations, but I prefer (f/g)(f/g) as less visually distracting, and evidently a generalization of the common notation C/xC/x for a slice category.

      Toby: Well, I never stick ‘EE’ in there unless necessary to avoid ambiguity. I agree that the slice-generalising notation is also good. I'll use it too, but I edited the text to not denigrate the hom-set generalising notation so much.

      Mike: The main reason I don’t like unadorned (f,g)(f,g) for either comma objects or hom-sets is that it’s already such an overloaded notation. My first thought when I see (f,g)(f,g) in a category is that we have f:XAf:X\to A and g:XBg:X\to B and we’re talking about the pair (f,g):XA×B(f,g):X\to A\times B — surely also a natural generalization of the very well-established notation for ordered pairs.

      Toby: The notation (f/g/h)(f/g/h) for a double comma object makes me like (fgh)(f \to g \to h) even more!

      Mike: I’d rather avoid using \to in the name of an object; talking about projections p:(fg)Ap:(f\to g)\to A looks a good deal more confusing to me than p:(f/g)Ap:(f/g)\to A.

      Toby: I can handle that, but after thinking about it more, I've realised that the arrow doesn't really work. If f,g:ABf, g: A \to B, then fgf \to g ought to be the set of transformations between them. (Or fgf \Rightarrow g, but you can't keep that decoration up.)

      Mike: Let me summarize this discussion so far, and try to get some other people into it. So far the only argument I have heard in favor of the notation (f,g)(f,g) is that it generalizes a notation for hom-sets. In my experience that notation for hom-sets is rare-to-nonexistent, nor do I like it as a notation for hom-sets: for one thing it doesn’t indicate the category in question, and for another it looks like an ordered pair. The notation (f,g)(f,g) for a comma category also looks like an ordered pair, which it isn’t. I also don’t think that a comma category is very much like a hom-set; it happens to be a hom-set when the domains of ff and gg are the point, but in general it seems to me that a more natural notion of hom-set between functors is a set of natural transformations. It’s really the fibers of the comma category, considered as a fibration from CC to DD, that are hom-sets. Finally, I don’t think the notation (f,g)(f,g) scales well to double comma objects; we could write (f,g,h)(f,g,h) but it is now even less like a hom-set.

      Urs: to be frank, I used it without thinking much about it. Which of the other two is your favorite? By the way, Kashiwara-Schapira use M[CfEgD]M[C\stackrel{f}{\to} E \stackrel{g}{\leftarrow} D]. Maybe comma[CfEgD]comma[C\stackrel{f}{\to} E \stackrel{g}{\leftarrow} D]? Lengthy, but at least unambiguous. Or maybe fE I g{}_f {E^I}_g?

      Zoran Skoda: (f/g)(f/g) or (fg)(f\downarrow g) are the only two standard notations nowdays, I think the original (f,g)(f,g) which was done for typographical reasons in archaic period is abandonded by the LaTeX era. (f/g)(f/g) is more popular among practical mathematicians, and special cases, like when g=id Dg = id_D) and (fg)(f\downarrow g) among category experts…other possibilities for notation should be avoided I think.

      Urs: sounds good. I’ll try to stick to (f/g)(f/g) then.

      Mike: There are many category theorists who write (f/g)(f/g), including (in my experience) most Australians. I prefer (f/g)(f/g) myself, although I occasionally write (fg)(f\downarrow g) if I’m talking to someone who I worry might be confused by (f/g)(f/g).

      Urs: recently in a talk when an over-category appeared as C/aC/a somebody in the audience asked: “What’s that quotient?”. But (C/a)(C/a) already looks different. And of course the proper (Id C/const a)(Id_C/const_a) even more so.

      Anyway, that just to say: i like (f/g)(f/g), find it less cumbersome than (fg)(f\downarrow g) and apologize for having written (f,g)(f,g) so often.

      Toby: I find (fg)(f \downarrow g) more self explanatory, but (f/g)(f/g) is cool. (f,g)(f,g) was reasonable, but we now have better options.


    • At comma object, Eduardo Pareja-Tobes put a query box which does not seem to have been ‘answered’. This was some time ago it seems.

    • Created page and added some references.

      v1, current

    • removing query box from page

      +– {: .query} Mike Shulman: Is there a formal statement in some formal system along the lines of “a non-extensional choice operator does not imply AC”?

      Toby: I don't know about a formal statement, but I can give you an example.

      Recall: In Per Martin-Löf's Intuitionistic Type Theory (and many other systems along similar lines), the basic notion axiomatised is not really that of a set (even though it might be called ’set’) but instead a preset (or ’type’). Often one hears that the axiom of choice does hold in these systems, which doesn't imply classical logic due to a lack of quotient (pre)sets. However, if we define a set to be a preset equipped with an equivalence predicate, then the axiom of choice fails (although we have COSHEP if presets come with an identity predicate).

      A lot of these systems (including Martin-Löf's) use ’propositions as types’, in which x:AP(x)\exists_{x:A} P(x) is represented as x:AP(x)\sum_{x:A} P(x), which comes equipped with an operation π: x:AP(x)A\pi: \sum_{x:A} P(x) \to A. That is not going to get us our choice operator, but since a choice operator is constructively questionable anyway, then let's throw in excluded middle. This is known to not imply choice, but we do have, for every preset AA, an element ε A\varepsilon_A of A¬AA \vee \neg{A}, that is of A AA \uplus \empty^A. It's not literally true that ε A\varepsilon_A is of type AA, of course, but that would be unreasonable in a structural theory; what we do have is a fixed ε A\varepsilon_A such that, if AA is inhabited, then ε A=ι A(e)\varepsilon_A = \iota_A(e) for some (necessarily unique) ee of type AA (where ι A\iota_A is the natural inclusion AA AA \to A \uplus \empty^A), which I think should be considered good enough. This is for presets (types), but every set has a type of elements, so that gets us our operator.

      How is this nonextensional? We do have ε A=ε B\varepsilon_A = \varepsilon_B if A=BA = B (which is a meaningful statement to Martin-Löf, albeit not a proposition exactly), but if AA and BB are given as subsets of some UU, then we may well have A=BA = B as subsets of UU without A=BA = B in the sense of identity of their underlying (pre)sets. In particular, if f:UVf: U \to V is a surjection and AA and BB are the preimages of elements xx and yy of VV, then x= Vyx =_V y will not imply that ε A=ε B\varepsilon_A = \varepsilon_B, and the proof of the axiom of choice does not go through. It will go through if xx and yy are identical, that is if x=yx = y in the underlying preset of VV, so again we do get choice for presets (again), but not for sets.

      I'm not certain that a nonextensional global choice operator won't imply excluded middle in some other way, but I don't see how it would. You'd want to do something with the idea that ε A\varepsilon_A always exists but belongs to AA if and only if AA is inhabited, but I don't see how to parse it (just by assuming that it exists) to decide the question.

      Mike Shulman: That’s a very nice explanation/example, and it did help me to understand better what’s going on; thanks! (Did you mean to say “excluded middle” and not “AC” in your final paragraph?) What I would really like, though, is a statement like “the addition of a nonextensional global choice operator to ____ set theory is conservative” (i.e. doesn’t enable the proving of any new theorems that doen’t refer explicitly to the choice operator). Of course I am coming from this comment, wondering whether what you suggested really is a way to get a choice operator without implying the axiom of choice.

      Toby: Yeah, I really did mean to say ’excluded middle’; remembering that comment, I assume that the real question is whether the thing is OK for a constructivist. I just argued ITT+EMCO\mathbf{ITT} + EM \vDash CO, and I know the result ITT+EM¬AC\mathbf{ITT} + EM \not\vDash AC, so I conclude ITT+CO¬AC\mathbf{ITT} + CO \not\vDash AC; but I don't know ITT+CO¬EM\mathbf{ITT} + CO \not\vDash EM for certain. I certainly don't have ITT+CO\mathbf{ITT} + CO conservative over ITT\mathbf{ITT}, nor with any other theory (other than those that already model COCO, obviously).

      Mike Shulman: Where should I look for a proof that ITT+EM\mathbf{ITT} + EM doesn’t imply AC?

      Toby: I'm not sure, it's part of my folk knowledge now. Probably Michael J. Beeson's Foundations of Constructive Mathematics is the best bet. I'll try to get a look in there myself next week; I can see that it's not exactly obvious, and perhaps my memory is wrong now that I think about it.

      Mike Shulman: I’m trying to prove the sort of statement I want over at SEAR+?.

      Toby: No, I can't get anything at all out of Beeson (or other references) about full AC (for types equipped with equivalence relations) in ITT\mathbf{ITT}.

      Harry Gindi: I have references for this discussion that should settle the issue at hand:

      Bell, J. L., 1993a. ’Hilbert’s epsilon-operator and classical logic’, Journal of Philosophical Logic, 22:1-18

      Bell, J. L., 1993b. ’Hilbert’s epsilon operator in intuitionistic type theories’, Mathematical Logic Quarterly 39:323-337

      Meyer Viol, W., 1995a. ’A proof-theoretic treatment of assignments’, Bulletin of the IGPL, 3:223-243

      Toby: Thanks, Harry! Now I just have to find these journals at the library. =–


      diff, v26, current

    • Created this page with the defintion of a terminating rewriting system. It was linked on the page “rewriting”.

      v1, current

    • starting article on the differences between set theory and dependent type theory


      v1, current

    • Only a stub at the moment, but I thought we needed to start a page on this. Looks like it’s going to become important.

      v1, current

    • adding section on the universal quantifier in dependent type theory


      diff, v25, current

    • Change 1: Original page describes the fan theorem as requiring the bar to be decidable, claims that the “classical” fan theorem contradicts Brouwer’s continuity principle. The latter claim is not true; I corrected the error. I have stated the result as two separate theorems: the decidable fan theorem, about decidable bars, and the fan theorem, about bars in general.

      Change 2: Slightly more information is provided about the relationship between the Fan Theorem and Bar Induction. Eventually, we should make a page about the latter.

      Change 3: the section on equivalents to the fan theorem has been fixed somewhat. The section originally asserted that all of the statements provided were equivalent to the decidable fan theorem; in fact, some are equivalent to the decidable fan theorem and some to the full fan theorem.

      diff, v22, current

    • created a minimum at function monad (aka “reader monad”, “environment monad”)

    • I have removed the bulk of the Idea section that I had written, starting way back when the entry was created in 2013.

      I kept the other material that Mike (Shulman) had written.

      I see now that mine was really besides the point.

      Now that I finally understand this topic more deeply, maybe I find time to write a better explanation of what’s really going on.

      diff, v58, current

    • I am finally giving this its own page, for ease of linking to it.

      Unfortunately the term is not self-explanatory: it’s implicitly short for something like “dynamic lifting of quantum measurement results back into a classical computational context”

      v1, current

    • brief category:people-entry for hyperlinking references

      v1, current

    • brief category:people-entry for hyperlinking references

      v1, current

    • Init page and try to describe why some computer scientists have wacky names like catamorphism for a homomorphism out of an initial algebra.

      Not sure what “context” sidebar to put here. Do we have one for just “computer science” or more specifically here “functional programming”?

      v1, current

    • I tried to implement the connection between D-modules and quasicoherent sheaves a bit more

      • added to D-module the alternative definition in terms of quasicoherent sheaves of the deRham space

      • added to deRham space accordingly a pointer to D-modules (also fixed wrong notation in the formulas there)

      • added to quasicoherent sheaf at the very bottom a pointer to D-modules.

      This needs improving. Notably good references should be given.

    • Page created, but author did not leave any comments.


      v1, current

    • added definitions of cosine function


      diff, v8, current

    • added the series definition of a sine function


      diff, v9, current

    • added a section on defining the exponential function in real algebras.


      diff, v33, current

    • I am starting something at six operations.

      (Do we already have an nLab page on this? I seemed to remember something, but can’t find it.)

    • Added two propositions about the general case of monoids and comonoids in a closed monoidal categories. It looks that it could work in such a general context and thus be used in models of linear logic or in differential categories, so that’s exciting. I’ll try to prove them.

      diff, v6, current

    • brief category:people-entry for hyperlinking references

      v1, current

    • brief category:people-entry for hyperlinking references

      v1, current

    • brief category:people-entry for hyperlinking references

      v1, current

    • stub entry, for the moment just to record some references

      v1, current

    • brief category:people-entry for hyperlinking references

      v1, current

    • in analogy to what I just did at classical mechanics, I have now added some basic but central content to quantum mechanics:

      • Quantum mechanical systems

      • States and observables

      • Spaces of states

      • Flows and time evolution

      Still incomplete and rough. But I have to quit now.

    • Wikipedia has a nice article on quantum operations.

      The nLab also had a page quantum operations and channels (cache bug?), but I’ve renamed this to simply quantum operation since a quantum channel seems to be nothing but a quantum operation when viewed from the perspective of quantum information theory. Eventually, this page might need some disambiguation since there may be several uses of the term, but for now I think it is “ok”.

      I think this page can be cleaned up. I started, but don’t think I will be able to finish.

      In particular, there is some background material that might be better on separate pages. I’ll continue trying to clean things up, but family might be calling soon and I’ll need to run quickly whatever state it is in.

      I also made the simple statement

      In quantum mechanics, a quantum operation is a morphism in the category of density matrices

      at the beginning of the Idea section motivated by O’Loan’s comment

      A quantum channel is a mapping which sends density matrices to density matrices.

      This seems innocent enough, but someone might check the statement. For one, I’ve never seen a category of density matrices, but the idea seems obvious enough. Maybe a word on density matrix would be good.

    • now creating this entry.

      The technical material under “Details” (here) is copied over from what I had written at reader monad – Examples – quantum reader monad. (There may still be room left to adjust the wording in order to reflect that this material moved to a new entry.)

      To this I have now added an Idea-section (here) which highlights the relation to (equivalence with) Bob Coecke’s “classical structures” (which term I made redirect to here now)

      v1, current

    • a stub entry, for the moment just to make links work

      v1, current