explicit computation

Stream: condensed mathematics

[Johan Commelin]

I want to compute very explicitly the dimensions of some homology groups associated with Breen--Deligne data. If you are a wizard with computations (on paper or on computer) please read on.

Cubes

Let $\square = \{0,1\}$ denote a set with two elements. Then we can consider $\square^n$ as a discrete cube. For every $n$ and every $0 \le i \le n$ and every $b \in \square$ we have natural maps $f^{n,i}_b \colon \square^n \to \square^{n+1}$ that maps $\square^n$ to the $(i,b)$-th face of $\square^{n+1}$. Concretely $(x_1, \dots, x_n)$ is mapped to $(x_1, \dots, x_{i-1}, b, x_i, \dots, x_n)$.

If we have some set $A$, then we get natural maps $(f^{n,i}_b)^* \colon A^{\square^{n+1}} \to A^{\square^n}$ by pullback (aka composition).

(Abstractly, we can say that $A^{\square^\bullet}$ is a cubical set.)

A complex

Now assume that $R$ is a ring, and that the set $A$ above is actually an $R$-module. We are going to build a chain complex

$$\dots \stackrel{d_n}{\longrightarrow} R[A^{\square^n}] \to \dots \stackrel{d_1}{\longrightarrow} \underbrace{R[A^{\square^1}]}_{=R[A^\square]} \stackrel{d_0}{\longrightarrow} \underbrace{R[A^{\square^0}]}_{= R[A]} \to 0$$

[Johan Commelin]

Recall the maps $(f^{n,i}_b)^* \colon A^{\square^{n+1}} \to A^{\square^n}$ from before. Since $A$ has an addition, we can consider the map

$$\sigma^{n,i} := (f^{n,i}_0)^* + (f^{n,i}_1)^* \colon A^{\square^{n+1}} \to A^{\square^n}$$

Now we define

$$d_n := \sum_i (-1)^i \cdot (R[(f^{n,i}_0)^*] + R[(f^{n,i}_1)^*] - R[\sigma^{n,i}])$$

This is the differential in the complex above.

(Abstractly, we are taking the alternating face map complex of a semisimplicial module constructed from the cubical module $A^{\square^\bullet}$.)

[Johan Commelin]

If you know that construction of the Breen--Deligne data from the blueprint, then you can work out for yourself that the definition in this thread is isomorphic to the recursive construction in the blueprint.

[Johan Commelin]

Computational challenge

Compute the homology groups $H_i$ of this complex for various $R$ and $A$.

[Johan Commelin]

I have a script that computes h(p,n) which is the dimension of $H_n$ for $R = A = \mathbb F_p$. But it is completely brute force, and quicly runs out of steam.

[Johan Commelin]

My results so far:

sage: [h(p,0) for p in primes_first_n(10)]                                                                                              [38/1895]
[1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
sage: h(2,1)
3
sage: h(2,2)
7
sage: h(2,3)
16
sage: h(3,1)
3
sage: h(3,2)
6
sage: h(5,1)
3
sage: h(5,2)
6
sage: h(7,1)
3
sage: h(11,1)
3
sage: h(13,1)
3
sage: h(17,1)
3

The script crashes on h(7,2).

[Johan Commelin]

It would be really quite interesting if we can compute h(3,3) and/or h(7,2).

[Johan Commelin]

But I'm quite a bad python/sage programmer, so my script is a bit messy. (For example: I'm modelling $R[A^n]$ using defaultdict(int) which is maybe not optimal.)

[Johan Commelin]

@Mario Carneiro Is there any chance we can do something like this in Lean?

[Mario Carneiro]

I've been thinking of commenting but I don't know what $H_n$ is

[Mario Carneiro]

and also what are the numbers coming out of your h(p,n) function? You said it was a group?

[Johan Commelin]

It is $\mathrm{Ker}(d_{n-1}) / \mathrm{Im}(d_n)$, where $\mathrm{Ker}(d_{-1}) = 0$ by convention.

[Mario Carneiro]

what does the code actually look like?

[Johan Commelin]

h(p,n) is the dimension of the homology group as $R$-vector space. (We've specialized to $R = A = \mathbb F_p$ here.)

[Johan Commelin]

Let me post a gist of what I have now.

[Johan Commelin]

https://gist.github.com/64480a449fba8dcc4e76a19e6cb3b5df

[Mario Carneiro]

I guess there is some theorem that says that the group is uniquely determined by this number?

[Johan Commelin]

Well, it's the dimension of a vector space. For now that's good enough.

[Johan Commelin]

Later on, we might want to have an explicit basis. But those quickly become to large to think about.

[Johan Commelin]

If $R$ is not a field, then the structure of $H_i$ can be a lot more delicate. What I'm really interested in is $R = A = \Z$. But that case is potentially very infinite in several ways. However, it turns out that you can reconstruct quite some interesting info by looking at $R = A = \mathbb F_p$ for all primes $p$.

[Johan Commelin]

And then everything is finite.

[Johan Commelin]

So the gist that I posted above has some really horrible code. And it's not formally verified :see_no_evil:

[Johan Commelin]

But computing $\mathrm{Im}(d_n)$ in Lean requires some algorithms (Gauss, or something?) that we don't have yet. And they need to be fast... we are quickly talking about the span of ~ 1 million vectors in ~1000 dimensional vector spaces.

[Mario Carneiro]

The first thing I would try to get a bit farther is put it in a more efficient language. This is the only part I don't know how to do, since it's relying essentially on sage

def im(b, i):
    V = VectorSpace(GF(b), b**(2**i))
    ts = product(range(b), repeat=2**(i+1))
    dts = [evd(i, single(t)) for t in ts]
    vs = [enc(b, dt, 2**i) for dt in dts]
    W = V.subspace(vs)
    return W.dimension()

[Johan Commelin]

What do you mean with "more efficient language"? Something that is not python?

[Mario Carneiro]

yes

[Mario Carneiro]

I would expect a ~1000x speedup rewriting a pure python program into C/C++/Rust

[Mario Carneiro]

that might be enough to calculate one step farther, although given the growth rate it probably won't get you that far

[Johan Commelin]

Sure, this stuff grows wickedly fast (-;

[Johan Commelin]

So I guess we should rewrite it in Lean 4? :rofl:

[Johan Commelin]

http://www-scf.usc.edu/~hoyeeche/papers/matrix-rank_conf.pdf gives an algorithm that is faster than Gauss

[Riccardo Brasca]

I cannot help with the programming, but my university's machine is working on h(7,2) and h(3,3). I can leave it like this for weeks... or until someone will write a faster program :)

[Johan Commelin]

On my server it crashed...

sage: h(7,2)
/usr/share/sagemath/bin/sage-python: line 2: 2841865 Killed                  sage -python "$@"

[Johan Commelin]

I don't know if it ran out of memory...

[Mario Carneiro]

Are the finite fields of interest primes or prime powers?

[Johan Commelin]

I would just go for p^1 for now.

[Johan Commelin]

The prime power fields don't help with getting information about $R = \Z$.

[Kevin Buzzard]

Do you ever use that A is an R-module rather than just an abelian group?

[Johan Commelin]

I thought I convinced myself that I needed that. But now I don't know why.

[Kevin Buzzard]

If you want to try and evaluate the cokernel of $d_0$ (there's a typo above by the way, the kernel of $d_{-1}$ is top not bot) then there's a map $R[A]\to A$ in the module case but not in general.

[Johan Commelin]

Kevin Buzzard said:

(there's a typo above by the way, the kernel of $d_{-1}$ is top not bot)

thanks, I'll fix it

[Johan Commelin]

Right, it's that map $R[A] \to A$! That's the reason I wanted $A$ to be an $R$-module. But I guess we might want to consider the complex in general.

[Johan Commelin]

In fact, it might be interesting to consider $R = \mathbb Q, \mathbb F_2, \mathbb F_3, \dots$ and $A = \Z/p^k\Z$.

[Kevin Buzzard]

If I didn't slip up, then $d_0:R[A^2]\to R[A]$ is the map which sends $[a_0,a_1]\in A^2$ to $[a_0]+[a_1]-[a_0+a_1]$ and $d_1:R[A^{2\times 2}]\to R[A^2]$ sends $[a_{00},a_{01},a_{10},a_{11}]$ to $[a_{00},a_{01}]+[a_{10},a_{11}]-[a_{00}+a_{10},a_{01}+a_{11}]-[a_{00},a_{10}]-[a_{01},a_{11}]+[a_{00}+a_{01},a_{10}+a_{11}].$

[Johan Commelin]

Yep, that looks right.

[Johan Commelin]

In fact, I can show that with $R = A = \Z$ we get a $\Z^{2^i}$ split subgroup in $H_i$.
The reason is that $\mathrm{Im}(d)$ is contained in the kernel of $Q_j \colon R[A^{2^i}] \stackrel{q_j}{\to} R[A] \to A$, where $q_j$ is induced by the $j$-th projection $A^{2^i} \to A$.
But I can exhibit $2^i$ elements $x_k$ of the kernel that are mapped under $Q_j$ to the Kronecker delta $\delta_{jk}$.

[Johan Commelin]

Those elements $x_k$ are $[e_k] - [0]$, where $e_k$ is the $k$-th unit vector in $A^{2^i}$. (You can show that they are in the kernel of $d$.)

[Kevin Buzzard]

Is this the cohomology of some topological object $X(A)$? I have no idea how to approach these sorts of questions but I kind of wonder whether a topologist might say "oh yeah I've seen that complex before"

[Johan Commelin]

Peter doesn't recognize it so far. This is one reason why I'm trying to compute these "small" cases explicitly. Maybe that will point us somewhere.

[Riccardo Brasca]

3,7,16,3,6 doesn't exist on oeis :unamused:

[Johan Commelin]

But which sequence is that? h(2,i) starts with 1,3,7,16.

[Johan Commelin]

But the 3,6 come from h(3,i), right? (For i=1,2.)

[Riccardo Brasca]

ah yes, sorry

[Johan Commelin]

Note that there is this crazy homotopy between $C(A^2 \stackrel{+}{\to} A)$ and $C(A^2 \stackrel{\pi_1}{\to} A) + C(A^2 \stackrel{\pi_2}{\to} A)$. I think this means that if $R$ and $A$ have coprime characteristics, then the homology vanishes.

[Peter Scholze]

Let me explain a little what's going on. So Johan built this explicit Breen--Deligne data of the form $C(A): \ldots\to \mathbb Z[A^8]\to \mathbb Z[A^4]\to \mathbb Z[A^2]\to \mathbb Z[A]$ where the first two differentials are made explicit by Kevin above, and in general have some rather simple description as Johan wrote at the beginning of this thread. Here $A$ is any abelian group.

It is known that the homology groups of $C(A)$ satisfy $H_i(C(A\oplus B))\cong H_i(C(A))\oplus H_i(C(B))$. Moreover, $C(A)$ obviously commutes with filtered colimits and simplicial resolutions; this gives a recipee for computing $C(A)$ for general $A$ in terms of $C(\mathbb Z)$, and unwinding one finds that for all $A$ there are (functorial, and noncanonically split) exact sequences

$0\to H_i(C(\mathbb Z))\otimes A\to H_i(C(A))\to \mathrm{Tor}_1(H_{i-1}(C(\mathbb Z)),A)\to 0.$

(Here and in the following, any undecorated tensor product or $\mathrm{Tor}$ is over $\mathbb Z$.) In this sense, knowledge of $H_i(C(\mathbb Z))$ is (largely) enough to determine $H_i(C(A))$ in general. Moreover, it is known that $H_i(C(\mathbb Z))$ is a finitely generated abelian group, so is a sum of a free part and some direct sum of cyclic modules of various $p$-power orders.

Above, Johan actually considered the complex $C(A)\otimes R$ for some further auxiliary ring $R$. (So no, it's not required that $A$ is an $R$-module.) Again, by general nonsense the universal coefficient theorem there are (in this case, noncanonically split) exact sequences

$0\to H_i(C(A))\otimes R\to H_i(C(A)\otimes R)\to \mathrm{Tor}_1(H_{i-1}(C(A)),R)\to 0.$

Note that a consequence of these things is that if $A\otimes R=0$, then $H_i(C(A)\otimes R)=0$. So in this way, when we choose $R=\mathbb F_p$, $A=\mathbb F_p$ is the most reasonable choice.

Johan has proved by hand that $H_0(C(\mathbb Z))=\mathbb Z$ and $H_1(C(\mathbb Z))=\mathbb Z^2$, and in general that $H_i(C(\mathbb Z))$ has a summand $\mathbb Z^{2^i}$. From his computations, it seems likely that $H_2(C(\mathbb Z))=\mathbb Z^4\oplus \mathbb Z/2\mathbb Z$.

Also note that the second sequence above implies (noting that $H_i(C(\mathbb F_p))$ is known to be killed by $p$, and thus an $\mathbb F_p$-vector space)

$h(p,i):=\mathrm{dim}(H_i(C(\mathbb F_p)\otimes \mathbb F_p)) = \mathrm{dim}(H_i(C(\mathbb F_p))) + \mathrm{dim} (H_{i-1}(C(\mathbb F_p)))$

and the first sequence can then be used to relate this to information about $C(\mathbb Z)$. Note that the dimension of $\mathrm{Tor}_1(H_i(C(\mathbb Z)),\mathbb F_p)$ is the number of cyclic summands of $p$-power order, equivalently $\mathrm{dim}(H_i(C(\mathbb Z))_{\mathrm{tor}}/p)$. One formula is then

$h(p,i) = \mathrm{dim}(H_i(C(\mathbb Z))/p) + \mathrm{dim}(H_{i-1}(C(\mathbb Z))/p) + \mathrm{dim}(H_{i-1}(C(\mathbb Z))_{\mathrm{tor}}/p) + \mathrm{dim}(H_{i-2}(C(\mathbb Z))_{\mathrm{tor}}/p).$

[Chris Birkbeck]

Maybe I haven't understood whats going on, but aren't some bits of your code are growing doubly exponentially, like the ts in your im(_,_) definition. So maybe its not suprising that you can only compute the first few examples. Can the same homology be computed by some other complex that doesn't grow as quickly?

[Peter Scholze]

Yeah, double exponential growth seems to be a recurring theme in this stream :-D

[Peter Scholze]

So as an example $H_0(C(\mathbb Z))=\mathbb Z$ means that we have $h(p,0)=0$ for all $p$, and $H_1(C(\mathbb Z))=\mathbb Z^2$ means $h(p,1)=1+2=3$ for all $p$. If $H_2(C(\mathbb Z))=\mathbb Z^4\oplus \mathbb Z/2\mathbb Z$, then $h(2,2)=5+2=7$ while we should have $h(p,2)=4+2=6$ for all $p>2$.

[Johan Commelin]

Do you mean $h(p,0) = 1$ at the begin of :this: (you now have $h(p,0) = 0$)?

[Peter Scholze]

I would expect that $H_3(C(\mathbb Z))$ has no $3$-torsion; in general I would expect $p$-torsion to appear only from degree $2p-2$ (there is no strong argument for this, but this happens in the integral dual Steenrod algebra, which is of some relevance here). If we hope that $H_3(C(\mathbb Z))=\mathbb Z^8 \oplus (\mathrm{torsion})$ (so that Johan's split $\mathbb Z^{2^i}$ is the correct answer at least modulo torsion), and that there is no $3$-torsion, then we should hope that $h(3,3)=8+4=12$.

[Peter Scholze]

Conversely, if $h(3,3)=12$ is true, then it follows that the rank of $H_3(C(\mathbb Z))$ is indeed $8$ and there is no $3$-torsion.

[Peter Scholze]

So I think the computation of $h(3,3)$ gives the most information. $h(7,2)$ would only confirm that there is no $7$-torsion in $H_2(C(\mathbb Z))$, but that seems extremely likely.

[Johan Commelin]

Which means we need to compute the dimension of a subspace of a 6561-dimensional vector space over $\mathbb F_3$ generated by 43046721 vectors :oops:

[Riccardo Brasca]

Anyway I confirm that the problem is the memory

[Peter Scholze]

Well, I do think/hope that there should be enough exploitable structure here to cut the problem to reasonable size...

[Peter Scholze]

Note that $h(2,3)=16$ means that $\mathrm{dim}(H_3(C(\mathbb Z))/2)=10$, so we already know that the rank is bounded by $10$. And it would seem quite likely that there are ~2 $2$-torsion summands. So I think one can be optimistic that Johan's split $\mathbb Z^{2^i}$ gives the correct rank.

[Chris Birkbeck]

Well, so if instead of looking at the subspace generated by all the 43046721 vectors , you instead pick 10000 random elements and check the resulting dimension, then I managed to get 12 both times I did this. But even this is slow, since sage takes a while to find the subspace defined by these random vectors. But at least 12 showed up again as Peter is predicting.

[Chris Birkbeck]

This is for h(3,3) I should add

[Johan Commelin]

@Chris Birkbeck Cool, that's really nice to know!

[Johan Commelin]

I guess we can try to do similar randomized computations for some other values.

[Chris Birkbeck]

Yeah, I was about to try h(7,2).

[Peter Scholze]

Lol, when I talked to Johan yesterday, I was suggesting this very algorithm of picking 10000 random vector first ;-)

[Peter Scholze]

(Note that the codimension is necessarily at least $12$, so if the 10000 random vectors already give this codimension, the result has to be exact.)

[Chris Birkbeck]

Oh haha nice. Yes sometimes this is a good way to cheat!

[Chris Birkbeck]

I just did h(7,2) (with the random sampling) and it came out to be 6 just as predicted :)

[Johan Commelin]

Ooh, that's a really nice observation!

[Peter Scholze]

I didn't check the numbers, but is it at all feasible to compute $h(2,4)$? (It would probably only give limited information unless we start to have some better idea of the $2$-torsion in $H_i(C)$, but I gather it's the only possible computation we can hope for about homology in degree $4$.)

[Peter Scholze]

I gather this is about some $65536$-dimensional space?

[Riccardo Brasca]

@Chris Birkbeck can you share the code to test the random sampling? I am really bad at this kind of stuff, but I like playing with them :D

[Chris Birkbeck]

@Peter Scholze yes
@Riccardo Brasca Yes certainly, let me just get it together :)

[Peter Scholze]

(lower bound on $h(2,4)$, achieved only when $H_4(C(\mathbb Z))$ has no $2$-torsion, which is extremely unlikely: $29$)

[Peter Scholze]

(So there's a nonzero chance that the answer is $42$ :wink: .)

[Johan Commelin]

Peter Scholze said:

I gather this is about some $65536$-dimensional space?

Right, so an exhaustive search has to treat 4294967296 vectors

[Chris Birkbeck]

Here are the bits of code you can just add at the end of Johan's code:

def Imsample(b, i, samplesize):
    V = VectorSpace(GF(b), b**(2**i))
    ts = product(range(b), repeat=2**(i+1))
    vt=list(ts)
    size=len(vt)
    dts = [evd(i, single(vt[randint(0,size-1)])) for t in range(samplesize)]
    vs = [enc(b, dt, 2**i) for dt in dts]
    W = V.subspace(vs)
    return W

def imsample(b, i, S):
    W = Imsample(b, i,S)
    return W.dimension()

def hsample(b, i,S):
    return ker(b, i) - imsample(b, i,S)

[Chris Birkbeck]

Its not pretty, but it works sometimes. I also didnt want to sample the kernel, but this could be done if needed.

[Peter Scholze]

@Johan Commelin Sure, but I gather some random $100000$ vectors will do. So this is only a factor ~100 above the randomized computation of $h(3,3)$.

[Johan Commelin]

Mario has a rust implementation. We are working on randomizing it right now. It could do 1% of the exhaustive h(3,3) computation in a bit more than a minute.

[Chris Birkbeck]

Yeah I'm trying with a sample size of 70000 at the moment to see what happens. It'll be a while since sage is slow to compute the subspace, but lets see

[Chris Birkbeck]

@Johan Commelin Oh that sounds much better!

[Peter Scholze]

Ah! A general comment is that $C(A)$ admits $C(A)^{\oplus 2}[-1]$ as a direct summand (functorially in $A$). I think this was at least implicitly already observed by Johan. It's a simple consequence of the cubical description; just embed (resp.~project to) codimension $1$ cubes. Let $\overline{C}(A)$ be the complementary direct summand.

In particular, $H_i(C(\mathbb Z)) = H_{i-1}(C(\mathbb Z))^{\oplus 2}\oplus H_i(\overline{C}(\mathbb Z))$, and we know $H_0(\overline{C}(\mathbb Z))=\mathbb Z$ (which then by induction give those summands $\mathbb Z^{2^i}$ of $H_i(C(\mathbb Z))$) and $H_1(\overline{C}(\mathbb Z))=0$, and we suspect $H_2(\overline{C}(\mathbb Z))=\mathbb Z/2\mathbb Z$. This in turn already gives a $2$-dimensional contribution to the $2$-torsion of $H_3(C(\mathbb Z))$, which by the computation of $h(2,3)$ must actually be everything. So $H_3(\overline{C}(\mathbb Z))$ has no $2$ or $3$-torsion, and so is surely $0$.

So $H_i(\overline{C}(\mathbb Z))$ starts with $\mathbb Z,0,\mathbb Z/2\mathbb Z,0,\ldots$.

[Mario Carneiro]

Rust implementation here: https://gist.github.com/digama0/6d7bf9693947113eec607d81d9336ccb

[Peter Scholze]

Also, a new lower bound for $h(2,4)$ is $33$.

[Johan Commelin]

I'll start running the rust code on my server

[Johan Commelin]

How does $H_i(\Z \otimes_{\mathbb S} \Z)$ start?

[Mario Carneiro]

If the rust program reaches $65305 - 33 = 65272$ then you win

[Peter Scholze]

The same :smile:

[Peter Scholze]

I'd have to check what is in degree $4$...

[Mario Carneiro]

the rust program calculates im(b, i) instead of h(b, i) so there is some translation necessary

[Peter Scholze]

OK, I bet 1 euro on $h(2,4)=34$

[Peter Scholze]

Wait, let me think for a moment

[Peter Scholze]

So even if my conceptual guess is right, I probably screwed up the relevant computation...

[Johan Commelin]

The rust program has been running for 4:50 now, and it has found 10000 lin indep vectors in the image.

[Johan Commelin]

I guess it will start slowing down at some point. But maybe in half an hour it will be close to 65000

[Johan Commelin]

After running for 15 minutes we have about 15500 lin indep vectors. So it's certainly slowing down fast.

[Alex J. Best]

What is the bottleneck for the current implementation?

[Johan Commelin]

My guess: Gaussian elimination

[Johan Commelin]

It's single-threaded, not running out of memory any time soon. (It's using 4% of my RAM, atm, and the implementation is basically constant memory.)

[Chris Birkbeck]

Well I just realised that quick thing I wrote wont work since it tries to first list all the vectors before starting to sample them, so thats not gonna work lol

[Johan Commelin]

The rust implementation is streaming the vectors in a random way, and running Gauss on that stream.

[Johan Commelin]

It has now slowed down to finding a bit more than 1 new dimension per second.

[Chris Birkbeck]

thats much better. I don't know anything about rust, so I have no idea how good its at Gaussian elimination.

[Peter Scholze]

Can you simultaneously at each step compute the quotient space by the current image, with explicit transition?

[Johan Commelin]

Mario just implemented Gauss from scratch

[Johan Commelin]

@Peter Scholze what exactly do you mean with "explicit transition"?

[Johan Commelin]

Also what is on top of the quotient? The ambient space, or the kernel? We don't have a basis for the kernel.

[Johan Commelin]

Ooh, do you mean we have $C_{i+1} \stackrel{d_i}{\to} C_i$, and we sample random vectors in $C_{i+1}$. Whenever we find a vector that is dependent on stuff that we have found, then we mod out $C_{i+1}$ by this vector, and start sampling from the smaller space?

[Johan Commelin]

That sounds like a good optimization. And we might need that to finish this computation.

[Peter Scholze]

I think I agree, except that "dependent" should read "independent"

[Peter Scholze]

Or wait

[Peter Scholze]

I mean we want to compute the image of $d_i$

[Peter Scholze]

Whenever you find a new vector in the image, pass to the quotient of $C_i$ by this vector

[Johan Commelin]

But we shouldn't sample vectors from the kernel of $d_i$. So if we do that by chance, we mod it out, so that we don't do that again.

[Peter Scholze]

And always explicitly keep track of the map $C_i\to \mathrm{current quotient}$

[Peter Scholze]

I think the chance to hit something in the kernel is small

[Peter Scholze]

This way, you only do Gaussian elimination against one vector

[Johan Commelin]

But the chance that you hit something in the kernel of $C_{i+1} \to C_i \to C_i/\textrm{whatwehavefound}$ gets larger and larger.

[Peter Scholze]

Hmm, it should always be tiny I think

[Johan Commelin]

I guess for the final vector its 1/p, right?

[Peter Scholze]

Yes

[Johan Commelin]

But I agree that for everything up to the last couple of vectors, it's very small.

[Peter Scholze]

But $100$ vectors before the end, it's $1/p^{100}$

[Johan Commelin]

Right, so that isn't worth it.

[Johan Commelin]

I guess your suggestion is a more serious speedup :racecar:

[Johan Commelin]

(We're at 18420 vectors now.)

[Johan Commelin]

But maybe the problem would translate into making $C_i \to \textrm{currentquotient}$ a map that is fast to compute.

[Peter Scholze]

Hmm, it's just some $65536\times ~50000$ matrix. I hope the application of such a matrix is fast?

[Johan Commelin]

The Gaussian elimination step needs to find the first non-zero index, and lookup whether there is a vector with that pivot in the existing basis using a binary search. That should be pretty fast as well.

[Johan Commelin]

I don't know enough to compare the speed of two such algorithms

[Johan Commelin]

(After 45 minutes, we have $\approx 19600$ vectors. It's still finding roughly 1 dimension per second.)

[Johan Commelin]

(If we continue with this speed, we'll be done tomorrow morning. But I guess it will slow down further.)

[Chris Birkbeck]

So, is it getting harder to find vectors that are lin indep to the set you already have or is it getting harder to check that they are lin indep? If its the second one then, this might be solvable. For example MAGMA can compute the rank of a 100000x65536 matrix over F_2 in about 3-4 mins.

[Johan Commelin]

I think as Peter pointed out, with chance almost 1 you pick a new vector that is indep. The hard part is the check, I guess.

[Johan Commelin]

It's true that over F_2 things simplify, and we should take advantage of that. For example, if $x \ne 0$, then you never need to multiply by $x^{-1}$, because it's 1 anyway.

[Chris Birkbeck]

Aha I see.

[Johan Commelin]

So, I guess we could export a list of ~100000 vectors out of the rust script, and ask Magma to compute the rank?

[Chris Birkbeck]

Yeah thats what I was thinking

[Johan Commelin]

But Kevin recently pointed out to me that this is a closed source algorithm that nobody knows anything about. (Apart from some magma devs.)

[Chris Birkbeck]

I was tring to get sage to do that, but I'm having problems getting the random vectors.

[Chris Birkbeck]

Haha yes! Sometimes you might get lucky and the code will be visible. But I expect the optimised things are probably not easy to see

[Riccardo Brasca]

Sorry for the stupid question: how do I run the rust code? I have rustc installed. Thank's!

[Johan Commelin]

You need to copy the top comments into the Cargo.toml and then run cargo run --release

[Johan Commelin]

Also, you need rust version > 1.50

[Johan Commelin]

I guess over $\mathbb F_2$, the whole thing can possibly be implemented using bool, xor, and, and or.

[Johan Commelin]

That should be blazingly fast.

[Johan Commelin]

@Mario Carneiro Does that make sense?

[Mario Carneiro]

I just profiled it and there is a huge performance bug, it's all going to the basis.insert call

[Peter Scholze]

By the way, John Rognes' answer here https://mathoverflow.net/questions/50519/integral-cohomology-stable-operations gives a simple answer for what $\mathbb Z\otimes_{\mathbb S} \mathbb Z$ is $2$-locally; and it sounds like there is a very similar description at other primes. Fun fact: No torsion is of the form $\mathbb Z/p^i\mathbb Z$ with $i>1$.

[Chris Birkbeck]

Yeah linear algebra over $\mathbb{F}_2$ is probably the nicest case. There are lots of good algorithms in this case

[Mario Carneiro]

try the gist now. It spends 95% of its time in gaussian_eliminate_one and 42% in Zp::add, so killing the modulo there will probably help

[Johan Commelin]

@Mario Carneiro Should we fork the code for $F_2$, and do everything using booleans there?

[Johan Commelin]

Zp::add would just be xor

[Johan Commelin]

@Peter Scholze thanks for digging up that old MO question!

[Peter Scholze]

I was surprised that I could not dig up a better reference (or that people like John Rognes didn't immediately name a good reference, for that matter)

[Johan Commelin]

Mario Carneiro said:

try the gist now. It spends 95% of its time in gaussian_eliminate_one and 42% in Zp::add, so killing the modulo there will probably help

@Mario Carneiro you mean that it's worth it to restart the script now?

[Mario Carneiro]

Oh yes

[Mario Carneiro]

it was spending 97% of its time in insert

[Johan Commelin]

Wow! It hit 10.000 in 10s!

[Mario Carneiro]

now that's down to 0.38%

[Mario Carneiro]

Actually, we're modding by % B where B is a compile time constant 2

[Mario Carneiro]

this is for sure optimized to a bit mask

[Mario Carneiro]

so I think that rewriting with bool won't help much

[Johan Commelin]

Do you think all the other operations in $\mathbb F_2$ were also optimized away by the compiler?

[Johan Commelin]

(After 4 minutes the output is now at 14500, so after reaching 10000 it quickly starts slowing down again.)

[Peter Scholze]

(So yes, at all primes the formula is

$\mathbb Z_{(p)}\otimes_{\mathbb S} \mathbb Z_{(p)}\cong \bigotimes^L_{i\geq 1} \mathbb Z_{(p)}[x_i]/(px_i)$

where $x_i$ has degree $2p^i - 2$.)

[Johan Commelin]

@Mario Carneiro I think the Zp should also be renamed to Fp to avoid confusion with $\Z_p$ or $\Z_{(p)}$.

[Johan Commelin]

So h(3,4) should see a bit of 3-torsion? Hopefully? But let's first try to get h(2,4) computable.

[Johan Commelin]

(11 minutes: 16000 vectors)

[Johan Commelin]

30 minutes: 18500 vectors

[Peter Scholze]

OK, this doesn't look good

[Riccardo Brasca]

I am at 23000, but I think I started earlier than Johan :(

[Mario Carneiro]

I tried multithreading it, but it's even slower. The basis vector data structure needs to be read-write locked and there are way too many writers; it easily gets deadlocked with one reader starving all the writers, and with more fine grained locking the overhead is too great

[Mario Carneiro]

I was wrong about % B being optimized; I was using mod_euclid() in order to get the right behavior at negatives and apparently the optimizer doesn't know about it. Removing the reduced row echelon stage in gaussian elimination (where you use the new row to simplify the others) also significantly improves performance. It now gets to 14500 in 23 seconds

[Johan Commelin]

@Mario Carneiro but it still isn't using bool as model for Fp when p = 2, right?

[Mario Carneiro]

not bool, but (x + y) & 1

[Johan Commelin]

I was thinking that we could maybe also optimize the binary search away. Because we expect the rank to be "almost" 2^16.

[Johan Commelin]

So if we find a new vector with first nonzero entry i and we don't have another such vector yet, we just insert it as row i in a $2^{16} \times 2^{16}$ matrix that is initialized to 0.

[Johan Commelin]

Mario Carneiro said:

not bool, but (x + y) & 1

But addition could just be xoring 2^13 bytes together, right?

[Mario Carneiro]

updated the gist. Using bool doesn't make a huge improvement, but it does allow for using bitsets which could be a big boost

[Johan Commelin]

Ok, I'm restarting. I was at 1h17, 23.000 vectors

[Johan Commelin]

41s, 15.000 vectors

[Johan Commelin]

I think my cores are not so fast (-;

[Mario Carneiro]

we should try to get a plot of the rate of growth and estimate how slow it will be at the end

[Johan Commelin]

2min, 16400

[Johan Commelin]

So there's really a sharp bent there. I wonder whether it has to do with caches. When the "basis found so far" no longer fits in a certain cache, it might start slowing down fast??

[Johan Commelin]

I wonder if a divide and conquer approach makes sense: have multiple cores compute 10.000 lin indep vectors, and then have a single process that joins them together and does another Gauss elimination.

[Johan Commelin]

But maybe that doesn't actually help so much

[Johan Commelin]

6min, 18500

[Johan Commelin]

10min, 20000

[Johan Commelin]

@Chris Birkbeck did you finish a computation of h(2,7)?

[Riccardo Brasca]

I guess I was using the old version... I am at 15000 in kind of 45 seconds

[Chris Birkbeck]

Do you mean h(7,2)? If so yes. It was 6.

[Johan Commelin]

Oh, yes, I meant h(7,2). Thanks.

[Johan Commelin]

I'm now at 26:30 and 24000 vectors

[Johan Commelin]

1h27, 32600

[Johan Commelin]

It's still finding >1 vector per second.

[Riccardo Brasca]

I understand this is completely stupid, but I am at 34500 :sunglasses:

[Matthew Ballard]

Out of curiosity what are the specs on your machines @Johan Commelin and @Riccardo Brasca?

[Riccardo Brasca]

My university gives me a 16-cores with 62 GB of Ram. cat /proc/cpuinfo says

processor   : 0
vendor_id   : GenuineIntel
cpu family  : 6
model       : 63
model name  : Intel(R) Xeon(R) CPU E5-2623 v3 @ 3.00GHz
stepping    : 2
microcode   : 0x43
cpu MHz     : 3360.875
cache size  : 10240 KB
physical id : 0
siblings    : 8
core id     : 0
cpu cores   : 4
apicid      : 0
initial apicid  : 0
fpu     : yes
fpu_exception   : yes
cpuid level : 15
wp      : yes
flags       : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 clflush dts acpi mmx fxsr sse sse2 ss ht tm pbe syscall nx pdpe1gb rdtscp lm constant_tsc arch_perfmon pebs bts rep_good nopl xtopology nonstop_tsc cpuid aperfmperf pni pclmulqdq dtes64 monitor ds_cpl vmx smx est tm2 ssse3 sdbg fma cx16 xtpr pdcm pcid dca sse4_1 sse4_2 x2apic movbe popcnt tsc_deadline_timer aes xsave avx f16c rdrand lahf_lm abm cpuid_fault epb invpcid_single pti ssbd ibrs ibpb stibp tpr_shadow vnmi flexpriority ept vpid ept_ad fsgsbase tsc_adjust bmi1 avx2 smep bmi2 erms invpcid cqm xsaveopt cqm_llc cqm_occup_llc dtherm ida arat pln pts md_clear flush_l1d
bugs        : cpu_meltdown spectre_v1 spectre_v2 spec_store_bypass l1tf mds swapgs itlb_multihit
bogomips    : 6000.11
clflush size    : 64
cache_alignment : 64
address sizes   : 46 bits physical, 48 bits virtual
power management:

[Riccardo Brasca]

I can also use a 48-cores machine with 315GM of ram.

processor   : 0
vendor_id   : GenuineIntel
cpu family  : 6
model       : 85
model name  : Intel(R) Xeon(R) Gold 6126 CPU @ 2.60GHz
stepping    : 4
microcode   : 0x2000043
cpu MHz     : 999.873
cache size  : 19712 KB
physical id : 0
siblings    : 24
core id     : 0
cpu cores   : 12
apicid      : 0
initial apicid  : 0
fpu     : yes
fpu_exception   : yes
cpuid level : 22
wp      : yes
flags       : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 clflush dts acpi mmx fxsr sse sse2 ss ht tm pbe syscall nx pdpe1gb rdtscp lm constant_tsc art arch_perfmon pebs bts rep_good nopl xtopology nonstop_tsc cpuid aperfmperf pni pclmulqdq dtes64 monitor ds_cpl vmx smx est tm2 ssse3 sdbg fma cx16 xtpr pdcm pcid dca sse4_1 sse4_2 x2apic movbe popcnt tsc_deadline_timer aes xsave avx f16c rdrand lahf_lm abm 3dnowprefetch cpuid_fault epb cat_l3 cdp_l3 invpcid_single pti intel_ppin mba ibrs ibpb stibp tpr_shadow vnmi flexpriority ept vpid ept_ad fsgsbase tsc_adjust bmi1 hle avx2 smep bmi2 erms invpcid rtm cqm mpx rdt_a avx512f avx512dq rdseed adx smap clflushopt clwb intel_pt avx512cd avx512bw avx512vl xsaveopt xsavec xgetbv1 xsaves cqm_llc cqm_occup_llc cqm_mbm_total cqm_mbm_local dtherm ida arat pln pts pku ospke
bugs        : cpu_meltdown spectre_v1 spectre_v2 spec_store_bypass l1tf mds swapgs taa itlb_multihit
bogomips    : 5200.00
clflush size    : 64
cache_alignment : 64
address sizes   : 46 bits physical, 48 bits virtual
power management:

[Riccardo Brasca]

To be honest I don't even know which one is better, I am playing with both of them

[Matthew Ballard]

Is there stock lean code to benchmark machines against more precisely? (I guess this is slightly off topic)

[Riccardo Brasca]

This question is like Chinese for me :rolling_on_the_floor_laughing:

[Matthew Ballard]

Sorry, I mean. Fix some lean code. Run it on different machines and measure things like memory utilization, cpu time, etc...

[Riccardo Brasca]

No idea. For me Lean is like LaTeX, but when it compiles it means that the math is correct

[Matthew Ballard]

I think this program whomever has the beefiest single core cpu will win.

[Matthew Ballard]

I ran it my laptop with 8 cores @ 1.8 GHz. I got curious and started it on my wife's lowest end macbook air. The air passed it despite the 20 minute lead. It was still slower than your servers. At 40 minutes, it was at 17000.

[Johan Commelin]

I'm at 49000 now, still finding roughly 1 new vector per second.

[Johan Commelin]

Here's my /proc/cpuinfo

processor       : 15
vendor_id       : GenuineIntel
cpu family      : 6
model           : 26
model name      : Intel(R) Xeon(R) CPU           E5540  @ 2.53GHz
stepping        : 5
microcode       : 0x1d
cpu MHz         : 2800.215
cache size      : 8192 KB
physical id     : 1
siblings        : 8
core id         : 3
cpu cores       : 4
apicid          : 23
initial apicid  : 23
fpu             : yes
fpu_exception   : yes
cpuid level     : 11
wp              : yes
flags           : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 clflush dts acpi mmx fxsr sse sse2 ht tm pbe syscall nx rdtscp lm constant_tsc arch_perfmon pebs bts rep_good nopl xtopology nonstop_tsc cpuid aperfmperf pni dtes64 monitor ds_cpl vmx est tm2 ssse3 cx16 xtpr pdcm dca sse4_1 sse4_2 popcnt lahf_lm pti ssbd ibrs ibpb stibp tpr_shadow vnmi flexpriority ept vpid dtherm ida flush_l1d
bugs            : cpu_meltdown spectre_v1 spectre_v2 spec_store_bypass l1tf mds swapgs itlb_multihit
bogomips        : 5066.90
clflush size    : 64
cache_alignment : 64
address sizes   : 40 bits physical, 48 bits virtual
power management:

[Johan Commelin]

I'm a bit worried that the code will not stop when it reaches the end, and will print 10000 lines ofx/10000 for x between 1 and 10000. We should have told the randomized code to stop after it samples 50 vectors in a row that are linearly dependent to the basis found so far.

[Johan Commelin]

The chance that it does that without having found the full image is 1/2^50

[Riccardo Brasca]

image-9840e453-31de-4867-857e-441eb9343b3a.jpg

[Riccardo Brasca]

It is like that since one minute

[Riccardo Brasca]

Same on the other machine, it arrived to 65271.

[Chris Birkbeck]

Oh amazing! I think you got it!

[Chris Birkbeck]

Oh wait, wasnt it 65272 that we expected? hmm

[Riccardo Brasca]

Maybe the script started at 0 instead of 1?

[Riccardo Brasca]

The speed was more or less constant until 65271, and then it stopped

[Yaël Dillies]

Riccardo Brasca said:

Maybe the script started at 0 instead of 1?

Oh no! Not an off-by-one error! Not now!

[Chris Birkbeck]

Ah well, looking back, it seems we said 33 at one point and then Peter bet 1 euro it would be 34. So 65271 would mean Peter is right.

[Peter Scholze]

Unfortunately nobody bet against me, I believe?

[Johan Commelin]

Great! Thanks for all your help! This is valuable input.

[Mathieu Guay-Paquet]

A bit late to the party for h(3, 3), but this might still be useful:

Note that there's a (family of) involutions $F_n : \square^n \to \square^n$ which I'll call bit-flip maps, defined by

$(x_1, \ldots, x_n) \mapsto (1-x_1, \ldots, 1-x_n)$,

and this (family of) maps commutes with the differential $d_n$, in the sense that $d_n \circ R[(F_n)^*] = R[(F_{n+1})^*] \circ d_n$ (assuming I didn't mess up the notation).

These maps give a natural decomposition of $R[A^{\square^n}]$ into a $(+1)$-eigenspace and a $(-1)$-eigenspace for $F_n$, with roughly equal dimensions and nice explicit bases.

Practically, for h(3, 3), this means that we can split the computation: compute the image of $(3^{16}-3^8)/2 = 21520080$ vectors into a $(3^8-3^4)/2 = 3240$ dimensional space, and the image of $(3^{16}+3^8)/2 = 21526641$ vectors into a $(3^8+3^4)/2 = 3321$ dimensional space. Both halves can be done completely in parallel with no synchronization, and the target spaces are roughly half-dimensional compared to the brute force approach.

(Essentially, there's a group action of the two-element group on the spaces $R[A^{\square^n}]$, and the differential $d_n$ commutes with these group actions, so we can use some representation theory to cut down the computation by a lot. For $p \neq 2$, I'm seeing a group action of an abelian group with $2 \times 2 \times (p-1)$ elements which is compatible with the differential, also with reasonably explicit bases, which would further cut down the computation.)

[Johan Commelin]

The next interesting target would be h(3,4). But with our current approach we would need to store a roughly 43Mx43M matrix. Using @Mathieu Guay-Paquet observation, we might be able to cut this down a bit. But even 1Mx1M is still in the order of 1TB of memory. My server doesn't have that. :crazy:
So unfortunately, I think we've hit the limit of what is reasonably computable without more theoretical simplifications.

[Peter Scholze]

Well, I'm convinced already now that the answer is that $\overline{C}(\mathbb Z)$ is quasi-isomorphic to the integral dual Steenrod algebra; and hopefully this is actually not too hard to prove once one tries to sit down and do it. But I won't hold you back from doing further computations if you find that fun :wink:

[Chris Birkbeck]

Yeah it was fun while it lasted, but I think, as it stands, $h(3,4)$ is probably going to be out of reach.

[David Michael Roberts]

Before we get to the point that someone needs to rerun the calculation again, is is possible to store the relevant data (the independent vectors etc) so that the result can be computationally verified independently? I guess if Peter comes up with a pen-and-paper proof of his overall hunch, then it's redundant, but until then it's firm numerical evidence.

[Johan Commelin]

But how do you verify that those independent vectors span the image?

[Johan Commelin]

The script doesn't save the preimages, certainly.

[Johan Commelin]

And if you save the preimage, you basically have to do the full computation again anyway.

[Johan Commelin]

Ooh, that's not true of course, we can save smart preimages, that give a row reduced matrix after taking images again.

[Yaël Dillies]

And I guess we're not gaining much by simply remembering the vectors? What's the ratio of vectors tried/independent vectors found?

[Johan Commelin]

Very close to 1

[David Michael Roberts]

I guess if one has verified independent vectors, then that's a computation one doesn't have to do again. But I didn't go through the script to see what it was doing, so take what I'm saying with a very large grain of salt.

[Johan Commelin]

The script isn't formally verified in the sense of lean

[Peter Scholze]

I currently don't have access to it, but I strongly suspect that MacLane "Homologie des anneaux et des modules" https://zbmath.org/?q=an%3A0084.26703 has Johan's complex, and proves the conjectured description

[David Michael Roberts]

@Johan Commelin Yes, I know. I meant in the colloquial sense, not in the formal sense.

[Mario Carneiro]

I don't think the computation that was run for h(2, 4) is even an informal proof. We have a lower bound of $33$ and the random guessing approach yields an upper bound of $34$, and given the pattern we saw where the vectors keep coming for a while at a constant rate and then just stop at the limit, assuming the vectors really are random it's probably possible to turn that into a probabilistic argument that the chance the value is not $34$ is $2^{-100}$ or something (depending on how long it was run after hitting the limit), but only the exhaustive search method can actually produce a proof, and I don't think anyone attempted to run it

[Peter Scholze]

Section 6 of this paper https://www.ams.org/journals/tran/1998-350-04/S0002-9947-98-02067-4/ is very relevant; I think MacLane really has proved this back then.

[David Michael Roberts]

@Peter Scholze it looks like Mac Lane might have published the stuff from the Belgian seminar in https://doi.org/10.1215/ijm/1255454537 see in particular section 3.

[Peter Scholze]

Section 12 of https://www.ams.org/journals/tran/1951-071-02/S0002-9947-1951-0043774-8/home.html is also very relevant

[David Michael Roberts]

Though, sadly, he cites "Homologie des anneaux..." for more details at one point :-(

[Adam Topaz]

https://arxiv.org/abs/2011.01620 seems relevant as well

[Riccardo Brasca]

I have Mac Lane paper if someone wants to have a look

[David Michael Roberts]

@Riccardo Brasca ah, do share it!

[David Michael Roberts]

Mac Lane credits Dixmier, and section 6 of http://www.numdam.org/item/?id=ASENS_1957_3_74_1_25_0 seems to be relevant, though it's for Lie algebras, and very much nuts and bolts.

But the paper @Adam Topaz linked looks pretty sweet, and a lot closer to where Peter wants to end up, methinks.

[Adam Topaz]

(I don't know why our linkifier arxiv#2011.01620 doesn't work)

[Peter Scholze]

Yeah. I'm still slightly confused about the way they pass to the normalized subcomplex versus how I wanted to do it above, but apart from this, everything seems to be there

[Peter Scholze]

OK, this is somewhat embarrassing. I knew about the name "MacLane homology", as after all it is the same as topological Hochschild homology. (So what is called MacLane homology is not quite this cubical thing considered here, but something else where this is a key step.) But I never bothered to read any details about MacLane homology.

[David Michael Roberts]

Last reference: https://core.ac.uk/download/pdf/82624711.pdf section 2. But some people now have the original, so that's it from me :-)

[Kevin Buzzard]

Amusingly, in that last reference the authors thank MacLane for giving them a copy of the mysterious Belgium paper "which had been unavailable to us" :-)

[Peter Scholze]

So I think the key argument is spelled out in Proposition 7.4 here https://www.ams.org/journals/tran/1998-350-04/S0002-9947-98-02067-4/

[Peter Scholze]

This is using critically, I believe, that one has modded out by all "slabs and diagonals", so I think strictly speaking the computation of what I denoted $\overline{C}(\mathbb Z)$ above may still be open

[Peter Scholze]

In particular, it may be that nobody has actually yet computed the homology of $C(\mathbb Z)$ (usually denoted $Q'(\mathbb Z)$ in the literature)

[Peter Scholze]

But it may also very well be that there is a very simple argument deducing it

[Peter Scholze]

Actually, relooking at the way I tried to normalize things, I think my claim that $C(A)$ contains $C(A)^{\oplus 2}[-1]$ as a summand is nonsense. Or at least I don't see how.

[Peter Scholze]

On the other hand, the claim has very solid computational support :stuck_out_tongue_wink:

[Peter Scholze]

OK, I have a proof of the computation; it's trivial :wink:

[Johan Commelin]

Hey! For the first time in 2 weeks I close Zulip for an hour... :shock: :rofl:

[Johan Commelin]

So where do we stand now? Is there anything left that is not completely obvious?

[David Michael Roberts]

So what's the actual statement, @Peter Scholze ?

[Peter Scholze]

Using all the jargon: The linearization of the functor $A\mapsto \mathbb Z[A]$ is the functor $A\mapsto \mathbb Z\otimes_{\mathbb S} A$ (this is an easy exercise in the definition of "linearization" = "Goodwillie derivative"). This means that the linearization of $C(A)$ can be computed by a complex of the form

$C(A)^{\mathrm{lin}}: \ldots \to \mathbb Z\otimes_{\mathbb S} A^4\to \mathbb Z\otimes_{\mathbb S} A^2\to \mathbb Z\otimes_{\mathbb S} A\to 0,$

where one has to suitably interpret this (as each term is a complex itself, so we're really doing some double complex stuff). But $C(A)$ is already linear in $A$, so this complex is quasi-isomorphic to $C(A)$.

On the other hand, there is a natural map $C(A)^{\oplus 2}[-1]\to C(A)$, including two opposite codimension $1$ faces. After linearization, this gives a map

$[\ldots \to \mathbb Z\otimes_{\mathbb S} A^4\to \mathbb Z\otimes_{\mathbb S} A^2\to 0\to 0]\to [\ldots \to \mathbb Z\otimes_{\mathbb S} A^4\to \mathbb Z\otimes_{\mathbb S} A^2\to \mathbb Z\otimes_{\mathbb S} A\to 0]$

whose cone is exactly the only remaining term $\mathbb Z\otimes_{\mathbb S} A$. But this maps naturally into the linearization of $C(A)$, so we get a splitting

$C(A)^{\mathrm{lin}}\cong C(A)^{\oplus 2}[-1]^{\mathrm{lin}}\oplus \mathbb Z\otimes_{\mathbb S} A.$

Again, there is a natural quasi-isomorphism $C(A)\to C(A)^{\mathrm{lin}}$. So the upshot is that there is a natural quasi-isomorphism

$C(A)\cong C(A)^{\oplus 2}[-1]\oplus \mathbb Z\otimes_{\mathbb S} A,$

i.e.

$C(A)\cong \bigoplus_{n\geq 0} \mathbb Z\otimes_{\mathbb S} A^{\oplus 2^n}[-n]$

by telescoping.

[Johan Commelin]

So the claim that $C(A)$ can be used to show that Ext groups vanish. Is that also part of the deluge of literature posted in the last hour? Or is that still new?

[Johan Commelin]

Also, do the computations above now give $\bar C(\Z) \cong \Z \otimes_{\mathbb S} \Z$ as a corollary?

[Johan Commelin]

Ooh right, it's in the 2nd-but-last display of Peter's post above (up to quasi-iso).

[Peter Scholze]

So the literature mostly considers a slightly different complex, modding out by more stuff, so strictly speaking I'm not sure whether the homology of $C(\mathbb Z)$ can be found in the literature. (Granted, to experts it may be obvious as per the argument above.) On the other hand, I still think the observation that this can be used for the computation of certain homology groups, as a substitute for Breen--Deligne resolutions, may still be new.

[Riccardo Brasca]

I asked to the second author of https://arxiv.org/abs/2011.01620 if he has any idea about the homology of our complex (I don't know him personally, but he appears very often in my twitter...)

[David Michael Roberts]

Oh, yes, Maxime is great, very easy to get on with. If he knows, there'll be a good explanation forthcoming.

[Maxime Ramzi]

Hi ! I don't have a lot to add to what's already been said but because I've been mentioned let me say what I can. Peter's argument is really nice - there is a proof in e.g. Johnson and McCarthy's paper that has already been mentioned that the functor Q' (aka C) is already linear before normalizing (they describe an explicit homotopy between the composite Q'(A + B) -> Q'(A) + Q'(B) -> Q'(A+B) and the identity, which is all that's really needed here - maybe the fact that this is so explicit can help for this project ? ), which I wasn't sure was true before reading this.

The end computation in terms of direct sums of Z smash A's seems to indicate though that this might not be a super easy calculation, even for A = Z (the name "dual Steenrod algebra" has already been mentioned here of course).
I guess a literature search for this complex Q' might be complicated because people have always focused on the normalized version Q, which is the one that has all the nice properties, or rather the "interesting homology".

Unfortunately I can't say much more - I studied this for my master's thesis and I think essentially all the literature I saw about this had Q' only for one or two lines before saying "now we normalize" and never mentioned it again, which I think explains why you guys have had trouble finding appropriate literature about Q' or C specifically :)

[Johan Commelin]

@Maxime Ramzi Thanks for taking the effort to create a Zulip account and write an answer!

[Peter Scholze]

Thanks Maxime! In fact the presence of this explicit homotopy on $Q'$ is the very reason $Q'=C$ came up in this stream. So yes that homotopy is definitely useful! ($Q$ on the other hand wouldn't be as useful here as the terms are not sums of $\mathbb Z[A^n]$'s.)

[Maxime Ramzi]

@Johan Commelin my pleasure :)

Actually, Peter's argument is even nicer than I thought because it might make a proof of Johnson and McCarthy's simpler ! I haven't worked out the details yet, so let me not flood this stream with an incomplete sketch of something not completely related, but it seems like the basic strategy (of linearizing each term in the complex individually) can lead to a proof that Q (so the normalized version) is just Z smash -, i.e. the linearization of Z[-] (which is essentially what Johnson and McCarthy prove in the paper that's already been mentioned here, and was the input to my paper with Geoffroy). I just have to understand a bit better how the inclusion of this shifted C(A)\oplus C(A) relates to the "degenerate chains" that you quotient out to get Q.

[Peter Scholze]

@Maxime Ramzi I actually wasn't sure how to do this, as the two notions of "degenerate chains" a priori seem a bit different. I think Johnson--McCarthy's argument essentially relies on the observation that after they mod out by degeneracies, all the higher terms in the complex actually have trivial linearization, so the linearization reduces to the contribution from degree $0$.

[Maxime Ramzi]

@Peter Scholze yes, I'm not too sure either, they are indeed (very) different. But it's slightly odd that the quotient you get of C(A) mod this shifted direct sum is exactly Q; even though the degeneracies are very different !

[Peter Scholze]

It is! I wonder whether you might simply use this other quotient instead in the stuff you are doing?

[Maxime Ramzi]

Well the original goal really was to answer a question about the Q-construction itself rather than replace it with something else that works better :D So unless there's an a priori argument why this complex is equivalent to the Q-construction, it wouldn't serve that purpose (but maybe it can serve other purposes !)

[Patrick Massot]

b) is very much a goal of this whole adventure on a large scale. What we're doing currently won't be enough of course. But there are also people in AI working on reading paper automatically and "understanding" enough to at least tell you you might be interested in that paper, although they clearly won't be to able to automatically formalize it as in the LTE project. But this is still science fiction of course.

[David Michael Roberts]

@Patrick Massot wrong topic!