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.
The page on inductive-inductive types refers to dialgebras without specifying them. Having a short page as some sort of reference is helpful.
I felt there should be an entry category of presheaves. So I started one.
a bare minimum, for the time being in order to record the main result of:
I gave the scan that Colin MacLarty just shared on the mailing list a home on the nLab:
Saunders MacLane,
Bowdoin Summer School 1969
Notes taken by Ellis Cooper (pdf)
Presently the pdf-link points to my Dropbox folder, as I keep forgetting the system password necessary to upload a file of this size to the nLab server. Maybe Mike or Adeel have the energy to upload it.
After a suggestion from Toby, I added a note on the “analytic Markov’s principle” to Markov’s principle.
gave representation theory a little Idea-section, then added some words on its incarnation as homotopy type theory in context/in the slice over BG and added the following homotopy type representation theory – table, which I am also including in other relevant entries:
| homotopy type theory | representation theory |
|---|---|
| pointed connected context BG | ∞-group G |
| dependent type | ∞-action/∞-representation |
| dependent sum along BG→* | coinvariants/homotopy quotient |
| context extension along BG→* | trivial representation |
| dependent product along BG→* | homotopy invariants/∞-group cohomology |
| dependent sum along BG→BH | induced representation |
| context extension along BG→BH | |
| dependent product along BG→BH | coinduced representation |
tried to bring the entry Lie group a bit into shape: added plenty of sections and cross links to other nLab material. But there is still much that deserves to be done.
I have given necessity and possibility (which used to redirect to S4-modal logc) an entry of their own.
The entry presently
first recalls the usual axioms;
then complains that these are arguably necessary but not sufficient to characterize the idea of necessity/possibility;
and then points out that if one passes from propositional logic to first-order logic (hyperdoctrines) and/or to dependent type theory, then there is a way to axiomatize modalities that actually have the correct interpretation, namely by forming the reflection (co)monads of ∃ and ∀, respectively.
You may possibly complain, but not necessarily. Give it a thought. I was upset about the state of affairs of the insufficient axiomatics considered in modal logic for a long time, and this is my attempt to make my peace with it.
Required at projective plane.
brief category:people-entry for hyperlinking references at exceptional generalized geometry
brought in the diagrammatics and the identification with natural transformations.
(this on my way to creating a new entry “twisted intertwiner”)
New page, cross ratio.
stub, to make links at Bertrand’s postulate work
I have expanded a bit the previous stub entry Goerss-Hopkins-Miller theorem. It’s still stubby, but less so.
I have added
more of the pertinent references;
an actual Idea-section
the statement of the Hopkins-Miller theorem in the version as it appears in Charles Rezk’s notes.
Maybe this feeble step forward inspires Aaron to add more… :-)
quick note at spin structure on the characterization over Kähler manifolds
I made a start on regular representation (via a stub from normalizer). My first thought was to made this a generic regular representation page so I put in definitions for groups and algebras.
Once I’d created the page I thought that it could be said to be an example of a more general thing whereby a monoid acts on itself. However, someone’s already editing the page (that was fast!) so I’ll have to wait to put that in.
(Unless the anonymous coward reads this and decides to put it in themselves!)
stub for 2-topos (mostly so that the links we have to it do point somewhere at least a little bit useful)
while adding to representable functor a pointer to representable morphism of stacks I noticed a leftover discussion box that had still be sitting there. So hereby I am moving that from there to here:
[ begin forwarded discussion ]
+–{+ .query} I am pretty unhappy that all entries related to limits, colimits and representable things at nlab say that the limit, colimit and representing functors are what normally in strict treatment are just the vertices of the corresponding universal construction. A representable functor is not a functor which is naturally isomorphic to Hom(-,c) but a pair of an object and such isomorphism! Similarly limit is the synonym for limiting cone (= universal cone), not just its vertex. Because if it were most of usages and theorems would not be true. For example, the notion and usage of creating limits under a functor, includes the words about the behaviour of the arrow under the functor, not only of the vertex. Definitions should be the collections of the data and one has to distinguish if the existence is really existence or in fact a part of the structure.–Zoran
Mike: I disagree (partly). First of all, a functor F equipped with an isomorphism F≅homC(−,c) is not a representable functor, it is a represented functor, or a functor equipped with a representation. A representable functor is one that is “able” to be represented, or admits a representation.
Second, the page limit says “a limit of a diagram F:D→C … is an object limF of C equipped with morphisms to the objects F(d) for all d∈D…” (emphasis added). It doesn’t say “such that there exist” morphisms. (Prior to today, it defined a limit to be a universal cone.) It is true that one frequently speaks of “the limit” as being the vertex, but this is an abuse of language no worse than other abuses that are common and convenient throughout mathematics (e.g. “let G be a group” rather than “let (G,⋅,e) be a group”). If there are any definitions you find that are wrong (e.g. that say “such that there exists” rather than “equipped with”), please correct them! (Thanks to your post, I just discovered that Kan extension was wrong, and corrected it.)
Zoran Skoda I fully agree, Mike that “equipped with” is just a synonym of a “pair”. But look at entry for limit for example, and it is clear there that the limiting cone/universal cone and limit are clearly distinguished there and the term limit is used just for the vertex there. Unlike for limits where up to economy nobody doubt that it is a pair, you are right that many including the very MacLane representable take as existence, but then they really use term “representation” for the whole pair. Practical mathematicians are either sloppy in writing or really mean a pair for representable. Australians and MacLane use indeed word representation for the whole thing, but practical mathematicians (example: algebraic geometers) are not even aware of term “representation” in that sense, and I would side with them. Let us leave as it is for representable, but I do not believe I will ever use term “representation” in such a sense. For limit, colimit let us talk about pairs: I am perfectly happy with word “equipped” as you suggest.
Mike: I’m not sure what your point is about limits. The definition at the beginning very clearly uses the words “equipped with.” Later on in the page, the word “limit” is used to refer to the vertex, but this is just the common abuse of language.
Regarding representable functors, since representations are unique up to unique isomorphism when they exist, it really doesn’t matter whether “representable functor” means “functor such that there exists an isomorphism F≅homC(−,c)” or “functor equipped with an isomorphism F≅homC(−,c).” (As long as it doesn’t mean something stupid like “functor equipped with an object c such that there exists an isomorphism F≅homC(−,c).”) In the language of stuff, structure, property, we can say that the Yoneda embedding is fully faithful, so that “being representable” is really a property, rather than structure, on a functor.
[ continued in next comment ]
I added to category of elements an argument for why El preserves colimits.
Explained at mapping cone how the mapping cone is model for a homotopy cofiber. In fact I used that to define and motivate the mapping cone.
Then I moved the example in Top to the top of the list, as that is the archetypical example.
I have expanded Green-Schwarz mechanism a fair bit
Created:
A subcategory C of an accessible category D is accessible if C is an accessible category and the inclusion functor C→D is an accessible functor.
Some authors, e.g., Lurie in Higher Topos Theory and Adámek–Rosický, require accessible subcategories to be full subcategory.
Some authors, e.g., Adámek–Rosický in Locally Presentable and Accessible Categories merely require C to be accessible, referring to the stronger notion as an accessibly embedded accessible subcategory.
Accessible subcategories are idempotent complete and are closed under set-indexed intersections.
See, for example, Definition 5.4.7.8 in
Fixed a hyperlink to Jardine’s lectures. Removed a query box:
+– {: .query} Can any of you size-issue experts help to clarify this?
Mike: I wish. I added some stuff, but I still don’t really understand this business. In particular I don’t really know what is meant by “inessential.” It certainly seems unlikely that you would get equivalent homotopy theories, but it does seem likely that you would get similar behavior no matter where you draw the line. And if all you care about is, say, having a good category of sheaves in which you can embed any particular space or manifold you happen to care about, then that may be good enough. But I don’t really know what the goal is of considering such large sites. =–
in reply to discussion on the blog I
added more details to Lie algebroid
added a reference by Courant to Lie algebroid, Poisson Lie algebroid and tangent Lie algebroid
created Legendre transformation as a placeholder that currently just serves to keep some references on Legendre transformation from the point of view of Lie algebroid theory.
Added:
A bijective correspondence between Lie algebroid structures, homological vector fields of degree 1, and odd linear Poisson structures is established in the paper
I started a page logicality and invariance. In Bristol the other day, Steve Awodey was promoting the thought that HoTT is a realisation of that thrust to understand logic as maximally invariant.
What would it be to take that seriously? If invariants are picked up by dependent product in some BAut context, could there be a useful context BAut(𝒰) for the universe 𝒰?
felt like the nLab should have an entry fraction
I created an entry on Larry Lambe. I included a link to some (on line) notes of his on Symbolic Computation which includes discussion of the perturbation lemma from homological perturbation theory.
Unfortunately, there are two entries on the same topic, both created by Urs: quantum Hall effect (redirecting also fractional quantum Hall effect what should eventually split off) with some substance, and the microstub quantum hall effect. I would like to create quantum spin Hall effect and I think I should rename/reclaim the stub quantum hall effect for this. Do others agree ? Urs ?
As the action is now delayed I record here the reference which I wanted to put there
Somewhat surprisingly, the authors and roughly this work of them are mentioned (though not in the list of references) in a paper in algebraic geometry
which considers the mirror symmetry and topological states of matters (topological insulators in particular) as main applications.
am starting curvature characteristic form and Chern-Simons form.
But still working…
started some bare minimum at Spin Chern-Simons theory
pointer, concerning the so-called “negative branes” of e.g. DHJV ’18
I was involved in some discussion about where the word “intensional” as in “intensional equality” comes from and how it really differs from “intenTional” and what the point is of having such a trap of terms.
Somebody dug out Martin-Löf’s lecture notes “Intuitionistic type theory” from 1980 to check. Having it in front of me and so before I forget, I have now briefly made a note on some aspects at equality in the section Different kinds of equalits (below the first paragraph which was there before I arrived.)
Anyway, on p. 31 Martin-Löf has
intensional (sameness of meaning)
I have to say that the difference between “sameness of meaning” and “sameness of intenTion”, if that really is the difference one wants to make, is at best subtle.
added pointer to section 7.5 of