Zulip Chat Archive

Stream: condensed mathematics

Topic: profinite trivialities

view this post on Zulip Johan Commelin (Apr 10 2021 at 05:45):

https://github.com/leanprover-community/lean-liquid/blob/master/src/pseudo_normed_group/FiltrationPow.lean#L69 defines Pow which takes powers of profinite sets.

  • We'll need Pow_mul and Pow_mul' which give functorial isos Xmn(Xm)nXnmX^{mn} \cong (X^m)^n \cong X^{nm}.
  • Do we already have iso_of_homeomorph for Profinite?

view this post on Zulip Adam Topaz (Apr 10 2021 at 13:06):

In the cech_stuff branch, I added iso_of_bijective :wink:

Last updated: May 09 2021 at 16:20 UTC