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.
I want to PR this to mathlib. Should I triplicate this file to also provide
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
Johan Commelin (May 20 2019 at 19:22):
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