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 looping combinator.
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.
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.
I am starting salamander lemma
I hope to be adding bits and pieces to an article real coalgebra, which I’ve started. (In some sense it might fit better on my web, but for some reason I’m placing it on the main nLab.)
I ended up spending some time with expanding extension of scalars. Towards the end I had more plans, but I’ll stop now, need to do something else.
created index of a subgroup
created four lemma (should still state the dual version, will do so later)
and now I even ended up creating a new floating table of contents: equality and equivalence - contents
(all I wanted to originally was to create an elementary entry linear equation…)
I really just wanted to start an entry linear equation but I ended up putting some content into equation.
I have added some links to preprint on the entry Lascar group. I do not understand the model theory, but its link with Galois theory may be of use to someone looking at model theory and type theory elsewhere on the Lab, so I hope it is useful.
I see we have internal set, while I was just about to make that term redirect to Bishop set.
That would have read more systematically in the list at internal infinity-categories contents .
I keep feeling the need to point to an entry named formal logic. None of the existing entries seems to quite deserve to be where this link should be redirecting to. So I created a page formal logic with just some pointers to pages that the reader might expect behind this term.
Just so that I can use that link for the time being.
have split off Hamiltonian form from n-plectic geometry (because I needed to be able to point to it)
I took simple function out of measure space, putting there abstract definitions up through the integral on .
creatd connecting homomorphism with (just) the pedestrian description.
(Relation to snake lemma and more generally to fiber sequences not there yet…)
As I said in another thread, I would like to see the Lab entries related to universes be somehow better, more organized, more comprehensive.
In order to get a handle on it I decided, as so often, to tabulate what we have and what we should have, so I am creating:
and will include it as a “floating table of contents” into the relevant entries
at inductive reasoning it says
Induction here is not to be confused with mathematical induction.
We should point out that, however, there is a close relation:
one can see this still in the German tem for, “induction over the natural numbers” which is not Induktion, but vollständige Induktion: meaning ” complete induction” !
I guess the reasoning is clear, mathematical induction (at least that over the natural numbers) is a special case of inductive reasoning, namely that where we can be sure that we are inducing from a complete set of instances of the general rule.
Does anyone feel like touching the entry accordingly to clarify this?
created Mod
created quotient module
created submodule
turns out plenty of entries were asking for quotient group. I created something. But am running a bit out of steam for tonight.
I have touched cokernel, briefly adding some basics. More needs to be done here.
After discussion here I have changed the organization of the entry structure and then expanded a bit by adding an Idea-section and a bit more here and there.
(The previous organization of the entry instead made it look like structure in model theory is a concept on par with that discussed at stuff, structure, property. But instead, the latter axiomatizes the general notion of “structure on something” as such, whereas the former is an example of a structure on something (namely an “-structure on a set”). The new version aims to reflect this properly.)
Using the LaTeX macro package TikZ, I’ve redrawn most of the SVGs on the knots and links pages. I hope that I haven’t trodden on any toes in so doing! I may have missed a few diagrams as well.
I’ve shifted the actual SVGs to pages of their own. This makes it easier to edit the pages with them on - TikZ’s SVG export isn’t as compact as the inbuilt SVG editor - and easier to include on other pages. For example, I can imagine that the trefoil knot is going to appear again and again!
(Incidentally, are the two trefoils distinct? If so, which have I drawn at trefoil knot - SVG).
I’ve named the pages with - SVG
in their name, though for the moment I’ve also put in redirects to the name without the SVG. When actually including the diagram, one should always use the canonical name (ie with the - SVG
) since it may be that we actually write a page about the trefoil knot one day. But I thought that for the moment, a nice aspect of hyperlinks is that if we mention the trefoil knot in a page then we can put in a link to an actual picture.
Diagrams done so far:
Pages with includes include: link, Reidemeister move, colorability, bridge number.
What would be fantastic here is if the “source” link took one to the actual LaTeX/TikZ source! I do intend to put that up on the nLab, but I need to clean it up a little as it depends on some customised style files that have a lot of crud in them.
I have been attacking some of the grey links in knot theory and the related pages. If someone has the time (and the patience) adding a few more links would be a good thing. I have added Crowell, Fox, Dehn, Alexander, Louis Kauffman, plus some non-people pages such as Alexander polynomial. That needs some diagrams if it is to do what it ’should’ and my svg skills are too slight to attempt that today. :-)
I added to the “abstract nonsense” section in free monoid a helpful general observation on how to construct free monoids. “Adjoint functor theorem” is overkill for free monoids over .
[ forwarding old discussion that used to be at context ]
The following discussion was initiated by a previous version of the above entry which referred to “cartesian multicategories” rather than finitely complete categories.
+–{: .query} Mike: What is a cartesian multicategory, and how do I interpret the theory of groups in one? I can guess what it would mean for a multicategory to have finite products. But if I interpret the multiplication as a morphism , then I’m not using the multicategory structure, so we might as well just be in a category with finite products. And if I interpret the multiplication as a multimap , then I don’t know how to interpret the axiom of inverses, since there is no ’diagonal’ or ’projection’ .
Toby: I'm not sure why I generalised to cartesian multicategories, but it is a nontrivial generalisation. (Perhaps I was planning to show, as an example, how the category of contexts of the canonical language of a multicategory becomes a monoidal category or something, but that doesn't seem very useful. Maybe I was just doing unnecessary generality, but of course it's not the absolutely most general situation either.)
Anyway … you make a multicategory cartesian much as you might make a monoidal category cartesian by equipping it with appropriate diagonal and projection maps. The problem is that, while and make sense in a monoidal category, they don't make sense in a multicategory. But you fix this by filtering through Yoneda.
So a cartesian multicategory is a multicategory equipped with, for each object and object , a function and a function . (H'm, my commas and semicolons are the opposite of yours; no matter.) Then these are subject to various coherence requirements that should be obvious.
Mike: Okay, I see. Though I’m guessing you wanted those natural transformations to go the other way. Are there any naturally occurring examples of cartesian multicategories that are not cartesian monoidal categories? Even if there are, I’m inclined to regard the concept as esoteric enough that it would be clearer to just say “category with finite products” in this introductory article.
Toby: Ah, the curse of contravariance! Going over the whole introduction again, I think that I understand why I mentioned multicategories, which is that a context like is more naturally interpreted as a list of objects than as a single object . But if we were really to go in that direction, then we'd also want the context to be interpreted as a list in its own right rather than an actual subobject of , and that's going a bit far … farther than I understand clearly, in any case. So in fact I let the category be finitely complete so that we could form that subobject (referred to only via the link to internal logic, of course).
Mike: True. Is a one-object cartesian multicategory the same as a Lawvere theory, aka an operad relative to the theory of categories with finite products? If so, then perhaps the relevant place to work is a multicategory relative to the theory of lex categories? Can that be generalized to stronger logics?
Toby: Yes, that seems to be right, that Lawvere theories are equivalent to one-object cartesian multicategories (cartesian multimonoids? cartesian operads?). So this should work.
Of course, one thing that contexts do is to form an honest category even if you start with a multicategory. So here we're trying to go backwards and see what bare-bones starting point could lead to the same category of contexts of the equational theory of a group. =–
I finally gave the poor entry physics a bit of text.
created internal sheaf
Mainly it was bugging me that I didn’t find a piece of literature that said it quite explicitly the way I do there, so I wanted to have that written down. To be expanded, eventually.
Made some changes at logic and started inductive inference and George Polya.
There are still things to change at logic
As a discipline, logic is the study of methods of reasoning. While in the past (and often today in philosophical circles), this discipline was prescriptive (describing how one should reason), it is increasingly (and usually in mathematical circles) descriptive (describing how one does reason).
Could whoever wrote it explain what they meant? Seems odd to me.
Also I don’t think that category-theoretic logic should be there. Should it not appear in mathematical logic, or be a new page?
Expanded second-countable space and started first-countable space.
Created arity class. Added links from a few places, but there are probably others I didn’t think of.
I fixed a strange link at John Power.
To Toby, mainly, of course also to anyone interested:
We have a page-“category” foundational axiom, but we have no entry of that name. We should start one! foundational axiom.
(We do have axiom of foundation. A bit of a different thing.)
I’ve been editing second order arithmetic (I usually write “second-order arithmetic”, with a hyphen). I would appreciate someone taking a look and making corrections if necessary. There are probably some hyperlinks which could be added.
Created κ-ary site.
I renamed familial regularity and exactness to k-ary exact category (with redirects from k-ary regular category), and updated some of the statements to match my exact completions paper a bit better.
I’m planning to create k-ary site as well, and add a statement of the main theorem of the paper somewhere on the nLab. But I’m undecided as to where that statement should go and how it should interact with the existing pages regular and exact completions and pretopos completion. Opinions are welcome.
expanded at Chan-Paton bundle the Idea-section and added two pointers to lecture notes. Also expanded at Freed-Witten anomaly a little.
I ended up polishing type theory - contents (which is included as a floating table of contents in the relevant entries):
expanded and re-arranged the list under “syntax”, created stubs for the missing items definition and program
expanded the (logic/type theory)-table to a (logic/category theory/type theory)-table and subsumed some of the items into it that were floating around elsewhere.
at axiom of choice into the section In dependent type theory I have moved the explicit statement taken from the entry of dependent type theory (see there for what I am talking about in the following).
One technical question: do we need the
: true
at the very end of the formal statement of the theorem?
One conceptual question: I feel inclined to add the following Remark to that, on how to think about the fact that the axiom of choice is always true in this sense in type theory. But please let me know what you think:
Heuristically, the reason that the axiom of choice is always true when formulated internally this way in dependent type theory is due to the fact that its assumption thereby is stated in constructive mathematics:
Stated in informal but internal logic, the axiom of choice says:
If is a map all whose fibers are inhabited, then there is a section.
But now if we interpret the assumption clause
a map all whose fibers are inhabited
constructively, we have to provide a constructive proof that indeed the fibers are inhabited. But such a constructive proof is a choice of section.
So constructively and internally the axiom is reduced to “If there is a section then there is a section.” And so indeed this is always true.
Would you agree that this captures the state of affairs?
stub for pseudocircle (a finite topological space)
split off total complex from double complex. Let the Definition-section stubby, as it was, but added a brief remark on exactness and on relation to total simplicial sets, under Dold-Kan and Eilenberg-Zilber. More to be done.
Stubs for structural rule, weakening rule, contraction rule, and exchange rule.
Speaking of philosophy, I added a little to dichotomy between nice objects and nice categories.
it seems that a few days back I had created a note truncation of a chain complex
I felt like having a simple stand-alone entry suspension of a chain complex, so I created one.
Dedekind completions of quasiorders (not just linear orders) may now be found at Dedekind completion. Example: the lower Dedekind completion of the quasiorder of continuous functions is the quasiorder of lower semicontinuous functions.
I put a bunch of stuff there that might be of interest to the logicians and foundationalists among us, although it’s still pretty trivial.
some trivial additions to chain map.
created an entry coefficient and linked it with
as well as with
at Mod I started a new subsection RMod is an abelian category, spelling out some of the details of this statement.