Zulip Chat Archive

Stream: maths

Topic: top mul groups


view this post on Zulip Patrick Massot (Oct 06 2018 at 10:07):

Am I blind or is the definition of multiplicative topological groups is missing in mathlib?

view this post on Zulip Patrick Massot (Oct 06 2018 at 10:07):

And nothing about topological groups uses the to_additive machine?

view this post on Zulip Kevin Buzzard (Oct 06 2018 at 10:11):

Maybe edit core Lean and redefine the notation for + to be mul?

view this post on Zulip Kevin Buzzard (Oct 06 2018 at 10:12):

You might well be right though. With groups I went through a phase of confusing group and add_group but I've never had the same confusion for topological groups.

view this post on Zulip Patrick Massot (Oct 06 2018 at 10:13):

I think I'll stick to additive group, and try to make progress on rings. Then someone will have to do a huge refactor of all this mess

view this post on Zulip Patrick Massot (Oct 06 2018 at 13:46):

Also, as I suspected, Lean doesn't want to hear that a ring quotiented by an ideal has anything to do with a add_comm_group quotiented by a subgroup. After proving addition is continuous when you quotient a commutative topological group by a subgroup, you cannot get continuity of addition when you quotient a ring by an ideal. This is a bit sad

view this post on Zulip Patrick Massot (Oct 06 2018 at 13:47):

Even after I wrote:

variables {α : Type*} [comm_ring α] {M : Type*} [module α M] (N : set α) [is_submodule N]

instance submodule_is_add_subgroup : is_add_subgroup N :=
{ zero_mem :=  is_submodule.zero,
  add_mem :=  λ a b, is_submodule.add,
  neg_mem := λ a,  is_submodule.neg}

view this post on Zulip Johan Commelin (Oct 06 2018 at 13:54):

Is that because quotients of modules is not done via quotients of add_groups?

view this post on Zulip Patrick Massot (Oct 06 2018 at 13:55):

yes

view this post on Zulip Patrick Massot (Oct 06 2018 at 13:57):

https://github.com/leanprover/mathlib/blob/master/linear_algebra/quotient_module.lean#L22
https://github.com/leanprover/mathlib/blob/master/group_theory/coset.lean#L145
No link

view this post on Zulip Johan Commelin (Oct 06 2018 at 13:59):

I've heard rumors that there are plans to fix this in mathlib 5.2

view this post on Zulip Patrick Massot (Oct 06 2018 at 14:02):

:oh_no: I try to copy-paste proofs but https://github.com/leanprover/mathlib/blob/master/linear_algebra/quotient_module.lean#L49 and https://github.com/leanprover/mathlib/blob/master/group_theory/coset.lean#L193 are not compatible :sad: :sad: :sad:

view this post on Zulip Patrick Massot (Oct 06 2018 at 14:24):

@Johannes Hölzl I just pushed https://github.com/leanprover-community/mathlib/commit/981ed82f657f49b4f276457de398b9c33af05d54 It's a mess with a lot of duplication and brute force but it should allow me to continue working on completions of topological rings. Of course I'd be grateful if you can refactor it, but I expect it would be quite a bit of work because topological_structures.lean does not use at all the to_additive machine, and module quotients are unrelated to additive group quotients.

view this post on Zulip Patrick Massot (Oct 06 2018 at 14:25):

To be clear: currently I need only the ring part of that commit (and the open map things of course) but I let the group and add_comm_group part in order to highlight the refactoring issue

view this post on Zulip Patrick Massot (Oct 06 2018 at 16:51):

And again it fails because we have multiple instances on the same type, see https://github.com/leanprover-community/mathlib/commit/125efed6aac2f44d8d466b001c655dd04ebd5fb0 I give up for today since I won't be there after dinner. @Johannes Hölzl you can have a look if you want. The issue is go back and forth between the separation quotient of a topological ring seen from the purely uniform space point of view and from the quotient ring point of view. It seems Lean doesn't accept they correspond to the same topology, although both are defeq to a quotient topology and I have a lemma stating the two setoid are equals.

view this post on Zulip Johannes Hölzl (Oct 11 2018 at 16:29):

I added a commit in lc\completions s.t. topological_structures uses to_additive (at least for topological_add_monoid and topological_add_group)

view this post on Zulip Patrick Massot (Oct 11 2018 at 18:08):

Thanks!

view this post on Zulip Patrick Massot (Oct 11 2018 at 18:08):

And thanks for working on this branch again


Last updated: May 12 2021 at 08:14 UTC