open subgroups

Stream: maths

[Johan Commelin]

In the perfectoid project, we have a 250 lines long file about open_subgroups G: the type of open subgroups of a topological group.
https://github.com/leanprover-community/lean-perfectoid-spaces/blob/master/src/for_mathlib/nonarchimedean/open_subgroup.lean

I want to PR this to mathlib. Should I triplicate this file to also provide open_submonoids, open_subrings? There will be all sorts of order preserving maps and galois insertions all over the place. Is that the right approach? Or do we need something a bit more meta?

[Neil Strickland]

I don't remember ever seeing a use for open submonoids that are not subgroups. Open ideals come up all the time, but open subrings seem less common.

[Johan Commelin]

Ok, so maybe we should just PR this as is... and then later someone can pile open ideals on top of this.

[Kevin Buzzard]

I do wonder exactly what we needed from open ideals which didn't just come straight from open subgroups. I feel like this might be a bit like the units of a ring. I was surprised when I couldn't find units of a ring and then realised we had units of a monoid. Then I thought "yeah but I need things like units of a ring are a group" and then I realised that units of a monoid are a group.

[Kevin Buzzard]

We formalised open subgroups precisely because we needed open ideals

[Johan Commelin]

PR'd in #1067.

[Neil Strickland]

Along the same lines: we currently have a default notion of divisibility for semirings, but most of it works fine for monoids (e.g. pnat) and it should really be refactored to cover that.