Implementing more features in Order.PFilter (ultraness, etc)

Stream: mathlib4

[Emilie (Shad Amethyst)]

Context: I've been working on a proof of Rubin's theorem, and have now managed to formalize it in Lean (https://github.com/adri326/rubin-lean4/ - the code is extremely messy as of now). In the last steps of the proof, I first tried using ultrafilters (which from what I could find are the only constructions in mathlib that guarantee that ClusterPt p F <-> F ≤ nhds p), which worked well for as long as I was working within the topology, but those broke as soon as I tried to use them outside of the topology, as I only had a map from the topological basis of the topology to a purely group-theoretic construction, made up of subgroups.
In the end, I constructed an ad-hoc version of ultrafilters designed around my usecase, which requires that every set in the filter implies it is a superset of an element of the topological basis also contained in the filter (∀ (S : Set α), S ∈ F → ∃ T ∈ F, T ∈ B ∧ T ⊆ S), and managed to implement my own version of Ultrafilter.of, which was enough for what I needed.

I now would like to work towards getting this proof of Rubin's theorem into Mathlib, and this means taking all of what I've written, and seeing if there isn't a close enough construct in mathlib already that I could use instead, so as to not introduce duplications in my pull requests.
I'm now realizing that my own version of "ultrafilters in a basis" is really just an Order.PFilter that is ultra. However, I'm not seeing any formalization of PFilter.IsUltra (as opposed to Ideal.IsMaximal), and there isn't a way to construct an Ideal.IsMaximal that is greater than a given Ideal.

So I would like to know if there is interest in me contributing to implement things like Idea.IsMaximal.of (I : Ideal α), PFilter.IsUltra, PFilter.IsUltra.of (F : PFilter α).
Additionally, I would like to know if this is something that is something that is reachable for someone like me who only has the equivalent of a bachelor's level of mathematics (given that my studies have been more around computer science).

On top of that, I would also like to map between PFilters and regular Filters, and have the theorem that if the lattice maps to a topological basis, where the infimum maps to set intersection, the order is preserved and the map is surjective, then if the resulting filter has a cluster point, it will also be smaller than the neighborhood filter of that point.
This is something I proved for my "ultrafilters in a basis", but I don't know how general this statement can be made outside of my narrow use-case, and I fear that I might either prove a weaker statement than what is possible, or struggle for a while in trying to prove a statement that is too strong.

Lastly, I worry that my proof style might be too tactic-y, as I see that a lot of proofs in mathlib have been heavily golfed.

I think I will make my first contribution on proving a few simple group-theoretic things, like g • x = x → g^z • x = x(a corollary of MulAction.zpow_smul_eq_iff_minimalPeriod_dvd), and regular open sets (sets S such that interior (closure S) = S).

I'm open to hearing your opinion on what I'm suggesting, and whether I might have missed an already-existing proof of some of the things that I'm planning to contribute to mathlib.

[Emilie (Shad Amethyst)]

I see now that @Yaël Dillies mentionned wanting to re-implement PFilter and Ideal from scratch a few weeks ago; I wouldn't mind helping with that, as long as I'm not doing this alone :)

[Oliver Nash]

Congratulations on completing this project. It's great that you now wish to PR this material to Mathlib.

I didn't quite follow your explanation of why you need to use docs#Order.PFilter but I expect this will become clearer in due course, e.g., during PR review. The only advice I'd offer for now is that it's a good idea to keep PRs short and that new definitions are harder to get right than new lemmas.

Good luck!

[Emilie (Shad Amethyst)]

PFilters would allow me to carry the ultra-ness of filters in the topological space α to filters made up of subgroups in G, allowing me to map to/from filters that are finer than the neighborhood filter of a point p. Right now I'm using regular filters, and it has its downsides, since the bottom element of subgroups isn't empty, and this translated to me needing to rely on properties of the topological basis in α to prove that my basis that is purely constructed from G is a topological basis.

[Yaël Dillies]

Yes, I do want to redo everything from scratch (and I doubt it would be a good learning experience to try helping here, since I have very clear views on how to do it), but sadly I severely ran out of Lean time for those holidays :sad: