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-theory 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 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 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 sheaves 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 topicpractical foundations
- Category Latest Changes
- Started by Urs
- Comments 3
- Last comment by Urs
- Last Active Oct 12th 2012

I wanted to be able to point to

*practical foundations*more directly than pointing to*foundations*and hoping that the reader would spot the paragraph on practical foundations there. So I split off an entry*practical foundations*. For the moment it contains nothing but the relevant material from*foundations*copy-and-pasted

- Discussion Type
- discussion topicghost field
- Category Latest Changes
- Started by Urs
- Comments 1
- Last comment by Urs
- Last Active Oct 12th 2012

since I needed to point to it explicitly, not just via the entry

*BRST complex*, I have created an entry*ghost field*with a paragraph of text.I promise that one day I fill in more detailed discussion, but not right now.

- Discussion Type
- discussion topicmetric jet
- Category Latest Changes
- Started by Mike Shulman
- Comments 1
- Last comment by Mike Shulman
- Last Active Oct 12th 2012

created metric jet after a mention at the Café.

- Discussion Type
- discussion topicfunctional
- Category Latest Changes
- Started by Urs
- Comments 1
- Last comment by Urs
- Last Active Oct 11th 2012

there already was a bit of case distinction at

*functional*between the notion in functional analysis and the nonlinear notion in mapping space theory. I have edited a bit more, trying to polish a bit.

- Discussion Type
- discussion topiclax vs oplax colimits
- Category Latest Changes
- Started by Mike Shulman
- Comments 4
- Last comment by Todd_Trimble
- Last Active Oct 11th 2012

Ross Tate has pointed out a mismatch in terminology: Kleisli objects and the Grothendieck construction (of a covariant Cat-valued functor) are both asserted to be “lax colimits”, but they are not the same kind of colimit (the 2-cells go in different directions). Thinking about this more, I have concluded that Kleisli objects are lax colimits and the Grothendieck construction is an

*oplax*colimit. I wrote a bit about my reasoning here. But before I go changing all references to the Grothendieck construction to say “oplax colimit”, I thought I should do a sanity check — does this make sense to everyone else?

- Discussion Type
- discussion topicBPTS instanton
- Category Latest Changes
- Started by Urs
- Comments 1
- Last comment by Urs
- Last Active Oct 10th 2012

created

*BPTS instanton*

- Discussion Type
- discussion topichafnian
- Category Latest Changes
- Started by zskoda
- Comments 1
- Last comment by zskoda
- Last Active Oct 9th 2012

- Discussion Type
- discussion topicTor
- Category Latest Changes
- Started by Urs
- Comments 2
- Last comment by Urs
- Last Active Oct 8th 2012

added a basic remark on the

*Relation to torsion groups*to*Tor*.

- Discussion Type
- discussion topiclocally free module
- Category Latest Changes
- Started by Urs
- Comments 5
- Last comment by Todd_Trimble
- Last Active Oct 8th 2012

created

*locally free module*

- Discussion Type
- discussion topiccategory of modules
- Category Latest Changes
- Started by Urs
- Comments 1
- Last comment by Urs
- Last Active Oct 8th 2012

added some basic paragraphs on

*The closed monoidal structure on RMod*to*Mod*.

- Discussion Type
- discussion topictensor product of modules
- Category Latest Changes
- Started by Urs
- Comments 2
- Last comment by Urs
- Last Active Oct 8th 2012

split off

*tensor product of modules*from*tensor product*

- Discussion Type
- discussion topiccoherence theorem for monoidal bicategories
- Category Latest Changes
- Started by Mike Shulman
- Comments 2
- Last comment by Todd_Trimble
- Last Active Oct 7th 2012

- Discussion Type
- discussion topiccategory of elements
- Category Latest Changes
- Started by Mike Shulman
- Comments 1
- Last comment by Mike Shulman
- Last Active Oct 6th 2012

I added to category of elements an argument for why $El$ preserves colimits.

- Discussion Type
- discussion topiccalculus of constructions
- Category Latest Changes
- Started by Urs
- Comments 21
- Last comment by Mike Shulman
- Last Active Oct 6th 2012

I have added the following paragraph to

*calculus of constructions*, I’d be grateful if experts could briefly give me a sanity check that this is an accurate characterization:More in detail, the

*Calculus of (co)Inductive Constructions*isa system of natural deduction with dependent types;

with the natural-deduction rules for dependent product types specified;

and with a rule for how to introduce new such natural-deduction rules for arbitrary (co)inductive types.

and with a type of types (hierarchy).

- Discussion Type
- discussion topiccoherence for bicategories with finite bilimits
- Category Latest Changes
- Started by Mike Shulman
- Comments 1
- Last comment by Mike Shulman
- Last Active Oct 5th 2012

- Discussion Type
- discussion topiccomplex analytic space
- Category Latest Changes
- Started by Urs
- Comments 5
- Last comment by Urs
- Last Active Oct 3rd 2012

started

*complex analytic space*but I really have some basic questions on this topic, at the time of posting this I am really a layperson:

is it right that every complex analytic space is locally isomorphic to a polydisk?

So then they are all locally contractible as topological spaces. Are they also locally contractible as seen by étale homotopy? (So: do they admit covers by polydsisks such that if in the Cech-nerves of these covers all disks are sent to points, the resulting simplicial set is contractible?)

- Discussion Type
- discussion topicHilbert's theorem 90
- Category Latest Changes
- Started by Urs
- Comments 1
- Last comment by Urs
- Last Active Oct 2nd 2012

I copied (not: moved) the last material that Todd had added to

*projective resolution*to create an entry*Hilbert’s theorem 90*

- Discussion Type
- discussion topicexistential quantifier
- Category Latest Changes
- Started by Urs
- Comments 1
- Last comment by Urs
- Last Active Oct 2nd 2012

I have tried to brush-up

*existential quantifier*a little more. But not really happy with it yet.

- Discussion Type
- discussion topicjudgment
- Category Latest Changes
- Started by Mike Shulman
- Comments 11
- Last comment by Mike Shulman
- Last Active Oct 1st 2012

Created judgment.

- Discussion Type
- discussion topiclocal systems and coefficients
- Category Latest Changes
- Started by ronniegpd
- Comments 4
- Last comment by ronniegpd
- Last Active Oct 1st 2012

- I have added some information on the work of Henry Whitehead which is related to this topic, and referred to work of Graham Ellis, and of Higgins and I, which is relevant.

I expect I have not given the best code for all of this so someone may want to improve it in that respect.

Graham, also writes in his paper:

In view of the ease with which Whitehead's methods handle the

classifications of Olum and Jajodia, it is surprising that the

papers \cite{olum:1953} and \cite{jaj:1980} (both of which were

written after the publication of \cite{whjhc:1949}) make

respectively no use, and so little use, of \cite{whjhc:1949}.

We note here that B. Schellenberg, who was a student of Olum, has

rediscovered in \cite{sch:1973} the main classification theorems

of \cite{whjhc:1949}. The paper \cite{sch:1973} relies heavily on

earlier work of Olum.

- Discussion Type
- discussion topicempty context
- Category Latest Changes
- Started by Urs
- Comments 11
- Last comment by TobyBartels
- Last Active Oct 1st 2012

I came to wonder about the words “empty context” in type theory, for what is really the context of the unit type. For there is also the context of the empty type.‘ That

*that*might also seem to be called the “empty context”.I suppose nobody probably bothers to call the context of the empty type anything, because type theory over the empty type is the empty theory. :-)

But still, it feel terminologogically unsatisfactory. Any suggestions?

Would it not be better to speak of the

*unit context*instead of the*empty context*for the context of the unit type?Also, I keep thinking that type theory in the context of the empty type is not entirely without use. For instance it appears in the type-theoretic version of what topos-theoretically is the base change maps over

$\emptyset \to Type \to *$and that is the codomain fibration

$\mathbf{H}_{/Type} \to \mathbf{H}$with its strutcure as a

$* \simeq \mathbf{H}_{/\emptyset} \,.$*pointed*map remembered, since the point isI don’t know yet if this is super-relevant for anything, but it seems non-irrlelevant enough not to preclude it from being speakable.

- Discussion Type
- discussion topictopological ring
- Category Latest Changes
- Started by Urs
- Comments 2
- Last comment by Tim_Porter
- Last Active Sep 28th 2012

- Discussion Type
- discussion topicQFT on non-commutative spacetime
- Category Latest Changes
- Started by Urs
- Comments 1
- Last comment by Urs
- Last Active Sep 28th 2012

*QFT on non-commutative spacetime*, for the moment just to record a review paper

- Discussion Type
- discussion topic[Dedekind completion]
- Category Latest Changes
- Started by DavidRoberts
- Comments 9
- Last comment by Urs
- Last Active Sep 28th 2012

Created Dedekind completion. Probably not very satisfactory, but I lifted the main definition from Paul Taylor’s page on Dedekind cuts, so should be ok with a little tweaking.

- Discussion Type
- discussion topicmatter
- Category Latest Changes
- Started by Urs
- Comments 9
- Last comment by TobyBartels
- Last Active Sep 28th 2012

needed

*matter*to point somewhere

- Discussion Type
- discussion topicAbsolutely continuous measures
- Category Latest Changes
- Started by TobyBartels
- Comments 1
- Last comment by TobyBartels
- Last Active Sep 27th 2012

Since it appeared as a prominent grey link in integration of differential forms (and is a grey link in many other places), I wrote absolutely continuous measure.

- Discussion Type
- discussion topicaxiom
- Category Latest Changes
- Started by Todd_Trimble
- Comments 7
- Last comment by Todd_Trimble
- Last Active Sep 27th 2012

Edited the definition at the article axiom.

- Discussion Type
- discussion topicupper bound
- Category Latest Changes
- Started by Urs
- Comments 2
- Last comment by TobyBartels
- Last Active Sep 27th 2012

- Discussion Type
- discussion topicminimal coupling
- Category Latest Changes
- Started by Urs
- Comments 1
- Last comment by Urs
- Last Active Sep 27th 2012

as mentioned in another thread, I have created an entry

*minimal coupling*

- Discussion Type
- discussion topicdivisible group
- Category Latest Changes
- Started by Urs
- Comments 6
- Last comment by Urs
- Last Active Sep 27th 2012

stub for divisible group

- Discussion Type
- discussion topicinjective module
- Category Latest Changes
- Started by Urs
- Comments 1
- Last comment by Urs
- Last Active Sep 27th 2012

I have been adding basic propositons and their (farily) detailed proofs at

*injective object*in the section*Existence of enough injectives*.This expands on statements and proofs mentioned in other entries, notably at

*injective object*, also at*coextension of scalars*(stuff added by Todd, I think).Generally, it is often hard to decide in which entry exactly to put a theorem. Often there are several choices. Best of course to copy stuff to each relevant point or at least link to it from there.

But I am quite a bit time pressured now (and I hope that does not already show too much in what I just typed). So I won’t do any further such organization right now. But if anyone feels like looking into this, please don’t hesitate.

- Discussion Type
- discussion topictelescope conjecture
- Category Latest Changes
- Started by Jon Beardsley
- Comments 1
- Last comment by Jon Beardsley
- Last Active Sep 27th 2012

Created the page telescope conjecture since I noticed it was linked to by Morava K-theory but didn’t exist. Might add more later, specifically about how this is generalized to the setting of axiomatic stable homotopy categories and how it is true after localizing at $BP$, $E(n)$ and some other spectra, but believed to be false in general.

- Discussion Type
- discussion topicautomorphism infinity-group
- Category Latest Changes
- Started by Urs
- Comments 9
- Last comment by Urs
- Last Active Sep 27th 2012

Since I was being asked I briefly expanded

*automorphism infinity-group*by adding the internal version and the HoTT syntax.Mike, what’s the best type theory syntax for the definition of $\mathbf{Aut}(X)$ via $\infty$-image factorization of the name of $X$?

- Discussion Type
- discussion topichypothesis and conclusion
- Category Latest Changes
- Started by Urs
- Comments 1
- Last comment by Urs
- Last Active Sep 26th 2012

I made

*hypothesis*and*conclusion*entries or redirects to make*deduction and induction - contents*look nicer(Gee, and I was really just editing

*injective module*when the detour through Zorn’s lemma made me get distracted again by all this foundational business…)

- Discussion Type
- discussion topiccomposition
- Category Latest Changes
- Started by Urs
- Comments 2
- Last comment by Urs
- Last Active Sep 26th 2012

added to composition a new section with trivial remarks on composition in enriched category theory.

- Discussion Type
- discussion topicevaluation map
- Category Latest Changes
- Started by Urs
- Comments 1
- Last comment by Urs
- Last Active Sep 25th 2012

I have slightly touched the paragraph

*Syntax and semantics*at*evaluation map*.And then I added to the entry

*internal hom*a similar Propeties-section*internal hom - Evaluation map*

- Discussion Type
- discussion topicgeometric fibre
- Category Latest Changes
- Started by Tim_Porter
- Comments 14
- Last comment by Tim_Porter
- Last Active Sep 25th 2012

created geometric fibre. Can someone lease check these algebraic geometry entries as that area is quite far from my safety zone! so I will get some things wrong.

- Discussion Type
- discussion topicAndreas Blass
- Category Latest Changes
- Started by Tim_Porter
- Comments 1
- Last comment by Tim_Porter
- Last Active Sep 25th 2012

created a stub Andreas Blass.

- Discussion Type
- discussion topicLévy hierarchy
- Category Latest Changes
- Started by Mike Shulman
- Comments 5
- Last comment by Urs
- Last Active Sep 25th 2012

Created Lévy hierarchy.

- Discussion Type
- discussion topicfree module
- Category Latest Changes
- Started by Urs
- Comments 1
- Last comment by Urs
- Last Active Sep 24th 2012

added to

*free module*and to*submodule*a remark on the characterization of submodules of free modules.

- Discussion Type
- discussion topiclinear equation
- Category Latest Changes
- Started by Urs
- Comments 11
- Last comment by Urs
- Last Active Sep 24th 2012

I finally started

*linear equation*. But am too tired now to really do it justice…

- Discussion Type
- discussion topichomotopy category of chain complexes
- Category Latest Changes
- Started by Urs
- Comments 4
- Last comment by Urs
- Last Active Sep 24th 2012

thought we’d need an entry

*homotopy category of chain complexes*

- Discussion Type
- discussion topicstratified space : strange typos { instead of -
- Category Latest Changes
- Started by Tim_Porter
- Comments 4
- Last comment by TobyBartels
- Last Active Sep 24th 2012

In stratified space, many of the references had page numbers given as if 123 { 234, rather than 123 - 234. This is probably a paste from somewhere else, but I was wondering how it happened so as to avoid it myself. I changed it. (Might it be a strange font?)

- Discussion Type
- discussion topicquasi-isomorphism
- Category Latest Changes
- Started by Urs
- Comments 5
- Last comment by Urs
- Last Active Sep 24th 2012

I have touched

*quasi-isomorphism*, expanded the Idea-section and polished the Definition-section, added References

- Discussion Type
- discussion topicC(n)-extendible cardinals and refining Vopenka's principle
- Category Latest Changes
- Started by Mike Shulman
- Comments 1
- Last comment by Mike Shulman
- Last Active Sep 24th 2012

Recorded some facts from http://arxiv.org/abs/1101.2792 at supercompact cardinal, Vopenka’s principle, and a newly created page C(n)-extendible cardinal (with bonus stub for [[extendible cardinal]).

- Discussion Type
- discussion topicDeductions/derivations
- Category Latest Changes
- Started by TobyBartels
- Comments 1
- Last comment by TobyBartels
- Last Active Sep 23rd 2012

Urs had a framework at deduction and I put in something very brief. Also disambiguation at derivation.

- Discussion Type
- discussion topicRussell's paradox
- Category Latest Changes
- Started by Mike Shulman
- Comments 10
- Last comment by Tim_Porter
- Last Active Sep 23rd 2012

Created Russell’s paradox.

- Discussion Type
- discussion topicenough projectives/injectives
- Category Latest Changes
- Started by Urs
- Comments 1
- Last comment by Urs
- Last Active Sep 23rd 2012

I have given the section

*Existence of enough injectives*at*injective object*a bit of structure. Then I started adding some similar basics to*Existence of enough projectives*at*projective object*.

- Discussion Type
- discussion topicBurali-Forti's paradox
- Category Latest Changes
- Started by Mike Shulman
- Comments 30
- Last comment by TobyBartels
- Last Active Sep 23rd 2012

Created Burali-Forti’s paradox.

- Discussion Type
- discussion topicsequent
- Category Latest Changes
- Started by Urs
- Comments 51
- Last comment by TobyBartels
- Last Active Sep 23rd 2012

For some text I need to explain the relation between

*sequents*in the syntax of dependent type theory and*morphisms*in their categorical semantics.I wanted to explain this table:

$\,$ types terms (∞,1)-topos theory $\;\;\;\;X \stackrel{\vdash \;\;\;\;E}{\to} \;\;\Type$ $\;\;\;\;X \stackrel{\vdash \;\;\;t}{\to} {}_X \;\;E$ homotopy type theory $x : X \vdash E(x) : Type$ $x : X \vdash t(x) : E(x)$ So I was looking for a place where to put it. This way I noticed that

*sequent*used to redirect to*sequent calculus*. I think this doesn’t do justice to the notion and so I havesplit off a new entry

*sequent*added a brief Idea-blurb

added my table and some explanation leading up to it

leaving the whole entry in genuinely stubby state. But no harm done, I think, if we compare to the previous state of affairs.

- Discussion Type
- discussion topicover-(oo,1)-topos
- Category Latest Changes
- Started by Urs
- Comments 2
- Last comment by Urs
- Last Active Sep 22nd 2012

splitt off an entry over-(infinity,1)-topos with material that had been scattered elsewhere and needed to be collected in order to allow referencing it

- Discussion Type
- discussion topicsyzygy
- Category Latest Changes
- Started by Urs
- Comments 7
- Last comment by Tim_Porter
- Last Active Sep 21st 2012

started

*syzygy*.

- Discussion Type
- discussion topicinconsistency
- Category Latest Changes
- Started by Urs
- Comments 3
- Last comment by TobyBartels
- Last Active Sep 21st 2012

I have created stubs for

*inconsistency*and*contradiction*

- Discussion Type
- discussion topicuse of category: blah
- Category Latest Changes
- Started by Tim_Porter
- Comments 18
- Last comment by TobyBartels
- Last Active Sep 21st 2012

I have been adding various entries to various categories such as infinity groupoid was added to category:∞-groupoid, as it was not there! This is partially for my information as I have forgotten what entries there are on things of current interest to me, but it will explain why there seem to be a lot of entries changed by me but not in substance.

- Discussion Type
- discussion topicVojta's conjecture
- Category Latest Changes
- Started by Urs
- Comments 2
- Last comment by zskoda
- Last Active Sep 20th 2012

- Discussion Type
- discussion topiclooping combinator
- Category Latest Changes
- Started by Mike Shulman
- Comments 6
- Last comment by Mike Shulman
- Last Active Sep 20th 2012

Created looping combinator.

- Discussion Type
- discussion topicinfinity-module
- Category Latest Changes
- Started by Urs
- Comments 5
- Last comment by Urs
- Last Active Sep 20th 2012

I noticed that in

the

*∞-module*was kind of missing (we had module over an algebra over an (∞,1)-operad). So I created something stubby.

- Discussion Type
- discussion topicterm
- Category Latest Changes
- Started by Urs
- Comments 1
- Last comment by Urs
- Last Active Sep 20th 2012

When making

*inhabitant*redirect to*term*a few minutes back I also found the entry*term*to be in an unfortunate state. I tried to improve it a bit by giving it more of an Idea section, and at least a vague indication of the formal definition.

- Discussion Type
- discussion topicsalamander lemma
- Category Latest Changes
- Started by Urs
- Comments 9
- Last comment by Urs
- Last Active Sep 20th 2012

I am starting

*salamander lemma*

- Discussion Type
- discussion topicimplication
- Category Latest Changes
- Started by Urs
- Comments 4
- Last comment by Urs
- Last Active Sep 20th 2012

at

*implication*there is currently the statement$q \to r \vdash (p \to q) \to (q \to r)$,

That’s a typo, right?