## Stream: maths

### Topic: top mul groups

#### Patrick Massot (Oct 06 2018 at 10:07):

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

#### Patrick Massot (Oct 06 2018 at 10:07):

And nothing about topological groups uses the to_additive machine?

#### Kevin Buzzard (Oct 06 2018 at 10:11):

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

#### 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.

#### 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

#### 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

#### 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]

{ zero_mem :=  is_submodule.zero,
neg_mem := λ a,  is_submodule.neg}


#### Johan Commelin (Oct 06 2018 at 13:54):

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

yes

#### Johan Commelin (Oct 06 2018 at 13:59):

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

#### 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.

#### 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

#### 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.

#### 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)

Thanks!

#### 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