Zulip Chat Archive
Stream: general
Topic: semi_normed_space vs normed_space
Eric Wieser (Jul 06 2021 at 19:48):
Looking at docs#semi_normed_space and docs#normed_space, I'm reminded of semimodule and module - the objects are identical, the only difference is unused typeclass arguments. Should we remove the latter and rename the former to replace it?
cc @Rémy Degenne, since you seem to be embarking on a generalization in this area.
Riccardo Brasca (Jul 06 2021 at 19:54):
I don't remember what happened with module and semimodule, but I think we really want both notions, and there are theorems that we can state for semi_normed_space that hold only for normed_space
Eric Wieser (Jul 06 2021 at 19:55):
Right, but there are no theorems which are true for [normed_group M] [normed_space R M] but not [normed_group M] [semi_normed_space R M]
Eric Wieser (Jul 06 2021 at 19:57):
Just as there are no theorems true for the old [ring R] [add_comm_group M] [module R M] but not [ring R] [add_comm_group M] [semimodule R M]
Riccardo Brasca (Jul 06 2021 at 20:00):
Ah yes, there is another layer coming from normed_group
Eric Wieser (Jul 07 2021 at 08:19):
Eric Wieser (Jan 14 2022 at 22:28):
6 months later, and CI passes in the branch :tada:!
Eric Wieser (Jan 14 2022 at 22:29):
Would have been much easier if people didn't keep proving more and more things on top of normed_spaces!
Yaël Dillies (Jan 14 2022 at 22:29):
Oh lol, I'm working on some myself right now.
Yaël Dillies (Feb 03 2022 at 09:42):
We have docs#semi_normed_add_torsor and docs#normed_add_torsor, which seems to be the exact same story. Anybody against me deleting the former?
Yaël Dillies (Feb 03 2022 at 09:45):
cc @Riccardo Brasca
Riccardo Brasca (Feb 03 2022 at 09:46):
I've never really tried to understand what normed_add_torsor means in mathlib, so I don't have any opinion, but I guess that if they're now the same thing we case delete one of them.
Yaël Dillies (Feb 03 2022 at 11:34):
Eric Wieser (Feb 03 2022 at 16:24):
Nice find, but good luck fighting CI
Yaël Dillies (Feb 03 2022 at 16:25):
I have good hope that torsors are less widely used than normed groups or modules!
Yaël Dillies (Feb 04 2022 at 20:17):
seminormed_add_torsor has been terminated :robot:
Last updated: Dec 20 2023 at 11:08 UTC