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

#### Related Tags

homotopy-theory × 2409at.algebraic-topology × 1462

ct.category-theory × 398

model-categories × 277

simplicial-stuff × 236

stable-homotopy × 188

higher-category-theory × 178

reference-request × 175

ag.algebraic-geometry × 158

homological-algebra × 137

gn.general-topology × 111

infinity-categories × 110

gt.geometric-topology × 107

cohomology × 97

operads × 72

kt.k-theory-and-homology × 70

loop-spaces × 51

differential-topology × 49

dg.differential-geometry × 48

lie-groups × 41

higher-algebra × 41

equivariant-homotopy × 41

classifying-spaces × 40

spectral-sequences × 39

fibration × 38