polyhedral isos

Stream: condensed mathematics

[Johan Commelin]

thm95/polyhedral_iso.lean contains a bunch of sorrys that are proof obligations to certain canonical isomorphisms of polyhedral lattices and pseudo normed groups. Feel free to kill some of them.

[Johan Commelin]

We'll need most of those for the final bit of homotopy glue, but also for col_exact to show that we are getting some Cech cover.