18

So the issue is with this: all of the groups occuring in the Goerss--Hopkins obstruction theory vanish In "generic terms", for the obstruction theory that you're running in either the $K(1)$-local case or the rational case you care about some bigraded obstruction groups $$ \mathfrak{E}xt^{s,t}(R;S) $$ where these are some nonabelian Ext-groups ...


11

There are many results that generalize the Riemann–Hilbert correspondence from the fundamental groupoid to the fundamental ∞-groupoid, for example: Jonathan Block, Aaron Smith. A Riemann–Hilbert correspondence for infinity local systems. Joseph Chuang, Julian Holstein, Andrey Lazarev. Maurer-Cartan moduli and theorems of Riemann-Hilbert type. Manuel ...


10

It is true, and follows from results of Browder on the mod 2 Bockstein spectral sequence for $K(\mathbb{Z}/2,4)$. (We can replace $4$ by any even integer $k$ and conclude that $\iota_k^2$ ia not the reduction of an integral class.) An argument is spelled out in Section 3 of Grant, Mark; Szűcs, András, On realizing homology classes by maps of restricted ...


8

Roughly speaking, a type theory is computationally adequate if there is an algorithm that evaluates a term belonging to any type into a "normal form" of that type. The simplest form of this is when dealing with closed terms (not involving any variables or hypotheses) belonging to a "base" type such as $\mathbb{N}$ or $\mathbf{2}$, in ...


8

The HoTT libraries in Lean can be considered dead. Since Lean has moved away from HoTT, I don't think it's a more convenient system to do HoTT in than - for example - Coq. There is still some formalization material in the Lean 2 library that hasn't been formalized in another proof assistant, but probably the best thing to do with that is to port it to other ...


5

Let P be a (nontrivial) principal bundle over the base space R^4 All principal bundles over R^4 are trivial because R^4 is contractible. Or at least can I assert that all such horizontal lifts end at the same point? No, because the curvature of the connection on P can be nonvanishing, in which case you can find two homotopic paths whose horizontal lifts ...


5

Let $S^n := \Delta^n/\partial \Delta^n$; and let me assume for simplicity that $X$ is connected. We have a (homotopy) fiber sequence $\Omega^n X \to X^{S^n} \to X$. In particular, for $n>k$, $\Omega^n X$ is contractible (it is a Kan complex and its homotopy groups are trivial by assumption), so that for $n>k$, $X^{S^n}\to X$ is a homotopy equivalence (...


4

For whatever it is worth, here is a link to a paper that you may find interesting. Nori diagrams and persistent homology (arXiv:1901.10301) by Yuri Manin and Matilde Marcolli


3

Let me first write what happens for classical cobordism. You are basically asking whether the map $\operatorname{MU}\to H\mathbb{Z}$ factors through the projection $\operatorname{ku}\to H\mathbb{Z}$. But this is clear, since all spectra in sight are connective and we have an equivalence $$\operatorname{Map}(E,H\mathbb{Z})\cong \operatorname{Map}(\pi_0E,\...


2

It is not the case: the terminal semi-simplicial set $1$ is obviously fibrant but as I will show below the geometric product $1 \otimes 1$ is not fibrant. 1) What does $1 \otimes 1$ look like ? So, $1 \otimes 1$ identifies with the subset of non-degenerate cells of $L(1 \otimes 1) = L 1 \times L 1$. In general $LX$ admits an explicit desciprion as: $$ (LX)_n ...


1

I think that the best answer so far comes from this paper: https://arxiv.org/abs/1811.07830 , where it is proved that homotopy categories of dg-categories and various flavours of A-infinity categories are equivalent.


Only top voted, non community-wiki answers of a minimum length are eligible