Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
created a minimum at computable real number, for the moment just so as to record the references with section numbers as given there.
happened to need Type Two Theory of Effectivity
just in case you are watching the logs and are wondering:
I think we should have another “floating table of contents” for collecting the topic cluster
so I am starting one at constructivism - contents and am including it into relevant entries.
But right now there is nothing much there yet. This is going to be expanded.
it seems that orthomodular lattice had been missing, so I created a bare minimum
stub tertiary radical with redirects third radical, tertiary decomposition theory
Created a brief entry transfer context in order to record an observation by Haugseng.
He defines a transfer context to be a linear homotopy-type theory aka Wirthmüller context in which not only but also satisfies its projection formula. Then he observes that a natural Umkehr map that may be built with this projection formula is (the abstract generalization of) the Becker-Gottlieb transfer.
(Have briefly cross-linked with these related entries.)
Thanks to Thomas Nikolaus for being reminded of Haugseng’s work when Joost Nuiten and me talked about something closely related as ESI yesterday.
uniform module (related also to essential submodule)
I created a link to axiom of pairing from constructible universe, then satisfied it.
I added some basic definitions to stability in model theory. No attempt yet to motivate them.
Some of the logic entries seem to be in a slight state of neglect, e.g., theory. I might want to get in there sometime soon, but anyone should please feel free to precede me.
I am adding some bits and pieces to geometric stability theory (which I am trying to learn more about these days).
created a stub for Chern-Simons gravity. But nothing much there yet.
started Hecke category with some bare minimum
started a bare minimum at horocycle correspondence
for some reason it seems we never had an entry compactly generated (infinity,1)-category (and out of all sections listed at HTT just 5.5.7 had been missing for some reason which is a mystery to me now).
I gave it a minimum of content. But this alerts one that there is a distinction being made here which we don’t have in the corresponding 1-categorical entries.
I’ve been adding material to Polish space, and plan on adding more (mostly in view of model-theoretic considerations).
started monad (in computer science)
(also added it as one line to the big table at computational trinitarianism)
created a stub for completion monad.
In the course of doing so I found it unfortunate that the link constructive analysis simply redirected to analysis, a page from which the constructive formulation and the point of it was hardly to be extracted. So I have split off constructive analysis right now. But except for a sentence pointing back to the completion monad, it just contains for the moment the list of references that we already had.
cretaed a brief entry K-motive in order to record a cool statement somewhat hidden in an article by Tabuada froma year back. Thanks a lot for Adeel Khan Yusufzai for pointing this out!
I changed the entry Cahiers to state that the free back issues are only available up until 2008, rather than with a two-year moving wall, as one can check. Also, I notice that the journal home page and the TAC mirror of the contents is a year behind (only info up till the end of 2012). Does anyone know anything about this?
brief entry perfect infinity-module with the definition and the main property
I was disappointed to discover that Boman's theorem doesn't work as one would like for functions with . So I wrote up something about it. (This is all in Boman's 1967 paper; he covered everything in 20 freely accessible pages!)
I gave Todd’s note A string diagram calculus for predicate logic a category:reference entry, turned the ps-file into a pdf and linked to it there, and then added pointers to this from relevant entries, such as hyperdoctrine and indexed monoidal categories, each going along with pointers to Ponto-Shulman.
This in an attempt to make more visible all the little pointers that are (or were now) hidden behind “here”-s at string diagram. Eventually that entry should be a bit clearer about what all that stuff is that it secretly subsumes.
Todd had filled in some text at Trimble rewiring. I have added a few more hyperlinks now and a floating TOC.
Todd, when you have another minute, could you say a bit more specifically what a Trimble rewiring does? Which kinds of diagrams are rewired how, and what’s the deal?
Created a stub for Kelly-Mac Lane graph to start recording some references
just so that there are (cross-)links to them, I have created brief stub entries on some linear connectives:
and we already talked about
I ’corrected’ the title of Serre’s criterion of affineness. I don’t like that word ‘affineness’!
the nLab was lacking an entry invertible object. I have started a minimum there, just so as to satisfy links for the moment.
stub for coherent (infinity,1)-topos, just to record the pointers to the DAGs.
(Thanks to Marc Hoyois for pointing out the hidden proposition in DAG XIII…)
The link bilimit used to redirect to 2-limit. With this the reader following this might miss the sense of biproducts.
I have now removed the redirects and instead made bilimit a category:disambiguation-page. Hopkins-Lurie suggest to speak of “ambidextrous diagrams” (spaces) instead, which is maybe an option out of the terminology clash.
So finally at ambidextrous adjunction I have added the case of coinciding limits and colimits as an example.
created finite homotopy type, just for completeness.
This just a distraction when I saw that it was missing,while I was really going to create an entry on truncated homotopy types with finite homotopy groups.
The main problem about them is that nobody agrees on how to call them ;-)
In groupoid cardinality they have been called “tame”, some call them -finite,I suppose, and homological algebra suggests “of finite type”, which in itself is good, however rather badly goes together with the crucially different “finite homotopy type”.
Jim Stasheff asked me to give a list of examples of applications of Kan extension in physics.
Since this shouldn’t be hidden away in private email, I have started a section Kan extension – Examples – Kan extension in physics
There will be many examples, two came immediately to mind, and so for the moment I have added there the following, to be expanded:
We list here some occurences of Kan extensions in physics.
Notice that since, by the above discussion, Kan extensions are ubiquitous in category theory and are essentially equivalent to other standard universal constructions such as notably co/limits, to the extenent that there is a relation between category theory and physics at all, it necessarily also involves Kan extensions, in some guise. But here is a list of some example where they appear rather explicitly.
In extended quantum field theory on open and closed manifolds, usually the theory “in the bulk” (on closed manifolds) is induced by “extending” that “on the boundary”, and in good cases this extension is explicitly a (homotopy)-Kan extension. This is the case notably for 2d TQFT in the form of TCFT (Costello 04), see at TCFT – Classification for details.
When path integral quantization is formalized in terms of fiber integration in generalized cohomology (as surveyed at _motivic quantization) then the push-forward step, hence the path integral itself, is given by left homotopy Kan extension of parameterized spectra. For explicit details see (Nuiten 13, section 4.1), also (Schreiber 14, section 6.2). By example 6.3 there a special case of this is are the integration formulas via Kan extension in (Hopkins-Lurie 14, section 4).
Urs put a stub at equicontinuous function; I moved this to equicontinuous family of functions, added many many other redirects, and expanded it. It’s still basically just definitions, however.
am starting K(n)-local stable homotopy theory .
stub for semiadditive (infinity,1)-category, for the moment just so as to record the pointer.
The link to Joyal’s Catlab discussion at Cisinski model structure leads to a page on his Lab at which the main link points to a non-existent pdf document at Paris 13. We have the correct link at Cisinski model structure, namely to his Toulouse address (http://www.math.univ-toulouse.fr/~dcisinsk/ast.pdf). What is the best way to fix this? I do not seem to have access to Joyal’s Lab to be able to edit that.
I had call to link to stable proposition, so I wrote it. It is possible that this should be combined with regular element.
started a bare minimum at modus ponens, as this came up in another thread.
So as to get rid of a grey unattached link, I created a stub for finitely presented group.
In looking at pro-categories and prohomotopy, I find statements in the literature to the effect that every constant pro-object is cosmall, and then (Christensen and Isaksen):Every object of every pro-category is κ-cosmall relative to all pro-maps for some κ. The proof that they give seems to me a bit like reinventing the wheel. Isn’t this something like the dual of the arguments used in looking at locally FP categories and Gabriel-Ulmer duality? Their result is used in a lot of the papers on pro-homotopy theories as then these are (very nearly) fibrantly generated.
I need this for my monograph on profinite homotopy, but we have nothing on cosmall objects and the consequences of the cosmall object argument in the nLab, and intend putting a version of it there afterwards.
Does anyone have thoughts on how to present this in the Lab. (I will have to give more (tedious) detail in the monograph as I do not have LFP categories explained anyway.) I also feel that some of the gory detail given more or less categorical folklore, but have not been able to track down enough to be able to pin that down. (It is almost in SGA4 which is online.) I am hindered by not having access to a library as I work from home. (Oh for universal open access!!!!!)
started a bare minimum at Bloch region
New entry special function, extensions to hypergeometric function, Selberg integral. New entries gamma function, recently also Euler beta function.
Stub for elementary function.
brief entry on the idea of world sheets for world sheets.
In the course of creating this I also started a stub for 2d quantum gravity, but clearly more needs to go there.
I was looking at simnplicial topological group and found mention of -cofibration. This is not provided with a link, and a search for the term did not find anything. What is one of these and where is that explained? (It occured to me that it related to the Strom model category structure on , but I could not find it on the relevant page.)
created some minimum at proof net (long requested by string diagram)
There was some confusion on the separator page in the section on strengthened sorts of separator. I’ve attempted to sort it out.
brief entry for amplimorphism
Bas Spitters had mentioned the following article on the HoTT list. While I suppose the conclusion has to be taken with several grains of salt, I found this discussion interesting and illuminating, and have added it now to the references at foundations of mathematics:
Freek Wiedijk, Is ZF a hack? Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics (pdf)
Abstract This paper presents Automath encodings (which also are valid in LF/P) of various kinds of foundations of mathematics. Then it compares these encodings according to their size, to find out which foundation is the simplest.
The systems analyzed in this way are two kinds of set theory (ZFC and NF), two systems based on Church’s higher order logic (Isabelle/Pure and HOL), three kinds of type theory (the calculus of constructions, Luo’s extended calculus of constructions, and Martin-Löf predicative type theory) and one foundation based on category theory. The conclusions of this paper are that the simplest system is type theory (the calculus of constructions) but that type theories that know about serious mathematics are not simple at all. Set theory is one of the simpler systems too. Higher order logic is the simplest if one looks at the number of concepts (twenty-five) needed to explain the system. On the other side of the scale, category theory is relatively complex, as is Martin-Löf’s type theory.
Is this here an accurate description of what is meant by the words “computational type theory”:
The term computational type theory is often used generally for intuitionistic type theory, referring to its computational content in view of the propositions-as-types and proofs-as-programs interpretation (e.g. Scholarpedia). More specifically it is used for type theory with inductive types and even more specifically (Fairtlough-Mendler 02) for modal type theory, hence for type theory equipped with a monad (in computer science) which exhibits a kind of computation.
?
While writing this reply on Physics.SE I thought to myself that it is curious that this tight relation between the topics in the title here is rarely made explict in introductions.
Then next occurred to me the observation that, unfortunately, not even the Lab did seem to say this. So therefore I have now briefly copied my reply there also to S-matrix – Formalization and to FQFT – Idea – General.
This deserves to be expanded on much further, of course, but at least it’s a start now.
entry for Bub-Clifton theorem with a rough idea section and some references
gave virtual fundamental class an Idea-section (feel free to improve) and added a bunch of pointers to the literature in the References-section
stub for integral transform (also a highly stubby stub for Fourier-Mukai transform)
started stub entry sheaf of L-infinity algebras, but it is still lacking some evident references
Originally I was going to add a comment on how to axiomatize in differential cohesion a sheaf of -algebras over as a pointed object in which is sent by the reduction modality to an identity. But maybe I’ll better do this tomorrow, when I am more awake (or else whenever that happens again).
I have started an entry on rewriting. It is just a stub for the moment.
Added to natural number a discussion about the fact that constructively, the natural numbers may fail to be (order) complete, as highlighted by Andrej Bauer in a very nice blog post. I quite like this example, because by interpreting a related lemma in the internal language of a certain sheaf topos one obtains a well-known proposition in algebraic geometry almost for free (see entry); but please let me know if stuff like this is too localized for the nLab.
created focal point
I typed at local topos in the section Local over-toposes statement and poof that sufficient for a slice topos to be local is that is tiny .
What are necessary conditions? Is this already necessary?
I added a few words to several complex variables, even though I am out of my depth here. If we have analysts popping by here, hopefully they will get an urge to add more.
stub for Anaxagoras’s Nous.