Zulip Chat Archive
Stream: mathlib4
Topic: ContinuousMonoidHomClass etc
Yury G. Kudryashov (Jul 15 2024 at 19:10):
What do you think about migrating from docs#ContinuousMonoidHomClass to [ContinuousMapClass] + [MonoidHomClass]?
Adam Topaz (Jul 15 2024 at 19:14):
docs#ContinuousMonoidHomClass looks wrong to me... do we not want to say that multiplication is continuous?
Yury G. Kudryashov (Jul 15 2024 at 19:15):
We can assume [ContinuousMul] on the domain or codomain as needed.
Adam Topaz (Jul 15 2024 at 19:15):
Oh ok, yeah that doesn't need to be assumed
Yury G. Kudryashov (Jul 15 2024 at 19:16):
In theorems. Why would we require it in the definition? E.g., the multiplication on ENNReal isn't continuous, but we can make a ContinuousMonoidHom from NNReal to ENNReal.
Adam Topaz (Jul 15 2024 at 19:16):
no, I agree, there is no problem.
Adam Topaz (Jul 15 2024 at 19:17):
And in this case I also agree with the question of the thread (i.e. that we could just use ContinuousMapClass and MonoidHomClass)
Adam Topaz (Jul 15 2024 at 19:19):
(The docstring is wrong btw: "ContinuousMonoidHomClass F A B states that F is a type of continuous additive monoid homomorphisms.")
Yury G. Kudryashov (Jul 15 2024 at 19:44):
Do you want to open a PR?
Adam Topaz (Jul 15 2024 at 19:55):
Jireh Loreaux (Jul 16 2024 at 16:12):
I very much agree with deleting docs#ContinuousMonoidHomClass in favor of the unbundled approach.
Yury G. Kudryashov (Jul 17 2024 at 01:35):
I'll try to do this next Saturday unless someone does it earlier.
Last updated: May 02 2025 at 03:31 UTC