skip to main content
US FlagAn official website of the United States government
dot gov icon
Official websites use .gov
A .gov website belongs to an official government organization in the United States.
https lock icon
Secure .gov websites use HTTPS
A lock ( lock ) or https:// means you've safely connected to the .gov website. Share sensitive information only on official, secure websites.


Title: On the ∞$\infty$‐topos semantics of homotopy type theory
Abstract Many introductions tohomotopy type theoryand theunivalence axiomgloss over the semantics of this new formal system in traditional set‐based foundations. This expository article, written as lecture notes to accompany a three‐part mini course delivered at the Logic and Higher Structures workshop at CIRM‐Luminy, attempt to survey the state of the art, first presenting Voevodsky's simplicial model of univalent foundations and then touring Shulman's vast generalization, which provides an interpretation of homotopy type theory with strict univalent universes in any ‐topos. As we will explain, this achievement was the product of a community effort to abstract and streamline the original arguments as well as develop new lines of reasoning.  more » « less
Award ID(s):
2204304
PAR ID:
10534820
Author(s) / Creator(s):
 
Publisher / Repository:
Oxford University Press (OUP)
Date Published:
Journal Name:
Bulletin of the London Mathematical Society
Volume:
56
Issue:
2
ISSN:
0024-6093
Format(s):
Medium: X Size: p. 461-517
Size(s):
p. 461-517
Sponsoring Org:
National Science Foundation
More Like this
  1. PurposeThe paper aims to determine the rational homotopy type of the total space of projectivized bundles over complex projective spaces using Sullivan minimal models, providing insights into the algebraic structure of these spaces. Design/methodology/approachThe paper utilises techniques from Sullivan’s theory of minimal models to analyse the differential graded algebraic structure of projectivized bundles. It employs algebraic methods to compute the Sullivan minimal model of P ( E ) and establish relationships with the base space. FindingsThe paper determines the rational homotopy type of projectivized bundles over complex projective spaces. Of great interest is how the Chern classes of the fibre space and base space, play a critical role in determining the Sullivan model ofP(E). We also provide the homogeneous space ofP(E)whenn = 2. Finally, we prove the formality ofP(E)over a homogeneous space of equal rank. Research limitations/implicationsLimitations may include the complexity of computing minimal models for higher-dimensional bundles. Practical implicationsUnderstanding the rational homotopy type of projectivized bundles facilitates computations in algebraic topology and differential geometry, potentially aiding in applications such as topological data analysis and geometric modelling. Social implicationsWhile the direct social impact may be indirect, advancements in algebraic topology contribute to broader mathematical knowledge, which can underpin developments in science, engineering, and technology with societal benefits. Originality/valueThe paper’s originality lies in its application of Sullivan minimal models to determine the rational homotopy type of projectivized bundles over complex projective spaces, offering valuable insights into the algebraic structure of these spaces and their associated complex vector bundles. 
    more » « less
  2. Let p∈Z be an odd prime. We prove a spectral version of Tate–Poitou duality for the algebraic K-theory spectra of number rings with p inverted. This identifies the homotopy type of the fiber of the cyclotomic trace K(OF)∧p→TC(OF)∧p after taking a suitably connective cover. As an application, we identify the homotopy type at odd primes of the homotopy fiber of the cyclotomic trace for the sphere spectrum in terms of the algebraic K-theory of Z. 
    more » « less
  3. Abstract Working at the prime 2 and chromatic height 2, we construct a finite resolution of the homotopy fixed points of MoravaE-theory with respect to the subgroup$$\mathbb {G}_2^1$$ G 2 1 of the Morava stabilizer group. This is an upgrade of the finite resolution of the homotopy fixed points ofE-theory with respect to the subgroup$$\mathbb {S}_2^1$$ S 2 1 constructed in work of Goerss–Henn–Mahowald–Rezk, Beaudry and Bobkova–Goerss. 
    more » « less
  4. Abstract Cut-and-paste $$K$$-theory has recently emerged as an important variant of higher algebraic $$K$$-theory. However, many of the powerful tools used to study classical higher algebraic $$K$$-theory do not yet have analogues in the cut-and-paste setting. In particular, there does not yet exist a sensible notion of the Dennis trace for cut-and-paste $$K$$-theory. In this paper we address the particular case of the $$K$$-theory of polyhedra, also called scissors congruence $$K$$-theory. We introduce an explicit, computable trace map from the higher scissors congruence groups to group homology, and use this trace to prove the existence of some nonzero classes in the higher scissors congruence groups. We also show that the $$K$$-theory of polyhedra is a homotopy orbit spectrum. This fits into Thomason’s general framework of $$K$$-theory commuting with homotopy colimits, but we give a self-contained proof. We then use this result to re-interpret the trace map as a partial inverse to the map that commutes homotopy orbits with algebraic $$K$$-theory. 
    more » « less
  5. Abstract This is the second installment in a series of papers applying descriptive set theoretic techniques to both analyze and enrich classical functors from homological algebra and algebraic topology. In it, we show that the Čech cohomology functorson the category of locally compact separable metric spaces each factor into (i) what we term theirdefinable version, a functortaking values in the category$$\mathsf {GPC}$$ofgroups with a Polish cover(a category first introduced in this work’s predecessor), followed by (ii) a forgetful functor from$$\mathsf {GPC}$$to the category of groups. These definable cohomology functors powerfully refine their classical counterparts: we show that they are complete invariants, for example, of the homotopy types of mapping telescopes ofd-spheres ord-tori for any$$d\geq 1$$, and, in contrast, that there exist uncountable families of pairwise homotopy inequivalent mapping telescopes of either sort on which the classical cohomology functors are constant. We then apply the functorsto show that a seminal problem in the development of algebraic topology – namely, Borsuk and Eilenberg’s 1936 problem of classifying, up to homotopy, the maps from a solenoid complement$$S^3\backslash \Sigma $$to the$$2$$-sphere – is essentially hyperfinite but not smooth. Fundamental to our analysis is the fact that the Čech cohomology functorsadmit two main formulations: a more combinatorial one and a more homotopical formulation as the group$$[X,P]$$of homotopy classes of maps fromXto a polyhedral$$K(G,n)$$spaceP. We describe the Borel-definable content of each of these formulations and prove a definable version of Huber’s theorem reconciling the two. In the course of this work, we record definable versions of Urysohn’s Lemma and the simplicial approximation and homotopy extension theorems, along with a definable Milnor-type short exact sequence decomposition of the space$$\mathrm {Map}(X,P)$$in terms of its subset ofphantom maps; relatedly, we provide a topological characterization of this set for any locally compact Polish spaceXand polyhedronP. In aggregate, this work may be more broadly construed as laying foundations for the descriptive set theoretic study of the homotopy relation on such spaces$$\mathrm {Map}(X,P)$$, a relation which, together with the more combinatorial incarnation of, embodies a substantial variety of classification problems arising throughout mathematics. We show, in particular, that ifPis a polyhedralH-group, then this relation is both Borel and idealistic. In consequence,$$[X,P]$$falls in the category ofdefinable groups, an extension of the category$$\mathsf {GPC}$$introduced herein for its regularity properties, which facilitate several of the aforementioned computations. 
    more » « less