Locally compact groups

Stream: condensed mathematics

[Patrick Massot]

This is not a question directly about the Lean version, more about consequences of Johan's effort. Do we know whether Johan's version of the Breen-Deligne resolution is enough to prove Theorem 4.3 in Lectures on Condensed Mathematics? This the theorem computing RHom from tori to discrete groups or reals. Is this documented anywhere?

[Johan Commelin]

I'm pretty sure that the proof of 4.3.(ii) will "just work". The spectral sequence argument for 4.3.(i) will hopefully be fine as well. But I didn't check carefully yet.
Unfortunately, the whole Breen--Deligne variant is not documented anywhere outside of our Zulip discussions. This should change in the next few months.