Zulip Chat Archive

Stream: maths

Topic: quotient norm group

Yury G. Kudryashov (Apr 18 2023 at 22:40):

Hi, is there any reason to override to_uniform_space in docs#add_subgroup.seminormed_add_comm_group_quotient ?

Yury G. Kudryashov (Apr 18 2023 at 22:41):

Why not use the docs#add_group_seminorm.to_seminormed_add_group constructor + default uniform_space instance coming from the norm?

Yury G. Kudryashov (Apr 18 2023 at 22:44):

It was backported from LTE in #7603 by @Patrick Massot

Patrick Massot (Apr 18 2023 at 23:14):

The answer is provided in the next five lines of this file (and the module docstring). The complicated version ensures:

example (S : add_subgroup M) : (quotient.topological_space : topological_space $ M ⧸ S) =
S.seminormed_add_comm_group_quotient.to_uniform_space.to_topological_space :=
rfl

Patrick Massot (Apr 18 2023 at 23:15):

You can delete the to_uniform_space and uniformity_dist field in that instance to see this rfl fail.

Yury G. Kudryashov (Apr 18 2023 at 23:37):

:face_palm: I should've read this before asking.

Last updated: Dec 20 2023 at 11:08 UTC