9.8 for profinite S

Stream: condensed mathematics

[Johan Commelin]

I just created an issue to track this todo. From the issue page https://github.com/leanprover-community/lean-liquid/issues/73

The first paragraph of the proof reduces the claim to the case of finite S. This reduction step is not yet formalized. The finite case is done.

The challenge is to connect explicit constructions (such as fin n → M) to abstract categorical constructions (n-fold categorical product of M with itself).

After such connections are made, the rest of the proof should be straightforward applications of general facts from mathlib.

[Johan Commelin]

I've pushed the statement to src/combinatorial_lemma/profinite.lean. Anyone looking for a small and self-contained bite of applied category to work can look here.