Hom(Lambda, M)

Stream: condensed mathematics

[Johan Commelin]

We have a functor PolyhedralLattice.Hom depending on a fixed polyhedral lattice $\Lambda$ and that takes $M$ to $\mathrm{Hom}(\Lambda, M)$ (i.e. group homs). It is functorial in $M$, but now we also need functoriality in $\Lambda$.
If someone wants to take on that refactor, please ping here.

[Johan Commelin]

Never mind, it's clear that my cold is making it hard for me to think clear. The thing we have is already functorial in $\Lambda$ and not in $M$. So it already behave the way we want.
I should probably crawl back in bed and wait till my brain works again :face_palm:

[Peter Scholze]

Ha! I was actually surprised, as you mentioned before that you needed an extremely large amount of functoriality for the homotopy part.