[Merged by Bors] - feat: compact subsets in products as cofiltered limits of projections

[dagurtomas]

We exhibit a compact subset in a product of totally disconnected Hausdorff spaces as a limit of its projections to finite subsets of the indexing set, in the category Profinite. The proof is structured in the same way as Profinite.isIso_asLimitCone_lift and DiscreteQuotient.exists_of_compat.

---

[dagurtomas]

I'm not sure where to put the stuff that is currently in section General in Mathlib/Topology/Category/Profinite/Product. And maybe the rest belongs in Mathlib/Topology/Category/Profinite/AsLimit?

[dagurtomas]

Also, if there is a better way to implement ProjRestrict/ProjRestricts, those suggestions are very welcome!

[joelriou]

About ProjRestrict, etc, would not it be better to redesign it (and also Proj and Set.proj) so that if we have φ : ι' → ι then there is an induced "pullback" map (∀ i, π i) → (∀ i', π (φ i)). Then, Set.proj is the direct image of a subset C by this map. (If it is not absolutely necessary, I am a little disturbed by the Inhabited instances which may seem to be a little bit artificial. If such assumptions is needed, Nonempty, which is a Prop, would presumably be better.)

[ADedecker]

I agree with Joël (I meant to comment on that a while ago but then forgot about it, I'm very sorry). Incidentally I need similar results, so #6836 is proving continuity for these "precomposition" maps (although they are not literally precompositions because of dependent types). You could also use Set.restrict for the particular case of inclusion of a set into a type, but it's probably easier to work in greater generality than with subsets!
Then, if you really need to extend by dummy values, you can probably prove a continuity result for Function.extend. Does that make sense?

[dagurtomas]

If this gets merged, then Nöbeling (#6286) is ready for review

[joelriou]

The definitions/statements in this PR looks good to me, but they do not seem to be in appropriate namespaces. The results about profinite sets should be in the Profinite namespace. I think that FinsetFunctor and precomp should be renamed and/or put in a namespace in a way which reflects the fact that this is topology; also it seems that SetFunctor would be better than FinsetFunctor.

[dagurtomas]

I moved precomp to Topology/ContinuousFunction/Basic, and put everything else in the Profinite namespace. I changed both the FinsetFunctor namespace and the name of the functor FinsetsToProfinite to Profinite.IndexFunctor, where index refers to the indexing set of the product. Does this make sense?

[dagurtomas]

Build fails because of "no space left on device"...

[ADedecker]

That happens from time to time, we've removed the affected runner for now until someone can fix the issue. I restarted the build.

[jcommelin]

Thanks 🎉

bors merge

[bors]

This PR was included in a batch that was canceled, it will be automatically retried

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style