Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion 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 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-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 sheaves simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

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

Welcome to nForum
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).
    • Something odd has been happening at a new entry entitled exchange structure. Someone signing in as Carol entered in quite a lot of material relating to J. Ayoub, Les six opérations de Grothendieck et le formalisme des cycles évanescents dans le monde motivique. This has just been deleted from the same IP address. This probably means nothing important but it is worth noting.

    • 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

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

    • created metric jet after a mention at the Café.

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

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

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

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

      Type* \emptyset \to Type \to *

      and that is the codomain fibration

      H /TypeH \mathbf{H}_{/Type} \to \mathbf{H}

      with its strutcure as a pointed map remembered, since the point is

      *H /. * \simeq \mathbf{H}_{/\emptyset} \,.

      I don’t know yet if this is super-relevant for anything, but it seems non-irrlelevant enough not to preclude it from being speakable.

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

    • needed matter to point somewhere

    • 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 BPBP, E(n)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 Aut(X)\mathbf{Aut}(X) via \infty-image factorization of the name of XX?

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

    • 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 XEType\;\;\;\;X \stackrel{\vdash \;\;\;\;E}{\to} \;\;\Type Xt XE\;\;\;\;X \stackrel{\vdash \;\;\;t}{\to} {}_X \;\;E
      homotopy type theory x:XE(x):Typex : X \vdash E(x) : Type x:Xt(x):E(x)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

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

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

    • 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

      qr(pq)(qr) 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.