Zulip Chat Archive

Stream: maths

Topic: open subgroups


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (May 20 2019 at 15:50):

We formalised open subgroups precisely because we needed open ideals

view this post on Zulip Johan Commelin (May 20 2019 at 19:22):

PR'd in #1067.

view this post on Zulip 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