16:40
@AkhilMathew It depends which spectrum you're working over, but my understanding is that you guys were discussing MU.
(sorry, @JonBeardsley too)
Say you have a "descent diagram": (homotopy) coCartesian section of modules over the cosimplicial diagram {MU --> MU^MU ---> MU^MU^MU ---->...}, call it {M^0 --> M^1 ---> M^2 ----> ...}.
Suppose M^0 is a perfect MU-module, so that it's a candidate for being MU ^ X for some finite complex X.
Let X = Tot {M^0 --> M^1 ---> ...}. I claim that smashing X with {MU --> MU ^ MU ---> ...} recovers our cosimplicial object.
The main components that make this go are the following:
(1) Because MU ^ MU -> MU is 2-connected, the Tot-diagram has a pretty large "vanishing line" in the sense that the fiber of Tot^n -> Tot^{n-1} has connectivity that grows linearly in n.
(2) Next, because MU, M^0, and hence all the M^i are of finite type, so is X.
Together these tell me that smashing with MU moves inside Tot.
Sorry, I have lost the remaining thread of the argument for now -- it is roughly the same as showing essential surjectivity for faithfully flat descent.
I believe that after smashing with MU, it becomes a module over the augmented cosimplicial diagram of rings {MU -> MU^MU --> MU^MU^MU --->}, which is degenerate; this is equivalent data to simply having an MU-module.
Serves me right for trying to do this on the fly. I can try to come back and fix this later tonight if anybody is actually interested.
The last step is observing that, because MU ^ X ~= M^0 is a perfect MU-module, HZ ^ X ~= HZ ^_{MU} M^0 is a perfect HZ-module, which is true iff X is equivalent to a finite complex.
