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 beauty bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality education elliptic-cohomology enriched fibration 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 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 multicategories 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 science 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).
    • created computational trinitarianism, combining a pointer to an exposition by Bon Harper (thanks to David Corfield) with my table logic/category-theory/type-theory.

    • Following discussion in some other threads, I thought one should make it explicit and so I created an entry

      Currently this contains some (hopefully) evident remarks of what “dependent linear type theory” reasonably should be at least, namely a hyperdoctrine with values in linear type theories.

      The entry keeps saying “should”. I’d ask readers to please either point to previous proposals for what “linear dependent type theory” is/should be, or criticise or else further expand/refine what hopefully are the obvious definitions.

      This is hopefully uncontroversial and should be regarded an obvious triviality. But it seems it might be one of those hidden trivialities which deserve to be highlighted a bit more. I am getting the impression that there is a big story hiding here.

      Thanks for whatever input you might have.

    • Updating reference to cubical type theory. This page need more work.

      diff, v55, current

    • brief category:people-entry for hyperlinking references

      v1, current

    • Aleks Kissinger has contacted me about his aims to start a collection of nLab entries on quantum information from the point of view of the Bob Coecke school.

      Being very much delighted about this offer, I created a template entry quantum information for his convenience.

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

      v1, current

    • a stub, to make links work

      (This used to be a stub “quantum circuit” which I just quasi-duplicated at a more extensive entry quantum circuit diagram. But since quantum gate was already redirecting here – which is how I discovered/remembered that this entry exists – no harm is done by making that it’s new title.)

      diff, v4, current

    • Add a reference for string diagrams in closed monoidal categories


      diff, v42, current

    • added to identity type a mentioning of the alternative definition in terms of inductive types (paths).

    • Decidable language =/= decidable type checking.

      Arvid Marx

      diff, v23, current

    • It should be clarified that type checking is decidable, not e.g Type inhabitation or some other property.


      diff, v10, current

    • changed page name to make it fit more systematic naming pattern

      diff, v25, current

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


      v1, current

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

      v1, current

    • I started an article about Martin-Löf dependent type theory. I hope there aren't any major mistakes!

      One minor point: I overloaded $\mathrm{cases}$ by using it for both finite sum types and dependent sum types. Can anyone think of a better name for the operation for finite sum types?

    • I created a stub certified programming.

      That’s motivated from me having expanded the Idea-section at type theory. I enjoyed writing the words “is used in industry”. There are not many nnLab pages where I can write these words.

      I am saying this only half-jokingly. Somehow there is something deep going on.

      Anyway, in (the maybe unlikely) case that somebody reading this here has lots of information about the use and relevance of certified programming in industry, I’d enjoy seeing more information added to that entry.

    • brief category:people-entry for hyperlinking references at QWIRE and related entries

      v1, current

    • brief category:people-entry for hyperlinking references at QWIRE and related entries

      v1, current

    • brief category:people-entry for hyperlinking references at QWIRE and related entries

      v1, current

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

      v1, current

    • am starting some minimum here. Have been trying to read up on this topic. This will likely become huge towards beginning of next year

      v1, current

    • Had a look at some literature and found of course that it’s vast, so have added some findings.

      diff, v4, current

    • I am trying to collect citable/authorative references that amplify the analog of the mass gap problem in particle phenomenology, where it tramslates into the open problem of computing hadron masses and spins from first principles (due to the open problem of showing existence of hadrons in the first place!).

      This is all well and widely known, but there is no culture as in mathematics of succinctly highlighting open problems such that one could refer to them easily.

      I have now created a section References – Phenomenology to eventually collect references that come at least close to making this nicely explicit. (Also checked with the PF community here)

      diff, v4, current

    • I have made explicit the example of involutive Hopf algebras, and how most of the other examples previously listed here are special cases of this one. Also expanded a little and organized it all into a new Examples-subsection (here)

      diff, v14, current

    • changed “involution” to “anti-involution”

      diff, v61, current

    • Switch commuting reasoning to use an implication for clarity.

      diff, v19, current

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

      v1, current

    • An old query at twisting cochain which was reaction to somebody putting that the motivation is the homological perturbation lemma:

      It is equally true that it is related to 20 more areas like that one (which is not the central). Brown’s paper on twisting cochains, is much earlier than homological perturbation theory. basic idea was to give algebraic models for fibrations. Nowedays you have these things in deformation theory, A-infty, gluing of complexes on varieties, Grothendieck duality on complex manifolds (Toledo-Tong), rational homotopy theory etc. One should either give a fairly balanced view to all applications or not list anything, otherwise it is not fair. This should be done together with massive expansion of Maurer-Cartan equation what is almost the same topic. The same with literature: Smirnov’s book on simplicial and operadic methods in algebraic topology is the most wide reference for twisting cochains and related issues in algebraic topology setup; Keller wrote much and well about this and Lefèvre-Hasegawa thesis (pdf) is very good, and the first reference is E. Brown’s paper from 1959. For applications in deformation theory there are many references, pretty good one from dg point of view and using 2-categorical picture of def functors is a trilogy of Efimov, Lunts and orlov on the arXiv. Few days ago Sharygin wrote a long article on twisting cochains on the arXiv, with more specific purposes in index theory. Interesting is the application of Baranovsky on constructing universal enveloping of L infty algebra. – Zoran

      Urs: concerning the “either give a fairly balanced view to all applications or not list anything”, I can see where you are coming from, Zoran, but I would still prefer here to have a little bit of material than to have none. The nnLb is imperfect almost everywhere, we’ll have to improve it incrementally as we find time, leisure and energy. But it’s good that you point out further aspects in a query box, so that we remember to fill them in later.

      Zoran Skoda My experience is that correcting a rambling and unbalanced entries takes more time than writing a new one at a stage when you really work on it. Plus all the communication explaining to others who made original entry which is hastily written. When it becomes very random and biased I stopped enjoying it at all to work on it.

      Ronnie Brown It may not possible for one person to give a “balanced entry” and is certainly not possible for me in this area. On the other hand, this may be endemic to the description of an area of maths for students and research workers.

      An advantage of the Homological Perturbation Lemma (HPL) is that it is an explicit formula, and this has been exploited by various writers, especially Gugenheim, Larry Lambe and collaborators, Huebschmann, and others, for symbolic computations in homological algebra. It is good of course to have the wide breadth of applications of twisting cochains explained.

      For me, an insight of the HPL was the explicit use of the homotopies in a deformation retract situation to lead to new results. This has been developed to calculate resolutions of groups, where one is constructing inductively a universal cover of a K(G,1)K(G,1) with its contracting homotopy.

      So let us continue to have various individually “unbalanced” points of view explained in this wiki, to let the readers be informed, and decide.

      Toby: Knowing basically nothing about this, I prefer to see various people explain their own perspectives. Even if they don't try to take the work to integrate them.