May 21, 2012
Superextensive Sites
Posted by Mike Shulman
When I first learned about sheaves and (1-)topos theory, I was taught that the most natural and general domain for sheaves is a site, i.e. a category equipped with a Grothendieck topology. This structure is a collection of covering families satisfying certain closure conditions.
However, as I progressed in sheaf theory, I found that often, people working with sheaves in some concrete way often consider only single covers . For instance, I’ve read one book in which sheaves on topological spaces were defined only in terms of gluing along single surjective local homeomorphisms. This sort of restriction is particularly pronounced among people who study internal categories in a topos: frequently an internal category is defined to be a stack just when it satisfies descent for single epimorphisms, and similarly internal anafunctors are defined using only single covers.
I have always found this strangely dissonant. Surely we care about the non-singleton covering families in all of these cases as well? So why are we justified in ignoring them?
Sometimes one finds a justifying comment along the lines of “any covering family can be replaced by the single cover ”. In this post I’d like to talk about (1) a nice general context in which we can do this, (2) what exactly it lets us do, and (3) what it doesn’t let us do.
May 18, 2012
Segal-Completeness and Univalence
Posted by Urs Schreiber
Here is a charming statement:
- Univalence in homotopy type theory is a special case of the Segal-completeness condition in internal (∞,1)-category theory .
Do you see it? Once you know what these terms mean this is pretty obvious, once stated. But it seems not to have been stated before.
I now briefly spell this out and give further pointers. This might be the beginning of a nice story. I am posting this here in the hope of discussing it a bit more.
Consider some ambient (∞,1)-topos and inside it an internal (∞,1)-category, hence a complete Segal space object . Its 1-skeleton, on which I will focus attention here, looks as follows (in this and the following formulas I display on the left the syntax and on the right its semantics, see HoTT methods for homotopy theorists if you are a homotopy theorist and need more background):
the object of morphisms sits by the source-and-target map over the object of objects
and the identity-assigning map is a diagonal section
Syntactically, the recursion principle / simple elimination rule for the inductive identity types, and semantically the (acyclic cofibrations fibrations)-weak factorization system, says that this section factors through the identity type (syntactically) respectively the path space object (semantically):
Now, Segal-completeness of is the statement that this exhibits the inclusion of the core, hence of those morphisms that are equivalences under the composition operation of .
Specifically, consider the case that is the universal small internal category object, equivalently the small reflection of the ambient -topos into itself, equivalently the classfier of the small codomain fibration, equivalently its stack semantics, or whatever you want to call it, that whose 1-skeleton is
where “” denotes the small universe / small object classifier.
Then the Segal-completeness condition of this internal category object is the univalence condition on .
May 17, 2012
Integrating Against the Euler Characteristic
Posted by Tom Leinster
The Euler characteristic of topological spaces behaves something like a measure. For example, under suitable hypotheses,
One of the main things you can do with a measure is integrate with respect to it — or ‘against’ it, as they say.
So: what happens if you try to integrate against the Euler characteristic?
I don’t completely understand the answer myself, but I’ll explain as well as I can. Along the way, we’ll see:
- how this train of thought helps us to define Euler characteristic
- how it also leads to the notion of curvature.
May 14, 2012
Postulated Colimits and Absolute Colimits
Posted by Mike Shulman
So there’s this thing invented by Anders Kock called a postulated colimit. It seems like I’ve read his note about them numerous times without really understanding it. I felt like there ought to be some relationship with my theory of exact completions, but I didn’t nail it down precisely in time for the posting of that preprint.
Now, however, I think I finally have a grasp on postulated colimits. They do turn out to be nicely related to exact completions, but to find out how, you’ll have to wait for me to update the exact completions paper (or figure it out yourself). Today, I just want to tell you what postulated colimits are, and talk about how they’re related to something else I like: absolute colimits.
May 10, 2012
What is Homotopy Type Theory Good For?
Posted by Urs Schreiber
The current situation of homotopy type theory reminds me a bit of the dot-com bubble at the turn of the millenium.
Back then a technology had appeared which was as powerful as it was new: while everybody had a sure feeling that the technology would have dramatically valuable impact, because it was so new nobody had an actual idea of what that would be. As opposed to other bubbles, that one did not burst because overly optimistic hopes had been unjustifed as such, but because it took a while to understand just how these hopes would be materialized in detail (for instance that today I would send a message as this here from a café via my webbook from my dropbox account).
With homotopy type theory the situation currently seems to be similar to me. On the one hand it is clear that some dramatic breakthrough right at the heart of mathematics has occured. One hears the sound of something big happening. But: what is the impact? It feels like after 1995 – when it was clear that the internet is going to be something big – but still before, say, 2003, when we started getting a good idea of how it changes our lives.
How will homotopy type theory change our lives?
Currently most research in homotopy type theory revolves around the fine-tuning of the formulation itself and completing the understanding of its relation to traditional homotopy theory. That’s necessary and good. (It’s great, I am enthusiastic about it!) But if the excitement about HoTT is not to be an illusion, then something will follow after that. The traditional homotopy theorist currently may complain (and some do) that much of what is happening is that facts already known are being re-formulated in a new language, not always yet to an effect a homotopy theorist would find noteworthy.
So I am wondering: how will the traditional homotopy theorist eventually benefit from homotopy type theory? How the researcher who uses homotopy theory for something else?
I am asking for personal reasons, too. Since, somewhat inadvertently, I have been investing some of my time into learning about it, I am naturally wondering: how will that time investment pay off for me? What does homotopy type theory do for my research?
I am not sure yet. But I have some first ideas. One of these I want to share here.
An example
My research, you may have noticed, is motivated from understanding basic structural phenomena in theoretical physics as incarnations of natural mathematical structures. What I will try to indicate in the following is a certain kind of problem that poses itself in the context of string theory, which – I think it is fair to say – was generally regarded to be among the more subtle problems in a field rich in subtle mathematical effects, and how it finds an elegant and simple solution once you regard it from the perspective of homotopy type theory.
What I say in the following I have said in different words before, together with my coauthors Domenico Fiorenza and Hisham Sati: in section 2 of an article titled The E8-moduli 3-stack of the C-field in M-theory. There we point out that the solution which we propose and study in the article, to some problem in string theory, can naturally be understood simply by reformulating a well-known equation – known as the flux quantization condition – first as a fiber product of sets of certain field configurations and then refining that to a homotopy fiber product of moduli ∞-stacks of certain field configurations.
Here I will just observe that if you come to this from homotopy type theory, then the solution looks even more elegant than this: one arrives there simply by taking verbatim the symbols denoting the solution set to the equation, but now interpreting these not in the ordinary logic of sets, but in the homotopy logic of homotopy types. It is then homotopy type theory which automatically produces the correct answer, the “-moduli 3-stack of the supergravity C-field in M-theory”. A solution that looks subtle to the eye of classical logic becomes self-evident from the point of view of homotopy logic / homotopy type theory.
From these remarks everybody with just basic training in category theory and homotopy theory can already deduce what I will say below. And what I say next is not hard to see, once you see it. It is one of those cases where a simple change of perspective leads with great ease to a solution of what seemed to be a difficult technical problem. Nevertheless, or because of this, I thought I’d say this explicitly.
May 7, 2012
The Mysterious Nature of Right Properness
Posted by Mike Shulman
I’ve been spending too much time recently thinking about (among other things) right properness of model categories. The ultimate goal is to build models of homotopy type theory in -toposes, but at the moment (in this post) I’m just trying to get a handle on about what right properness means, at an intuitive level. So this is going to be kind of rambly and philosophical and lacking in conclusions.
The issue of right properness is an aspect of a more general question: how do properties of a model category — call it , say — reflect properties of the -category that it presents — call it ? I’ve started thinking of this as a sort of coherence problem: if we view a model category as a certain sort of “strictification” of an -category, then asking “which -categories can be presented by a model category with such-and-such property?” is the same sort of question as “can every tricategory be presented by a strict 3-category?” In classical coherence theory, we know that sometimes we can make some aspects of a structure strict at the expense of others, e.g. we can make the units in a tricategory strict, or the interchange law, but not both at once. As we’ll see, model categories display similar phenomena.
May 5, 2012
Twisted Higher Bundles in Münster
Posted by Urs Schreiber
Right now I am at the 17th NRW Topology Meeting. In a few minutes I will talk about Principal ∞-Bundles – Theory and Applications.
By coincidence it turns out that the previous speaker, Ulrich Pennig discussed, in a nice talk, such an application: twisted 2-vector bundles.
This is joint work of him and Brano Jurčo. They consider BDR 2-vector bundles which, by definition, are the objects classified by, roughly, the monoidal delooping of the monoidal category . Their starting point to consider twists of these structures is the discussion in Thomas Kragh’s Orientations and Connective Structures on 2-vector Bundles, who constructs, for each , a fiber sequence
and interprets the space on the left as that classifying “oriented BDR 2-vector bundles”, in higher analogy of orientation of vector bundle. Accordingly, the map induces a notion of twisted (twisted oriented) 2-vector bundles, with twist a class in , hence with twisting -bundles specific -principal 3-bundles (aka bundle 2-gerbes).
This is similar to the twisted String 2-bundles which are twisted by the fractional Pontryagin class in .
Have to run now. More details later.
May 4, 2012
Quivering with Excitement
Posted by John Baez
Over on Google+, David Roberts just told me the most exciting theorem I’ve heard all week. Every projective variety is the Grassmannian of a quiver representation! I suppose it’s just another indication of the ‘wildness’ of quiver representations once we leave the safe waters of Gabriel’s theorem.
Let me explain….