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 bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-theory cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive constructive-mathematics 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 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 simplicial space spin-geometry stable-homotopy-theory string string-theory 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 topicquantum circuits via dependent linear types
- Category Latest Changes
- Started by Urs
- Comments 1
- Last comment by Urs
- Last Active 7 hours ago

Am starting a write-up (here) of how (programming languages for) quantum circuits “with classical control and/by measurement” have a rather natural and elegant formulation within the linear homotopy type theory of Riley 2022.

Aspects of this have a resemblance to some constructions considered in/with “Quipper”, but maybe it helps clarify some issues there, such as that of “dynamic lifting”.

The entry is currently written without TOC and without Idea-section etc, but rather as a single top-level section that could be

`!include`

-ed into relevant entries (such as at*quantum circuit*and at*dependent linear type theory*). But for the moment I haven’t included it anywhere yet, and maybe I’ll eventually change my mind about it.

- Discussion Type
- discussion topicvector space
- Category Latest Changes
- Started by Urs
- Comments 7
- Last comment by nLab edit announcer
- Last Active 7 hours ago

added pointer to:

- Marc Bezem, Ulrik Buchholtz, Pierre Cagne, Bjørn Ian Dundas, Daniel R. Grayson: Chapter 8 of:
*Symmetry*(2021) $[$pdf$]$

- Marc Bezem, Ulrik Buchholtz, Pierre Cagne, Bjørn Ian Dundas, Daniel R. Grayson: Chapter 8 of:

- Discussion Type
- discussion topicQuipper
- Category Latest Changes
- Started by Urs
- Comments 7
- Last comment by Urs
- Last Active 8 hours ago

added pointer to:

- Peng Fu, Kohei Kishida, Neil Ross, Peter Selinger,
*A Tutorial Introduction to Quantum Circuit Programming in Dependently Typed Proto-Quipper*, in I. Lanese, M. Rawski (eds.)*Reversible Computation*RC 2020. Lecture Notes in Computer Science, vol 12227 (arXiv:2005.08396, doi:10.1007/978-3-030-52482-1_9)

- Peng Fu, Kohei Kishida, Neil Ross, Peter Selinger,

- Discussion Type
- discussion topicinaccessible cardinal
- Category Latest Changes
- Started by DavidRoberts
- Comments 15
- Last comment by Guest
- Last Active 13 hours ago

The following sentence was at inaccessible cardinal:

A weakly inaccessible cardinal may be strengthened to produce a (generally larger) strongly inaccessible cardinal.

I have removed it after complaints by a set theorist, and in light of the below discussion box, which I have copied here and removed.

Mike: What does that last sentence mean? It seems obviously false to me in the absence of CH.

*Toby*: It means that if a weakly inaccessible cardinal exists, then a strongly inaccessible cardinal exists, but I couldn't find the formula for it. Something like $\beth_\kappa$ is strongly inaccessible if $\kappa$ is weakly inaccessible (note that $\aleph_\kappa = \kappa$ then), but I couldn't verify that (or check how it holds up in the absence of choice).Mike: I don’t believe that. Suppose that the smallest weakly inaccessible is not strongly inaccessible, and let $\kappa$ be the smallest strongly inaccessible. Then $V_\kappa$ is a model of set theory in which there are weakly inaccessibles but not strong ones. I’m almost certain there is no reason for the smallest weakly inaccessible to be strongly inaccessible.

JCMcKeown: Surely $\beth_\kappa$ has cofinality at most $\kappa$, so it can’t be regular. Maybe the strengthening involves some forcing or other change of universe? E.g., you can forcibly shift $2^\lambda = \lambda^+$ for $\lambda \lt \kappa$, and then by weak inaccessibility, etc… I

*think*. Don’t trust me. —- (some days later) More than that: since the ordinals are well ordered, if there is any strongly inaccessible cardinal*greater*than $\kappa$, then there is a*least*one, say $\theta$. Then $V_\theta$ is a universe with a weakly inaccessible cardinal and no greater strongly inaccessible cardinal. Ih! Mike said that already… So whatever construction will have to work the other way around: if there is a weakly inaccessible cardinal that isn’t strongly inaccessible, and if furthermore a weakly inaccessible cardinal implies a strongly inaccessible cardinal, then the strongly inaccessible cardinal implied must be less than $\kappa$. And that sounds really weird.I was also supplied with a AC-free proof that weakly inaccessibles are $\aleph_{(-)}$-fixed points:

First, a quick induction shows that $\alpha\leq\omega_\alpha$ is always true. If $\kappa$ is a limit cardinal, then the set of cardinals below $\kappa$ is unbounded; but since it’s also regular there are $\kappa$ of them. So $\omega_\kappa\leq\kappa\leq\omega_\kappa$, and equality ensues.

I can edit this into the page if desired.

- Discussion Type
- discussion topicPainleve transcendent
- Category Latest Changes
- Started by zskoda
- Comments 2
- Last comment by zskoda
- Last Active 1 day ago

Some important references added, including recent geometric study

- Leonid O. Chekhov, Marta Mazzocco, Vladimir N. Rubtsov,
*Painlevé monodromy manifolds, decorated character varieties, and cluster algebras*, IMRN**24**(2017) 7639–7691 doi

and a section of papers studying the mathematics of Painlevé equations and of Fuchsian $j_\Gamma$-functions from model theoretic perspective (strongly minimal structures), including a new paper in Annals 2020.

- Leonid O. Chekhov, Marta Mazzocco, Vladimir N. Rubtsov,

- Discussion Type
- discussion topicTom de Jong
- Category Latest Changes
- Started by Urs
- Comments 2
- Last comment by nLab edit announcer
- Last Active 1 day ago

brief

`category:people`

-entry for hyperlinking references at*domain theory*and*mathematics presented in HoTT*

- Discussion Type
- discussion topiccardinal number
- Category Latest Changes
- Started by nLab edit announcer
- Comments 2
- Last comment by nLab edit announcer
- Last Active 1 day ago

removing query boxes

+– {: .query}

*Madeleine Birchfield*: Wouldn’t a cardinal number be an object of the decategorification of the category Set, just as a natural number is an object of the decategorification of the category FinSet? =–+– {: .query}

*Roger Witte*First of all sorry if I am posting in the wrong placeWhile thinking about graphs, I wanted to define them as subobjects of naive cardinal

**2**and this got me thinking about the behaviour of the full subcategories of**Set**defined by isomorphism classes. These categories turned out to be more interesting than I had expected.If the background set theory is ZFC or similar, these are all large but locally small categories with all hom sets being isomorphic. They all contain the same number of objects (except

**0**, which contains one object and no non-identity morphisms) and are equinumerous with**Set**. Each hom Set contains $N^N$ arrows. In the finite case $N!$ of the morphisms in a particular hom set are isomorphisms. In particular, only**0**and**1**are groupoids. I haven’t worked out how this extends to infinite cardinalities, yet.If the background theory is NF, then they are set and

**1**is smaller than**Set**. I haven’t yet worked out how**2**compares to**1**. I need to brush up on my NF to see how NF and category theory interact.I am acutely aware that NF/NFU is regarded as career suicide by proffesional mathematicians, but, fortunately, I am a proffesional transport planner, not a mathematician.

*Toby*: Each of these categories is equivalent (but not isomorphic, except for**0**) to a category with exactly one object, which may be thought of as a monoid. Given a cardinal $N$, if you pick a set $X$ with $N$ elements, then this is (up to equivalence, again) the monoid of functions from $X$ to itself. The invertible elements of this monoid form the symmetric group, with order $N!$ as you noticed. Even for infinite cardinalities, we can say $N^N$ and $N!$, where we*define*these numbers to be the cardinalities of the sets of functions (or invertible functions) from a set of cardinality $N$ to itself.From a structural perspective, there's no essential difference between equivalent categories, so the fact that these categories (except for

**0**) are equinumerous with all of**Set**is irrelevant; what matters is not the number of objects but the number of*isomorphism classes*of objects (and similarly for morhpisms). That doesn't mean that your result that they are equinumerous with**Set**is meaningless, of course; it just means that it says more about how sets are represented in ZFC than about sets themselves. So it should be no surprise if it comes out differently in NF or NFU, but I'm afraid that I don't know enough about NF to say whether they do or not.By the way, every time you edit this page, you wreck the links to external web pages (down towards the bottom in the last query box). It seems as if something in your editor is removing URLs. =–

Anonymous

- Discussion Type
- discussion topicanafunctor
- Category Latest Changes
- Started by DavidRoberts
- Comments 6
- Last comment by Tim_Porter
- Last Active 1 day ago

- Discussion Type
- discussion topictrace
- Category Latest Changes
- Started by nLab edit announcer
- Comments 2
- Last comment by mstone
- Last Active 2 days ago

- Discussion Type
- discussion topicdirected topological space
- Category Latest Changes
- Started by nLab edit announcer
- Comments 4
- Last comment by Christoph Dorn
- Last Active 2 days ago

- Discussion Type
- discussion topicidentity type
- Category Latest Changes
- Started by Urs
- Comments 112
- Last comment by Mike Shulman
- Last Active 2 days ago

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

- Discussion Type
- discussion topiclist of theses in category theory
- Category Latest Changes
- Started by varkor
- Comments 27
- Last comment by BryceClarke
- Last Active 2 days ago

- Discussion Type
- discussion topictypes and logic - table
- Category Latest Changes
- Started by Urs
- Comments 14
- Last comment by maxsnew
- Last Active 2 days ago

created types and logic - table and all the entries to complete it.

Currently I am using this to include inside type theory - contents, which I keep reorganizing.

- Discussion Type
- discussion topicJoseph M. Renes
- Category Latest Changes
- Started by Urs
- Comments 1
- Last comment by Urs
- Last Active 2 days ago

- Discussion Type
- discussion topicGerhart Lüders
- Category Latest Changes
- Started by Urs
- Comments 1
- Last comment by Urs
- Last Active 2 days ago

- Discussion Type
- discussion topicwave function collapse
- Category Latest Changes
- Started by Urs
- Comments 4
- Last comment by Urs
- Last Active 2 days ago

I have added to

*wave function collapse*its relation to the expression for conditional expectation values in quantum probability: here (e.g. Kuperberg 05, section 1.2, Yuan 12)

- Discussion Type
- discussion topicquantum mechanics
- Category Latest Changes
- Started by Urs
- Comments 16
- Last comment by Urs
- Last Active 2 days ago

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.

- Discussion Type
- discussion topicfixed point operator
- Category Latest Changes
- Started by maxsnew
- Comments 9
- Last comment by maxsnew
- Last Active 2 days ago

- Discussion Type
- discussion topicobjective type theory
- Category Latest Changes
- Started by nLab edit announcer
- Comments 1
- Last comment by nLab edit announcer
- Last Active 3 days ago

somebody on the nForum thread on the identity type article brought up objective type theory so I thought I would start an article on that subject

Anonymous

- Discussion Type
- discussion topiceta-conversion
- Category Latest Changes
- Started by maxsnew
- Comments 2
- Last comment by nLab edit announcer
- Last Active 3 days ago

- Discussion Type
- discussion topicManuel Rivera
- Category Latest Changes
- Started by Tim_Porter
- Comments 2
- Last comment by Tim_Porter
- Last Active 3 days ago

Created a page on Manuel Rivera who has some interesting papers on the cobar construction.

- Discussion Type
- discussion topicsmooth topos
- Category Latest Changes
- Started by Urs
- Comments 3
- Last comment by nLab edit announcer
- Last Active 3 days ago

created smooth topos on the axioms on toposes used in synthetic differential geometry.

- Discussion Type
- discussion topicproduct-regular cardinal
- Category Latest Changes
- Started by nLab edit announcer
- Comments 1
- Last comment by nLab edit announcer
- Last Active 3 days ago

- Discussion Type
- discussion topiclax monoidal category
- Category Latest Changes
- Started by Mike Shulman
- Comments 11
- Last comment by varkor
- Last Active 3 days ago

- Discussion Type
- discussion topicopposite category
- Category Latest Changes
- Started by John Baez
- Comments 8
- Last comment by varkor
- Last Active 3 days ago

I made a little addition to opposite category, pointing out some amusing nuances regarding the opposite of a $V$-enriched category when $V$ is merely braided. This remark could surely be clarified, but I think you’ll get the idea.

(In case you’re wondering why I did this, it’s because I needed a reference for “opposite category” in a blog entry I’m writing.)

- Discussion Type
- discussion topicreverse monoidal category
- Category Latest Changes
- Started by David_Corfield
- Comments 2
- Last comment by varkor
- Last Active 3 days ago

- Discussion Type
- discussion topicopposite 2-category
- Category Latest Changes
- Started by varkor
- Comments 1
- Last comment by varkor
- Last Active 3 days ago

- Discussion Type
- discussion topicnecessity and possibility
- Category Latest Changes
- Started by Urs
- Comments 163
- Last comment by Urs
- Last Active 3 days ago

I have given

*necessity*and*possibility*(which used to redirect to*S4-modal logc*) an entry of their own.The entry presently

first recalls the usual axioms;

then complains that these are arguably necessary but not sufficient to characterize the idea of necessity/possibility;

and then points out that if one passes from propositional logic to first-order logic (hyperdoctrines) and/or to dependent type theory, then there is a way to axiomatize modalities that actually have the correct interpretation, namely by forming the reflection (co)monads of $\exists$ and $\forall$, respectively.

You may possibly complain, but not necessarily. Give it a thought. I was upset about the state of affairs of the insufficient axiomatics considered in modal logic for a long time, and this is my attempt to make my peace with it.

- Discussion Type
- discussion topiccategory of presheaves
- Category Latest Changes
- Started by Urs
- Comments 22
- Last comment by varkor
- Last Active 3 days ago

I felt there should be an entry category of presheaves. So I started one.

- Discussion Type
- discussion topicpseudomonoid
- Category Latest Changes
- Started by Mike Shulman
- Comments 3
- Last comment by varkor
- Last Active 4 days ago

- Discussion Type
- discussion topicgraded vector bundle
- Category Latest Changes
- Started by Dmitri Pavlov
- Comments 1
- Last comment by Dmitri Pavlov
- Last Active 4 days ago

Created:

## Definition

A

**graded vector bundle**is simply a graded object in the category of vector bundles, or, equivalently, a bundle of graded vector spaces.## Related concepts

- Discussion Type
- discussion topicset-like structures in homotopy type theory
- Category Latest Changes
- Started by nLab edit announcer
- Comments 12
- Last comment by Mike Shulman
- Last Active 4 days ago

- Discussion Type
- discussion topicclosed category
- Category Latest Changes
- Started by Tobias Fritz
- Comments 52
- Last comment by varkor
- Last Active 4 days ago

A query box has been added:

I suspect there is a variant of the definition involving a transformation $R^Z_{X Y} \colon [X,Y] \to [[Y,Z],[X,Z]]$ rather than $L$. Is this correct? If so, how do these two definitions relate? Can one of them be expressed in terms of the other? Or is there a refined definition which comprises both $L$ and $R$?

- Discussion Type
- discussion topicAnders Kock
- Category Latest Changes
- Started by varkor
- Comments 2
- Last comment by zskoda
- Last Active 4 days ago

- Discussion Type
- discussion topiclax-idempotent 2-monad
- Category Latest Changes
- Started by John Baez
- Comments 2
- Last comment by zskoda
- Last Active 4 days ago

I corrected an apparent typo:

A 2-monad $T$ as above is lax-idempotent if and only if for any $T$-algebra $a \colon T A \to A$ there is a 2-cell $\theta_a \colon 1 \Rightarrow \eta \circ a$

to

A 2-monad $T$ as above is lax-idempotent if and only if for any $T$-algebra $a \colon T A \to A$ there is a 2-cell $\theta_a \colon 1 \Rightarrow \eta_A \circ a$

It might be nice to say $\eta_A$ is the unit of the algebra….

- Discussion Type
- discussion topicrelative category
- Category Latest Changes
- Started by Dmitri Pavlov
- Comments 8
- Last comment by Hurkyl
- Last Active 4 days ago

- Discussion Type
- discussion topicaccessible category
- Category Latest Changes
- Started by Urs
- Comments 32
- Last comment by zskoda
- Last Active 4 days ago

quickly added at accessible category parts of the MO discussion here. Since Mike participated there, I am hoping he could add more, if necessary.

- Discussion Type
- discussion topicAlexander Odesskii
- Category Latest Changes
- Started by zskoda
- Comments 4
- Last comment by zskoda
- Last Active 4 days ago

- Discussion Type
- discussion topic(infinity,1)-Grothendieck construction
- Category Latest Changes
- Started by Hurkyl
- Comments 8
- Last comment by Tim_Porter
- Last Active 4 days ago

- Discussion Type
- discussion topicJonathan Beardsley
- Category Latest Changes
- Started by Urs
- Comments 2
- Last comment by Tim_Porter
- Last Active 4 days ago

changed entry title to full name,

added “category:people” tag,

updated webpage url,

added section “Related nLab entries”, so far with a pointer to

*Grothendieck construction*

- Discussion Type
- discussion topicSeverin Bunk
- Category Latest Changes
- Started by nLab edit announcer
- Comments 4
- Last comment by David_Corfield
- Last Active 5 days ago

- Discussion Type
- discussion topicpath space object
- Category Latest Changes
- Started by Urs
- Comments 2
- Last comment by Urs
- Last Active 5 days ago

added to path space object an Examples-section with some model category-theoretic discussion, leading up to the statement that in a simplicial model category for fibrant $X$ the powering $X^{\Delta[1]}$ is always a path space object.

- Discussion Type
- discussion topictype theory
- Category Latest Changes
- Started by Mike Shulman
- Comments 99
- Last comment by Mike Shulman
- Last Active 5 days ago

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

- Discussion Type
- discussion topicE-category
- Category Latest Changes
- Started by nLab edit announcer
- Comments 5
- Last comment by Mike Shulman
- Last Active 5 days ago

- Discussion Type
- discussion topicpseudo-proset
- Category Latest Changes
- Started by nLab edit announcer
- Comments 4
- Last comment by Mike Shulman
- Last Active 5 days ago

- Discussion Type
- discussion topiclocally
- Category Latest Changes
- Started by varkor
- Comments 3
- Last comment by Mike Shulman
- Last Active 5 days ago

- Discussion Type
- discussion topicprecategory
- Category Latest Changes
- Started by nLab edit announcer
- Comments 29
- Last comment by Mike Shulman
- Last Active 5 days ago

- Discussion Type
- discussion topicidentity of indiscernibles
- Category Latest Changes
- Started by Urs
- Comments 11
- Last comment by Urs
- Last Active 6 days ago

A late-night edit for entertainment – I’ll try to polish it up tomorrow when I am more awake:

I have added a translated original quote from Leibniz, as given by Gries & Schneider 1998:

Two terms are the same (eadem) if one can be substituted for the otherwithout altering the truth of any statement (salva veritate). If we have $P$ and $Q$, and $P$ enters into some true proposition, and the substitution of $Q$ for $P$ wherever it appears results in a new proposition that is likewise true, and if this can be done for every proposition, then $P$ and $Q$ are said to be the same;

Interestingly – and this is what I was searching for – Leibniz ends this paragraph with stating the converse:

conversely, if $P$ and $Q$ are the same, they can be substituted for one another.

I was chasing for a historical reference on this “principle of substitution of equals” (or what do people call it?) since this is the logical seed of path induction.

I’d like to find a more canonical reference. But not tonight.

- Discussion Type
- discussion topicEduardo Dubuc
- Category Latest Changes
- Started by zskoda
- Comments 1
- Last comment by zskoda
- Last Active 6 days ago

- Discussion Type
- discussion topicflat functor
- Category Latest Changes
- Started by Urs
- Comments 18
- Last comment by zskoda
- Last Active 6 days ago

I have added to

*flat functor*right after the very first definition (“$C \to Set$ is flat if its category of elements is cofiltered”) a remark which spells out explicitly what this means in components. Just for convenience of the reader.

- Discussion Type
- discussion topiclocalization of a 2-category
- Category Latest Changes
- Started by Urs
- Comments 3
- Last comment by zskoda
- Last Active 6 days ago

- Discussion Type
- discussion topicMichèle Audin
- Category Latest Changes
- Started by zskoda
- Comments 1
- Last comment by zskoda
- Last Active 6 days ago

- Discussion Type
- discussion topicargument shift method
- Category Latest Changes
- Started by zskoda
- Comments 1
- Last comment by zskoda
- Last Active 6 days ago

- Discussion Type
- discussion topictopological phases of matter via K-theory -- references
- Category Latest Changes
- Started by Urs
- Comments 9
- Last comment by Urs
- Last Active 6 days ago

- Discussion Type
- discussion topicHessel Posthuma
- Category Latest Changes
- Started by Urs
- Comments 1
- Last comment by Urs
- Last Active 6 days ago

- Discussion Type
- discussion topicLuuk Stehouwer
- Category Latest Changes
- Started by Urs
- Comments 1
- Last comment by Urs
- Last Active 6 days ago

- Discussion Type
- discussion topicFinInj
- Category Latest Changes
- Started by varkor
- Comments 2
- Last comment by varkor
- Last Active 6 days ago

- Discussion Type
- discussion topicJorrit Kruthoff
- Category Latest Changes
- Started by Urs
- Comments 1
- Last comment by Urs
- Last Active 6 days ago

- Discussion Type
- discussion topicsemicartesian monoidal category
- Category Latest Changes
- Started by nLab edit announcer
- Comments 13
- Last comment by varkor
- Last Active 6 days ago

- Discussion Type
- discussion topicdecidable equality
- Category Latest Changes
- Started by Mike Shulman
- Comments 5
- Last comment by nLab edit announcer
- Last Active 7 days ago

I added to decidable equality some remarks on the difference between the propositions-as-types version and the propositions-as-some-types version.