Start a new discussion

Not signed in

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

Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

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

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

• 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$?

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

• I had set out to add to the entry equivalence in homotopy type theory a detailed derivation of the categorical semantics of $Equiv(X,Y)$. But then I ended up getting distracted by various editorial work in other entries and for the moment I only have this puny remark added, expanding on the previous discussion there.

Maybe more later…

• I have started creating a hyperlinked index at

A colleague may use this for a course and maybe we get a chance to polish and/or write up some more related material in relevant $n$Lab entries.

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

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

• I finally started linear equation. But am too tired now to really do it justice…

• 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?)

• I have touched quasi-isomorphism, expanded the Idea-section and polished the Definition-section, added References

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

• 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 have

• split off a new entry sequent

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

• 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

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

• I have created an entry type of types. Wanted to collect some literature there, but ended up not finding too much…

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

• at implication there is currently the statement

$q \to r \vdash (p \to q) \to (q \to r)$,

That’s a typo, right?

• 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 four lemma (should still state the dual version, will do so later)

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

• I took simple function out of measure space, putting there abstract definitions up through the integral on $L^1$.

• 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 $n$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:

universe - contents

• 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?

• I have touched the formatting at direct sum and then expanded a little:

1. Added a paragraph to the Idea-section such that something familiar is mentioned right at the beginning;

2. Expanded on the example of direct sums in $Ab$ by drawing the cocone diagrams and explicitly mentioning the universal property.

3. Mentioned the relation to formal linear combinations.

4. Mentioned the examples of direct sums of modules.

• 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 “$L$-structure on a set”). The new version aims to reflect this properly.)