Zulip Chat Archive

Stream: condensed mathematics

Topic: explicit computation


Johan Commelin (Jun 16 2021 at 06:40):

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 ={0,1}\square = \{0,1\} denote a set with two elements. Then we can consider n\square^n as a discrete cube. For every nn and every 0in0 \le i \le n and every bb \in \square we have natural maps fbn,i ⁣:nn+1f^{n,i}_b \colon \square^n \to \square^{n+1} that maps n\square^n to the (i,b)(i,b)-th face of n+1\square^{n+1}. Concretely (x1,,xn)(x_1, \dots, x_n) is mapped to (x1,,xi1,b,xi,,xn)(x_1, \dots, x_{i-1}, b, x_i, \dots, x_n).

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

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

A complex

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

dnR[An]d1R[A1]=R[A]d0R[A0]=R[A]0\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 (Jun 16 2021 at 06:44):

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

σn,i:=(f0n,i)+(f1n,i) ⁣:An+1An\sigma^{n,i} := (f^{n,i}_0)^* + (f^{n,i}_1)^* \colon A^{\square^{n+1}} \to A^{\square^n}

Now we define

dn:=i(1)i(R[(f0n,i)]+R[(f1n,i)]R[σn,i])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 AA^{\square^\bullet}.)

Johan Commelin (Jun 16 2021 at 06:45):

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 (Jun 16 2021 at 06:47):

Computational challenge

Compute the homology groups HiH_i of this complex for various RR and AA.

Johan Commelin (Jun 16 2021 at 06:48):

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

Johan Commelin (Jun 16 2021 at 06:50):

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 (Jun 16 2021 at 06:50):

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

Johan Commelin (Jun 16 2021 at 06:52):

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

Johan Commelin (Jun 16 2021 at 06:54):

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

Mario Carneiro (Jun 16 2021 at 06:55):

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

Mario Carneiro (Jun 16 2021 at 06:55):

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

Johan Commelin (Jun 16 2021 at 06:56):

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

Mario Carneiro (Jun 16 2021 at 06:56):

what does the code actually look like?

Johan Commelin (Jun 16 2021 at 06:56):

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

Johan Commelin (Jun 16 2021 at 06:56):

Let me post a gist of what I have now.

Johan Commelin (Jun 16 2021 at 06:57):

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

Mario Carneiro (Jun 16 2021 at 06:57):

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

Johan Commelin (Jun 16 2021 at 06:58):

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

Johan Commelin (Jun 16 2021 at 06:58):

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

Johan Commelin (Jun 16 2021 at 07:00):

If RR is not a field, then the structure of HiH_i can be a lot more delicate. What I'm really interested in is R=A=ZR = 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=FpR = A = \mathbb F_p for all primes pp.

Johan Commelin (Jun 16 2021 at 07:00):

And then everything is finite.

Johan Commelin (Jun 16 2021 at 07:00):

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

Johan Commelin (Jun 16 2021 at 07:02):

But computing Im(dn)\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 (Jun 16 2021 at 07:02):

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 (Jun 16 2021 at 07:06):

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

Mario Carneiro (Jun 16 2021 at 07:21):

yes

Mario Carneiro (Jun 16 2021 at 07:21):

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

Mario Carneiro (Jun 16 2021 at 07:22):

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

Johan Commelin (Jun 16 2021 at 07:23):

Sure, this stuff grows wickedly fast (-;

Johan Commelin (Jun 16 2021 at 07:24):

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

Johan Commelin (Jun 16 2021 at 07:29):

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

Riccardo Brasca (Jun 16 2021 at 07:40):

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 (Jun 16 2021 at 07:40):

On my server it crashed...

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

Johan Commelin (Jun 16 2021 at 07:41):

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

Mario Carneiro (Jun 16 2021 at 07:41):

Are the finite fields of interest primes or prime powers?

Johan Commelin (Jun 16 2021 at 07:41):

I would just go for p^1 for now.

Johan Commelin (Jun 16 2021 at 07:42):

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

Kevin Buzzard (Jun 16 2021 at 08:07):

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

Johan Commelin (Jun 16 2021 at 08:11):

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

Kevin Buzzard (Jun 16 2021 at 08:12):

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

Johan Commelin (Jun 16 2021 at 08:13):

Kevin Buzzard said:

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

thanks, I'll fix it

Johan Commelin (Jun 16 2021 at 08:14):

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

Johan Commelin (Jun 16 2021 at 08:15):

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

Kevin Buzzard (Jun 16 2021 at 08:16):

If I didn't slip up, then d0:R[A2]R[A]d_0:R[A^2]\to R[A] is the map which sends [a0,a1]A2[a_0,a_1]\in A^2 to [a0]+[a1][a0+a1][a_0]+[a_1]-[a_0+a_1] and d1:R[A2×2]R[A2]d_1:R[A^{2\times 2}]\to R[A^2] sends [a00,a01,a10,a11][a_{00},a_{01},a_{10},a_{11}] to [a00,a01]+[a10,a11][a00+a10,a01+a11][a00,a10][a01,a11]+[a00+a01,a10+a11].[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 (Jun 16 2021 at 08:17):

Yep, that looks right.

Johan Commelin (Jun 16 2021 at 08:20):

In fact, I can show that with R=A=ZR = A = \Z we get a Z2i\Z^{2^i} split subgroup in HiH_i.
The reason is that Im(d)\mathrm{Im}(d) is contained in the kernel of Qj ⁣:R[A2i]qjR[A]AQ_j \colon R[A^{2^i}] \stackrel{q_j}{\to} R[A] \to A, where qjq_j is induced by the jj-th projection A2iAA^{2^i} \to A.
But I can exhibit 2i2^i elements xkx_k of the kernel that are mapped under QjQ_j to the Kronecker delta δjk\delta_{jk}.

Johan Commelin (Jun 16 2021 at 08:21):

Those elements xkx_k are [ek][0][e_k] - [0], where eke_k is the kk-th unit vector in A2iA^{2^i}. (You can show that they are in the kernel of dd.)

Kevin Buzzard (Jun 16 2021 at 08:23):

Is this the cohomology of some topological object X(A)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 (Jun 16 2021 at 08:30):

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 (Jun 16 2021 at 08:32):

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

Johan Commelin (Jun 16 2021 at 08:33):

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

Johan Commelin (Jun 16 2021 at 08:33):

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

Riccardo Brasca (Jun 16 2021 at 08:34):

ah yes, sorry

Johan Commelin (Jun 16 2021 at 09:17):

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

Peter Scholze (Jun 16 2021 at 09:28):

Let me explain a little what's going on. So Johan built this explicit Breen--Deligne data of the form C(A):Z[A8]Z[A4]Z[A2]Z[A]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 AA is any abelian group.

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

0Hi(C(Z))AHi(C(A))Tor1(Hi1(C(Z)),A)0. 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 Tor\mathrm{Tor} is over Z\mathbb Z.) In this sense, knowledge of Hi(C(Z))H_i(C(\mathbb Z)) is (largely) enough to determine Hi(C(A))H_i(C(A)) in general. Moreover, it is known that Hi(C(Z))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 pp-power orders.

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

0Hi(C(A))RHi(C(A)R)Tor1(Hi1(C(A)),R)0. 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 AR=0A\otimes R=0, then Hi(C(A)R)=0H_i(C(A)\otimes R)=0. So in this way, when we choose R=FpR=\mathbb F_p, A=FpA=\mathbb F_p is the most reasonable choice.

Johan has proved by hand that H0(C(Z))=ZH_0(C(\mathbb Z))=\mathbb Z and H1(C(Z))=Z2H_1(C(\mathbb Z))=\mathbb Z^2, and in general that Hi(C(Z))H_i(C(\mathbb Z)) has a summand Z2i\mathbb Z^{2^i}. From his computations, it seems likely that H2(C(Z))=Z4Z/2ZH_2(C(\mathbb Z))=\mathbb Z^4\oplus \mathbb Z/2\mathbb Z.

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

h(p,i):=dim(Hi(C(Fp)Fp))=dim(Hi(C(Fp)))+dim(Hi1(C(Fp)))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(Z)C(\mathbb Z). Note that the dimension of Tor1(Hi(C(Z)),Fp)\mathrm{Tor}_1(H_i(C(\mathbb Z)),\mathbb F_p) is the number of cyclic summands of pp-power order, equivalently dim(Hi(C(Z))tor/p)\mathrm{dim}(H_i(C(\mathbb Z))_{\mathrm{tor}}/p). One formula is then

h(p,i)=dim(Hi(C(Z))/p)+dim(Hi1(C(Z))/p)+dim(Hi1(C(Z))tor/p)+dim(Hi2(C(Z))tor/p).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 (Jun 16 2021 at 09:29):

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 (Jun 16 2021 at 09:30):

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

Peter Scholze (Jun 16 2021 at 09:37):

So as an example H0(C(Z))=ZH_0(C(\mathbb Z))=\mathbb Z means that we have h(p,0)=0h(p,0)=0 for all pp, and H1(C(Z))=Z2H_1(C(\mathbb Z))=\mathbb Z^2 means h(p,1)=1+2=3h(p,1)=1+2=3 for all pp. If H2(C(Z))=Z4Z/2ZH_2(C(\mathbb Z))=\mathbb Z^4\oplus \mathbb Z/2\mathbb Z, then h(2,2)=5+2=7h(2,2)=5+2=7 while we should have h(p,2)=4+2=6h(p,2)=4+2=6 for all p>2p>2.

Johan Commelin (Jun 16 2021 at 09:38):

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

Peter Scholze (Jun 16 2021 at 09:40):

I would expect that H3(C(Z))H_3(C(\mathbb Z)) has no 33-torsion; in general I would expect pp-torsion to appear only from degree 2p22p-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 H3(C(Z))=Z8(torsion)H_3(C(\mathbb Z))=\mathbb Z^8 \oplus (\mathrm{torsion}) (so that Johan's split Z2i\mathbb Z^{2^i} is the correct answer at least modulo torsion), and that there is no 33-torsion, then we should hope that h(3,3)=8+4=12h(3,3)=8+4=12.

Peter Scholze (Jun 16 2021 at 09:40):

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

Peter Scholze (Jun 16 2021 at 09:42):

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

Johan Commelin (Jun 16 2021 at 09:47):

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

Riccardo Brasca (Jun 16 2021 at 09:48):

Anyway I confirm that the problem is the memory

Peter Scholze (Jun 16 2021 at 09:48):

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

Peter Scholze (Jun 16 2021 at 09:50):

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

Chris Birkbeck (Jun 16 2021 at 10:53):

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 (Jun 16 2021 at 10:55):

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

Johan Commelin (Jun 16 2021 at 11:30):

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

Johan Commelin (Jun 16 2021 at 11:30):

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

Chris Birkbeck (Jun 16 2021 at 11:32):

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

Peter Scholze (Jun 16 2021 at 11:35):

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

Peter Scholze (Jun 16 2021 at 11:36):

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

Chris Birkbeck (Jun 16 2021 at 11:37):

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

Chris Birkbeck (Jun 16 2021 at 11:37):

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

Johan Commelin (Jun 16 2021 at 11:41):

Ooh, that's a really nice observation!

Peter Scholze (Jun 16 2021 at 11:42):

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

Peter Scholze (Jun 16 2021 at 11:44):

I gather this is about some 6553665536-dimensional space?

Riccardo Brasca (Jun 16 2021 at 11:45):

@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 (Jun 16 2021 at 11:50):

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

Peter Scholze (Jun 16 2021 at 11:53):

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

Peter Scholze (Jun 16 2021 at 11:54):

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

Johan Commelin (Jun 16 2021 at 12:10):

Peter Scholze said:

I gather this is about some 6553665536-dimensional space?

Right, so an exhaustive search has to treat 4294967296 vectors

Chris Birkbeck (Jun 16 2021 at 12:14):

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 (Jun 16 2021 at 12:16):

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

Peter Scholze (Jun 16 2021 at 12:16):

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

Johan Commelin (Jun 16 2021 at 12:17):

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 (Jun 16 2021 at 12:17):

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 (Jun 16 2021 at 12:18):

@Johan Commelin Oh that sounds much better!

Peter Scholze (Jun 16 2021 at 12:36):

Ah! A general comment is that C(A)C(A) admits C(A)2[1]C(A)^{\oplus 2}[-1] as a direct summand (functorially in AA). 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 11 cubes. Let C(A)\overline{C}(A) be the complementary direct summand.

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

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

Mario Carneiro (Jun 16 2021 at 12:37):

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

Peter Scholze (Jun 16 2021 at 12:38):

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

Johan Commelin (Jun 16 2021 at 12:38):

I'll start running the rust code on my server

Johan Commelin (Jun 16 2021 at 12:39):

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

Mario Carneiro (Jun 16 2021 at 12:39):

If the rust program reaches 6530533=6527265305 - 33 = 65272 then you win

Peter Scholze (Jun 16 2021 at 12:39):

The same :smile:

Peter Scholze (Jun 16 2021 at 12:39):

I'd have to check what is in degree 44...

Mario Carneiro (Jun 16 2021 at 12:40):

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

Peter Scholze (Jun 16 2021 at 12:40):

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

Peter Scholze (Jun 16 2021 at 12:42):

Wait, let me think for a moment

Peter Scholze (Jun 16 2021 at 12:46):

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

Johan Commelin (Jun 16 2021 at 12:59):

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

Johan Commelin (Jun 16 2021 at 12:59):

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

Johan Commelin (Jun 16 2021 at 13:09):

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

Alex J. Best (Jun 16 2021 at 13:10):

What is the bottleneck for the current implementation?

Johan Commelin (Jun 16 2021 at 13:10):

My guess: Gaussian elimination

Johan Commelin (Jun 16 2021 at 13:10):

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 (Jun 16 2021 at 13:13):

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 (Jun 16 2021 at 13:13):

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

Johan Commelin (Jun 16 2021 at 13:14):

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

Chris Birkbeck (Jun 16 2021 at 13:14):

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

Peter Scholze (Jun 16 2021 at 13:14):

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

Johan Commelin (Jun 16 2021 at 13:15):

Mario just implemented Gauss from scratch

Johan Commelin (Jun 16 2021 at 13:15):

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

Johan Commelin (Jun 16 2021 at 13:15):

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 (Jun 16 2021 at 13:20):

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

Johan Commelin (Jun 16 2021 at 13:21):

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

Peter Scholze (Jun 16 2021 at 13:23):

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

Peter Scholze (Jun 16 2021 at 13:23):

Or wait

Peter Scholze (Jun 16 2021 at 13:23):

I mean we want to compute the image of did_i

Peter Scholze (Jun 16 2021 at 13:24):

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

Johan Commelin (Jun 16 2021 at 13:24):

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

Peter Scholze (Jun 16 2021 at 13:24):

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

Peter Scholze (Jun 16 2021 at 13:24):

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

Peter Scholze (Jun 16 2021 at 13:25):

This way, you only do Gaussian elimination against one vector

Johan Commelin (Jun 16 2021 at 13:25):

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

Peter Scholze (Jun 16 2021 at 13:26):

Hmm, it should always be tiny I think

Johan Commelin (Jun 16 2021 at 13:26):

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

Peter Scholze (Jun 16 2021 at 13:27):

Yes

Johan Commelin (Jun 16 2021 at 13:27):

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

Peter Scholze (Jun 16 2021 at 13:27):

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

Johan Commelin (Jun 16 2021 at 13:27):

Right, so that isn't worth it.

Johan Commelin (Jun 16 2021 at 13:28):

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

Johan Commelin (Jun 16 2021 at 13:28):

(We're at 18420 vectors now.)

Johan Commelin (Jun 16 2021 at 13:30):

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

Peter Scholze (Jun 16 2021 at 13:31):

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

Johan Commelin (Jun 16 2021 at 13:32):

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 (Jun 16 2021 at 13:33):

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

Johan Commelin (Jun 16 2021 at 13:39):

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

Johan Commelin (Jun 16 2021 at 13:40):

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

Chris Birkbeck (Jun 16 2021 at 14:16):

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 (Jun 16 2021 at 14:16):

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 (Jun 16 2021 at 14:18):

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

Chris Birkbeck (Jun 16 2021 at 14:18):

Aha I see.

Johan Commelin (Jun 16 2021 at 14:19):

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 (Jun 16 2021 at 14:19):

Yeah thats what I was thinking

Johan Commelin (Jun 16 2021 at 14:19):

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 (Jun 16 2021 at 14:20):

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

Chris Birkbeck (Jun 16 2021 at 14:20):

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 (Jun 16 2021 at 14:22):

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

Johan Commelin (Jun 16 2021 at 14:23):

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

Johan Commelin (Jun 16 2021 at 14:23):

Also, you need rust version > 1.50

Johan Commelin (Jun 16 2021 at 14:26):

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

Johan Commelin (Jun 16 2021 at 14:26):

That should be blazingly fast.

Johan Commelin (Jun 16 2021 at 14:27):

@Mario Carneiro Does that make sense?

Mario Carneiro (Jun 16 2021 at 14:27):

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

Peter Scholze (Jun 16 2021 at 14:28):

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

Chris Birkbeck (Jun 16 2021 at 14:28):

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

Mario Carneiro (Jun 16 2021 at 14:32):

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 (Jun 16 2021 at 14:33):

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

Johan Commelin (Jun 16 2021 at 14:33):

Zp::add would just be xor

Johan Commelin (Jun 16 2021 at 14:33):

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

Peter Scholze (Jun 16 2021 at 14:35):

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 (Jun 16 2021 at 14:38):

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 (Jun 16 2021 at 14:39):

Oh yes

Mario Carneiro (Jun 16 2021 at 14:39):

it was spending 97% of its time in insert

Johan Commelin (Jun 16 2021 at 14:40):

Wow! It hit 10.000 in 10s!

Mario Carneiro (Jun 16 2021 at 14:40):

now that's down to 0.38%

Mario Carneiro (Jun 16 2021 at 14:41):

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

Mario Carneiro (Jun 16 2021 at 14:41):

this is for sure optimized to a bit mask

Mario Carneiro (Jun 16 2021 at 14:41):

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

Johan Commelin (Jun 16 2021 at 14:43):

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

Johan Commelin (Jun 16 2021 at 14:44):

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

Peter Scholze (Jun 16 2021 at 14:45):

(So yes, at all primes the formula is

Z(p)SZ(p)i1LZ(p)[xi]/(pxi)\mathbb Z_{(p)}\otimes_{\mathbb S} \mathbb Z_{(p)}\cong \bigotimes^L_{i\geq 1} \mathbb Z_{(p)}[x_i]/(px_i)

where xix_i has degree 2pi22p^i - 2.)

Johan Commelin (Jun 16 2021 at 14:46):

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

Johan Commelin (Jun 16 2021 at 14:48):

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 (Jun 16 2021 at 14:51):

(11 minutes: 16000 vectors)

Johan Commelin (Jun 16 2021 at 15:10):

30 minutes: 18500 vectors

Peter Scholze (Jun 16 2021 at 15:11):

OK, this doesn't look good

Riccardo Brasca (Jun 16 2021 at 15:16):

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

Mario Carneiro (Jun 16 2021 at 15:19):

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 (Jun 16 2021 at 15:41):

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 (Jun 16 2021 at 15:45):

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

Mario Carneiro (Jun 16 2021 at 15:46):

not bool, but (x + y) & 1

Johan Commelin (Jun 16 2021 at 15:46):

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 (Jun 16 2021 at 15:47):

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 216×2162^{16} \times 2^{16} matrix that is initialized to 0.

Johan Commelin (Jun 16 2021 at 15:49):

Mario Carneiro said:

not bool, but (x + y) & 1

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

Mario Carneiro (Jun 16 2021 at 15:56):

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 (Jun 16 2021 at 15:57):

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

Johan Commelin (Jun 16 2021 at 15:58):

41s, 15.000 vectors

Johan Commelin (Jun 16 2021 at 15:59):

I think my cores are not so fast (-;

Mario Carneiro (Jun 16 2021 at 15:59):

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

Johan Commelin (Jun 16 2021 at 16:00):

2min, 16400

Johan Commelin (Jun 16 2021 at 16:01):

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 (Jun 16 2021 at 16:02):

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 (Jun 16 2021 at 16:03):

But maybe that doesn't actually help so much

Johan Commelin (Jun 16 2021 at 16:04):

6min, 18500

Johan Commelin (Jun 16 2021 at 16:07):

10min, 20000

Johan Commelin (Jun 16 2021 at 16:22):

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

Riccardo Brasca (Jun 16 2021 at 16:22):

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

Chris Birkbeck (Jun 16 2021 at 16:22):

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

Johan Commelin (Jun 16 2021 at 16:24):

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

Johan Commelin (Jun 16 2021 at 16:24):

I'm now at 26:30 and 24000 vectors

Johan Commelin (Jun 16 2021 at 17:25):

1h27, 32600

Johan Commelin (Jun 16 2021 at 17:26):

It's still finding >1 vector per second.

Riccardo Brasca (Jun 16 2021 at 17:27):

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

Matthew Ballard (Jun 16 2021 at 18:09):

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

Riccardo Brasca (Jun 16 2021 at 18:13):

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 (Jun 16 2021 at 18:15):

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 (Jun 16 2021 at 18:15):

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

Matthew Ballard (Jun 16 2021 at 18:18):

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

Riccardo Brasca (Jun 16 2021 at 18:19):

This question is like Chinese for me :rolling_on_the_floor_laughing:

Matthew Ballard (Jun 16 2021 at 18:21):

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

Riccardo Brasca (Jun 16 2021 at 18:23):

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

Matthew Ballard (Jun 16 2021 at 18:36):

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

Matthew Ballard (Jun 16 2021 at 19:31):

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 (Jun 16 2021 at 20:29):

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

Johan Commelin (Jun 16 2021 at 20:29):

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 (Jun 16 2021 at 20:55):

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 (Jun 16 2021 at 20:56):

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

Riccardo Brasca (Jun 16 2021 at 21:33):

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

Riccardo Brasca (Jun 16 2021 at 21:33):

It is like that since one minute

Riccardo Brasca (Jun 16 2021 at 21:37):

Same on the other machine, it arrived to 65271.

Chris Birkbeck (Jun 16 2021 at 21:54):

Oh amazing! I think you got it!

Chris Birkbeck (Jun 16 2021 at 21:56):

Oh wait, wasnt it 65272 that we expected? hmm

Riccardo Brasca (Jun 16 2021 at 21:56):

Maybe the script started at 0 instead of 1?

Riccardo Brasca (Jun 16 2021 at 21:57):

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

Yaël Dillies (Jun 16 2021 at 22:01):

Riccardo Brasca said:

Maybe the script started at 0 instead of 1?

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

Chris Birkbeck (Jun 16 2021 at 22:07):

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 (Jun 16 2021 at 22:23):

Unfortunately nobody bet against me, I believe?

Johan Commelin (Jun 17 2021 at 02:10):

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

Mathieu Guay-Paquet (Jun 17 2021 at 02:33):

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

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

(x1,,xn)(1x1,,1xn)(x_1, \ldots, x_n) \mapsto (1-x_1, \ldots, 1-x_n),

and this (family of) maps commutes with the differential dnd_n, in the sense that dnR[(Fn)]=R[(Fn+1)]dnd_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[An]R[A^{\square^n}] into a (+1)(+1)-eigenspace and a (1)(-1)-eigenspace for FnF_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 (31638)/2=21520080(3^{16}-3^8)/2 = 21520080 vectors into a (3834)/2=3240(3^8-3^4)/2 = 3240 dimensional space, and the image of (316+38)/2=21526641(3^{16}+3^8)/2 = 21526641 vectors into a (38+34)/2=3321(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[An]R[A^{\square^n}], and the differential dnd_n commutes with these group actions, so we can use some representation theory to cut down the computation by a lot. For p2p \neq 2, I'm seeing a group action of an abelian group with 2×2×(p1)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 (Jun 17 2021 at 04:55):

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 (Jun 17 2021 at 05:26):

Well, I'm convinced already now that the answer is that C(Z)\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 (Jun 17 2021 at 08:01):

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

David Michael Roberts (Jun 17 2021 at 09:45):

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 (Jun 17 2021 at 10:12):

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

Johan Commelin (Jun 17 2021 at 10:13):

The script doesn't save the preimages, certainly.

Johan Commelin (Jun 17 2021 at 10:53):

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

Johan Commelin (Jun 17 2021 at 10:53):

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 (Jun 17 2021 at 10:54):

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 (Jun 17 2021 at 10:56):

Very close to 1

David Michael Roberts (Jun 17 2021 at 11:00):

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 (Jun 17 2021 at 11:06):

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

Peter Scholze (Jun 17 2021 at 12:18):

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 (Jun 17 2021 at 12:22):

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

Mario Carneiro (Jun 17 2021 at 12:29):

I don't think the computation that was run for h(2, 4) is even an informal proof. We have a lower bound of 3333 and the random guessing approach yields an upper bound of 3434, 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 3434 is 21002^{-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 (Jun 17 2021 at 12:35):

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 (Jun 17 2021 at 12:40):

@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 (Jun 17 2021 at 12:41):

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 (Jun 17 2021 at 12:42):

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

Adam Topaz (Jun 17 2021 at 12:42):

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

Riccardo Brasca (Jun 17 2021 at 12:43):

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

David Michael Roberts (Jun 17 2021 at 12:44):

@Riccardo Brasca ah, do share it!

David Michael Roberts (Jun 17 2021 at 12:48):

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 (Jun 17 2021 at 12:49):

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

Peter Scholze (Jun 17 2021 at 12:53):

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 (Jun 17 2021 at 13:03):

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 (Jun 17 2021 at 13:05):

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 (Jun 17 2021 at 13:09):

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 (Jun 17 2021 at 13:18):

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 (Jun 17 2021 at 13:20):

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 C(Z)\overline{C}(\mathbb Z) above may still be open

Peter Scholze (Jun 17 2021 at 13:20):

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

Peter Scholze (Jun 17 2021 at 13:21):

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

Peter Scholze (Jun 17 2021 at 13:32):

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

Peter Scholze (Jun 17 2021 at 13:32):

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

Peter Scholze (Jun 17 2021 at 13:39):

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

Johan Commelin (Jun 17 2021 at 13:43):

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

Johan Commelin (Jun 17 2021 at 13:43):

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

David Michael Roberts (Jun 17 2021 at 13:44):

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

Peter Scholze (Jun 17 2021 at 13:48):

Using all the jargon: The linearization of the functor AZ[A]A\mapsto \mathbb Z[A] is the functor AZSAA\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)C(A) can be computed by a complex of the form

C(A)lin:ZSA4ZSA2ZSA0,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)C(A) is already linear in AA, so this complex is quasi-isomorphic to C(A)C(A).

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

[ZSA4ZSA200][ZSA4ZSA2ZSA0][\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 ZSA\mathbb Z\otimes_{\mathbb S} A. But this maps naturally into the linearization of C(A)C(A), so we get a splitting

C(A)linC(A)2[1]linZSA.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)C(A)linC(A)\to C(A)^{\mathrm{lin}}. So the upshot is that there is a natural quasi-isomorphism

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

i.e.

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

by telescoping.

Johan Commelin (Jun 17 2021 at 13:56):

So the claim that C(A)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 (Jun 17 2021 at 13:56):

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

Johan Commelin (Jun 17 2021 at 13:57):

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

Peter Scholze (Jun 17 2021 at 13:59):

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(Z)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 (Jun 17 2021 at 14:01):

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 (Jun 17 2021 at 14:05):

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

Maxime Ramzi (Jun 17 2021 at 16:37):

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 (Jun 17 2021 at 16:54):

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

Peter Scholze (Jun 17 2021 at 19:06):

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

Maxime Ramzi (Jun 17 2021 at 19:51):

@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 (Jun 17 2021 at 20:46):

@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 00.

Maxime Ramzi (Jun 17 2021 at 20:52):

@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 (Jun 17 2021 at 20:53):

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

Maxime Ramzi (Jun 17 2021 at 21:03):

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 (Jun 17 2021 at 21:03):

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 (Jun 17 2021 at 23:05):

@Patrick Massot wrong topic!


Last updated: Dec 20 2023 at 11:08 UTC