profinite trivialities

Stream: condensed mathematics

[Johan Commelin]

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 $X^{mn} \cong (X^m)^n \cong X^{nm}$.
• Do we already have iso_of_homeomorph for Profinite?

[Adam Topaz]

In the cech_stuff branch, I added iso_of_bijective :wink:

[Filippo A. E. Nuccio]

I am trying to prove that a certain set is open in the space of bounded Laurent measures. If I look at these as a "honest" inverse limit, I know how to do, because my set is a product of some subsets of finitely many components, and then the whole component elsewhere, using docs#topological_space.is_topological_basis.is_open_iff . I also get that the topology on the bounded Laurent measures is induced from that on the limit cone (the two types are equivalent), and I wonder if there is a painless way to describe this limit cone as a subtype of the Pi type.

[Johan Commelin]

There is a homeomorphism between the two. I'm not near Lean right now, but it should be somewhere close to the definition of the topology.

[Filippo A. E. Nuccio]

Well, I can find laurent_measures_bdd_homeo { F : ℒ S | ∥F∥₊ ≤ c } ≃ₜ (Profinite.limit_cone (laurent_measures_bdd_functor r S c ⋙ Fintype.to_Profinite)).X, is it the one you are referring to?

[Filippo A. E. Nuccio]

This is actually not very useful, I think: it is basically tautological, because the topology on laurent measures is defined as the topology on the limit cone.

[Adam Topaz]

@Filippo A. E. Nuccio Are you working with a subset of one of the filtered pieces of Laurent measures? I suppose so, because otherwise there is no topology!

[Filippo A. E. Nuccio]

Yes, indeed.

[Adam Topaz]

Note that Profinite.limit_cone is defeq to the "usual" limit, i.e. as a closed subset of the pi type

[Filippo A. E. Nuccio]

Really defeq?!

[Adam Topaz]

Yeah, it should be

[Adam Topaz]

https://github.com/leanprover-community/mathlib/blob/631890bf90e76818b80c57c00291380c0329143d/src/topology/category/Profinite/default.lean#L161

[Filippo A. E. Nuccio]

Wow, so I can blindly apply your result on the basis of the topology of a Pi.top space and get somewhere? I did not even dare trying... :smiling_face:

[Filippo A. E. Nuccio]

Adam Topaz said:

https://github.com/leanprover-community/mathlib/blob/631890bf90e76818b80c57c00291380c0329143d/src/topology/category/Profinite/default.lean#L161

Oh nice!

[Filippo A. E. Nuccio]

Thanks

[Adam Topaz]

well, first you apply ssome lemma about the induced topology

[Filippo A. E. Nuccio]

Yes yes, this I thought.

[Adam Topaz]

since you need to pass from the subspace to the ambient pi type

[Adam Topaz]

It all boils down to the following construction
https://github.com/leanprover-community/mathlib/blob/631890bf90e76818b80c57c00291380c0329143d/src/topology/category/Top/limits.lean#L40

[Filippo A. E. Nuccio]

OK, I will try but it seems easy, thanks.

[Adam Topaz]

If you want, there is also docs#Top.limit_cone_infi which you can use in conjunction with the fact that Profinite_to_Top preserves limits to obtain a description of the limit Profinite set as the infimum of topologies. IIRC I also proved some lemma (in mathlib?) describing a basis for the topology of an infimum of topologies.

[Adam Topaz]

docs#is_topological_basis_infi

[Filippo A. E. Nuccio]

Thanks, I think the lemmas about explicit Pi topologies (rather than general infi ones) should be enough, but if not I'll try these.

[Kevin Buzzard]

Filippo -- if you're talking about what I think you're talking about, then maybe it's enough to observe that the profinite thing you have is defined as a limit, so there will be map to one of the factors (all of which are finite), and this map will be known to be continuous, and then you can take the preimage of a point in the factor and this will be open.

[Filippo A. E. Nuccio]

Oh, very good point Kevin. I am indeed talking about what I think you think I am talking about... :sweat_smile:

[Filippo A. E. Nuccio]

I am grabbing this option to dwell a bit into the category_theory library, and construction of limits, but I will probably take your approach soon.

[Filippo A. E. Nuccio]

Thanks.