Stream: maths

Topic: open subgroups

Johan Commelin (May 20 2019 at 14:40):

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 (May 20 2019 at 14:45):

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 (May 20 2019 at 14:46):

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

Kevin Buzzard (May 20 2019 at 15:49):

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 (May 20 2019 at 15:50):

We formalised open subgroups precisely because we needed open ideals

PR'd in #1067.

Neil Strickland (May 20 2019 at 20:18):

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.

Last updated: May 14 2021 at 19:21 UTC