Not signed in (Sign In)

A discussion forum about contributions to the nLab wiki and related areas of mathematics, physics, and philosophy.

Want to take part in these discussions? Sign in if you have an account, or apply for one below

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.

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

- Discussion Type
- discussion topiccomputational trinitarianism
- Category Latest Changes
- Started by Urs
- Comments 34
- Last comment by Urs
- Last Active 2 hours ago

created

*computational trinitarianism*, combining a pointer to an exposition by Bon Harper (thanks to David Corfield) with my table logic/category-theory/type-theory.

- Discussion Type
- discussion topicMitchell Riley
- Category Latest Changes
- Started by Urs
- Comments 1
- Last comment by Urs
- Last Active 2 hours ago

brief

`category:people`

-entry for hyperlinking references at*dependent linear type theory*and elsewhere

- Discussion Type
- discussion topicquantum computation
- Category Latest Changes
- Started by Urs
- Comments 10
- Last comment by Urs
- Last Active 4 hours ago

stub for

*quantum computation*

- Discussion Type
- discussion topicSimon J. Devitt
- Category Latest Changes
- Started by Urs
- Comments 1
- Last comment by Urs
- Last Active 4 hours ago

brief

`category:people`

-entry for hyperlinking references at*quantum error correction*and at*quantum computation*

- Discussion Type
- discussion topicMartin Lundfall
- Category Latest Changes
- Started by Urs
- Comments 1
- Last comment by Urs
- Last Active 5 hours ago

brief

`category:people`

-entry for hyperlinking references at*dependent linear type theory*

- Discussion Type
- discussion topicdependent linear type theory
- Category Latest Changes
- Started by Urs
- Comments 76
- Last comment by Urs
- Last Active 5 hours ago

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.

- Discussion Type
- discussion topicbeta-gamma system
- Category Latest Changes
- Started by Urs
- Comments 2
- Last comment by Luigi
- Last Active 7 hours ago

added a definition to

*beta-gamma system*

- Discussion Type
- discussion topicside effect
- Category Latest Changes
- Started by Urs
- Comments 1
- Last comment by Urs
- Last Active 9 hours ago

added pointer to:

- Matthijs Vákár,
*In Search of Effectful Dependent Types*(arXiv:1706.07997, uuid:e91e19b3-7e10-4fda-9433-f23b469e4049)

- Matthijs Vákár,

- Discussion Type
- discussion topicHomotopy Type Theory -- Univalent Foundations of Mathematics
- Category Latest Changes
- Started by Urs
- Comments 27
- Last comment by Urs
- Last Active 9 hours ago

I had given it an $n$Lab page already a while back, so that I could stably link to it without it being already there:

Now it’s even “there” in the sense of being incarnated as a pdf.

- Discussion Type
- discussion topicunivalence axiom
- Category Latest Changes
- Started by spitters
- Comments 29
- Last comment by Urs
- Last Active 9 hours ago

- Discussion Type
- discussion topicBernhard Ömer
- Category Latest Changes
- Started by Urs
- Comments 1
- Last comment by Urs
- Last Active 11 hours ago

- Discussion Type
- discussion topicquantum programming languages -- references
- Category Latest Changes
- Started by Urs
- Comments 6
- Last comment by Urs
- Last Active 11 hours ago

a bare list of references, to be

`!includ`

-ed into the list of references of relevant entries, such as at*quantum computing*and*quantum programming*, for ease of updating and syncing

- Discussion Type
- discussion topicClaudia Faggian
- Category Latest Changes
- Started by Urs
- Comments 1
- Last comment by Urs
- Last Active 11 hours ago

brief

`category:people`

-entry for hyperlinking references at*quantum circuit diagram*

- Discussion Type
- discussion topicGiulio Casati
- Category Latest Changes
- Started by Urs
- Comments 1
- Last comment by Urs
- Last Active 12 hours ago

brief

`category:people`

-entry for hyperlinking references at*quantum computation*and*quantum information*

- Discussion Type
- discussion topicGiuliano Benenti
- Category Latest Changes
- Started by Urs
- Comments 1
- Last comment by Urs
- Last Active 12 hours ago

brief

`category:people`

-entry for hyperlinking references at*quantum computation*and*quantum information*

- Discussion Type
- discussion topicDavide Rossini
- Category Latest Changes
- Started by Urs
- Comments 1
- Last comment by Urs
- Last Active 12 hours ago

brief

`category:people`

-entry for hyperlinking references at*quantum computation*and*quantum information*

- Discussion Type
- discussion topicShor's algorithm
- Category Latest Changes
- Started by Urs
- Comments 2
- Last comment by Urs
- Last Active 12 hours ago

- Discussion Type
- discussion topicquantum information
- Category Latest Changes
- Started by Urs
- Comments 14
- Last comment by Urs
- Last Active 12 hours ago

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.

- Discussion Type
- discussion topicquantum complexity theory
- Category Latest Changes
- Started by Urs
- Comments 1
- Last comment by Urs
- Last Active 12 hours ago

- Discussion Type
- discussion topicJarosław Adam Miszczak
- Category Latest Changes
- Started by Urs
- Comments 1
- Last comment by Urs
- Last Active 12 hours ago

brief

`category:people`

-entry for hyperlinking references at*quantum programming language*

- Discussion Type
- discussion topicquantum gate
- Category Latest Changes
- Started by Urs
- Comments 1
- Last comment by Urs
- Last Active 13 hours ago

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

- Discussion Type
- discussion topicquantum circuit diagram
- Category Latest Changes
- Started by Urs
- Comments 2
- Last comment by Urs
- Last Active 13 hours ago

- Discussion Type
- discussion topicstring diagram
- Category Latest Changes
- Started by nLab edit announcer
- Comments 40
- Last comment by Urs
- Last Active 13 hours ago

- Discussion Type
- discussion topicER = EPR
- Category Latest Changes
- Started by Luigi
- Comments 4
- Last comment by Urs
- Last Active 13 hours ago

- Discussion Type
- discussion topicholographic entanglement entropy
- Category Latest Changes
- Started by Urs
- Comments 19
- Last comment by Urs
- Last Active 13 hours ago

created a stub for

*holographic entanglement entropy*in reaction to this MO question.

- Discussion Type
- discussion topicidentity type
- Category Latest Changes
- Started by Urs
- Comments 32
- Last comment by Urs
- Last Active 14 hours ago

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

- Discussion Type
- discussion topicextensional type theory
- Category Latest Changes
- Started by nLab edit announcer
- Comments 4
- Last comment by Urs
- Last Active 14 hours ago

- Discussion Type
- discussion topicintensional type theory
- Category Latest Changes
- Started by nLab edit announcer
- Comments 2
- Last comment by Urs
- Last Active 14 hours ago

- Discussion Type
- discussion topicFrans R. Klinkhamer
- Category Latest Changes
- Started by Urs
- Comments 1
- Last comment by Urs
- Last Active 15 hours ago

brief

`category:people`

-entry for hyperlinking references at*IKKT matrix model*

- Discussion Type
- discussion topicD=5 supergravity
- Category Latest Changes
- Started by Urs
- Comments 3
- Last comment by Urs
- Last Active 15 hours ago

- Discussion Type
- discussion topicCayley distance kernel
- Category Latest Changes
- Started by Urs
- Comments 141
- Last comment by Urs
- Last Active 1 day ago

for completeness, to go alongside

*Mallows kernel*

- Discussion Type
- discussion topichook length formula
- Category Latest Changes
- Started by David_Corfield
- Comments 1
- Last comment by David_Corfield
- Last Active 1 day ago

- Discussion Type
- discussion topic!-modality
- Category Latest Changes
- Started by Urs
- Comments 21
- Last comment by Urs
- Last Active 1 day ago

collected some references on the interpretation of the !-modality as the Fock space construction at

*!-modality*.Cross-linked briefly with he stub entries_Fock space_ and

*second quantization*.

- Discussion Type
- discussion topicmagmoidal category
- Category Latest Changes
- Started by nLab edit announcer
- Comments 8
- Last comment by DavidRoberts
- Last Active 1 day ago

- Discussion Type
- discussion topicquantum logic
- Category Latest Changes
- Started by Urs
- Comments 39
- Last comment by Urs
- Last Active 1 day ago

have expanded the Idea-section at

*quantum logic*to now read as follows:

Broadly speaking,

*quantum logic*is meant to be a kind of formal logic that is to traditional formal logic as quantum mechanics is to classical mechanics.The first proposal for such a formalization was (Birkhoff-vonNeumann 1936), which suggested that given a quantum mechanical system with a Hilbert space of states, the logical propositions about the system are to correspond to (the projections to) closed subspaces, with implication given by inclusion of such subspaces, hence that quantum logic is given by the lattice of closed linear subspaces of Hilbert spaces.

This formalization is often understood as being the default meaning of “quantum logic”. But the proposal has later been much criticized, for its lack of key properties that one would demand of a formal logic. For instance in (Girard 11, page xii) it says:

Among the magisterial mistakes of logic, one will first mention quantum logic, whose ridiculousness can only be ascribed to a feeling of superiority of the language – and ideas, even bad, as soon as they take a written form – over the physical world. Quantum logic is indeed a sort of punishment inflicted on nature, guilty of not yielding to the prejudices of logicians… just like Xerxes had the Hellespont – which had destroyed a boat bridge – whipped.

and for more criticisms see (Girard 11, section 17).

Therefore later other proposals as to what quantum logic should be have been made, and possibly by “quantum logic” in the general sense one should understand any formal framework which is supposed to be able to

*express*the statements whose semantics is the totality of all what is verifiable by measurement in a quantum system.In particular it can be argued that flavors of

*linear logic*and more generally*linear type theory*faithfully capture the essence of quantum mechanics (Abramsky-Duncan 05, Duncan 06, see (Baez-Stay 09) for an introductory exposition) due to its categorical semantics in symmetric monoidal categories such as those used in the desctiption of finite quantum mechanics in terms of dagger-compact categories. In particular the category of (finite dimensional) Hilbert spaces that essentially underlies the Birkhoff-vonNeumann quantum logic interprets linear logic.Another candidate for quantum logic has been argued to be the internal logic of Bohr toposes .

In quantum computing the quantum analog of classical logic gates are called

*quantum logic gates*.

- Discussion Type
- discussion topicHarley Eades
- Category Latest Changes
- Started by Urs
- Comments 1
- Last comment by Urs
- Last Active 1 day ago

- Discussion Type
- discussion topictype theory
- Category Latest Changes
- Started by Mike Shulman
- Comments 93
- Last comment by Urs
- Last Active 1 day ago

I incorporated some of my spiel from the blog into the page type theory.

- Discussion Type
- discussion topicMartin-Löf dependent type theory
- Category Latest Changes
- Started by Zhen Lin
- Comments 27
- Last comment by Urs
- Last Active 1 day ago

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?

- Discussion Type
- discussion topiccertified programming
- Category Latest Changes
- Started by Urs
- Comments 25
- Last comment by Urs
- Last Active 1 day ago

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 $n$Lab 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.

- Discussion Type
- discussion topicSteve Zdancewic
- Category Latest Changes
- Started by Urs
- Comments 1
- Last comment by Urs
- Last Active 1 day ago

- Discussion Type
- discussion topicRobert Rand
- Category Latest Changes
- Started by Urs
- Comments 1
- Last comment by Urs
- Last Active 1 day ago

- Discussion Type
- discussion topicJennifer Paykin
- Category Latest Changes
- Started by Urs
- Comments 1
- Last comment by Urs
- Last Active 1 day ago

- Discussion Type
- discussion topicQWIRE
- Category Latest Changes
- Started by Urs
- Comments 1
- Last comment by Urs
- Last Active 1 day ago

one more in the list of quantum programming languages

- Discussion Type
- discussion topichomotopy type theory
- Category Latest Changes
- Started by Urs
- Comments 54
- Last comment by Urs
- Last Active 1 day ago

stub for homotopy type theory

- Discussion Type
- discussion topichook-content formula
- Category Latest Changes
- Started by Urs
- Comments 4
- Last comment by David_Corfield
- Last Active 1 day ago

- Discussion Type
- discussion topicleptoquark
- Category Latest Changes
- Started by Urs
- Comments 37
- Last comment by Urs
- Last Active 1 day ago

- Discussion Type
- discussion topicflavour anomaly
- Category Latest Changes
- Started by Urs
- Comments 166
- Last comment by Urs
- Last Active 1 day ago

- Discussion Type
- discussion topicEI-category
- Category Latest Changes
- Started by David_Corfield
- Comments 9
- Last comment by varkor
- Last Active 2 days ago

- Discussion Type
- discussion topicKlaus Mainzer
- Category Latest Changes
- Started by Urs
- Comments 1
- Last comment by Urs
- Last Active 2 days ago

brief

`category:people`

-entry for hyperlinking references at*certified programming*

- Discussion Type
- discussion topicMihhail Aizatulin
- Category Latest Changes
- Started by Urs
- Comments 1
- Last comment by Urs
- Last Active 2 days ago

brief

`category:people`

-entry for hyperlinking references at*verified programming*and at*cryptography*

- Discussion Type
- discussion topiccryptography
- Category Latest Changes
- Started by zskoda
- Comments 2
- Last comment by Urs
- Last Active 2 days ago

Stub. For now just recording links which go beyond the scope of arithmetic cryptography.

- Discussion Type
- discussion topicAdam Petcher
- Category Latest Changes
- Started by Urs
- Comments 1
- Last comment by Urs
- Last Active 2 days ago

brief

`category:people`

-entry for hyperlinking references at*verified programming*

- Discussion Type
- discussion topicPaventhan Vivekanandan
- Category Latest Changes
- Started by Urs
- Comments 1
- Last comment by Urs
- Last Active 2 days ago

brief

`category:people`

-entry for hyperlinking references at*verified programming*

- Discussion Type
- discussion topicmass gap
- Category Latest Changes
- Started by Urs
- Comments 21
- Last comment by Urs
- Last Active 2 days ago

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)

- Discussion Type
- discussion topicstar-algebra
- Category Latest Changes
- Started by Urs
- Comments 2
- Last comment by Urs
- Last Active 2 days ago

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)

- Discussion Type
- discussion topicC-star-algebra
- Category Latest Changes
- Started by Urs
- Comments 1
- Last comment by Urs
- Last Active 2 days ago

- Discussion Type
- discussion topicinvolution
- Category Latest Changes
- Started by bgm
- Comments 2
- Last comment by Urs
- Last Active 2 days ago

- Discussion Type
- discussion topicHopf algebra
- Category Latest Changes
- Started by Urs
- Comments 22
- Last comment by Urs
- Last Active 2 days ago

added to the Properties-section at Hopf algebra a brief remark on their interpretation as 3-vector spaces.

- Discussion Type
- discussion topic(classical) axiom of multiple choice
- Category Latest Changes
- Started by Brian Pinsky
- Comments 3
- Last comment by Mike Shulman
- Last Active 2 days ago

- Discussion Type
- discussion topictwisting cochain
- Category Latest Changes
- Started by zskoda
- Comments 4
- Last comment by zskoda
- Last Active 2 days ago

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 $n$Lb 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)$ 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.