Zulip Chat Archive
Stream: Is there code for X?
Topic: Abstracting * and /
Yaël Dillies (Dec 27 2021 at 10:39):
Do we have a typeclass for binary operations f : α → β → γ such that ∀ a b c d, f (a * b) (c * d) = f a c * f b d? This is respected for * and / for example.
Johan Commelin (Dec 27 2021 at 12:05):
No, I'm quite certain we don't have that. Especially if you want f : α → β → γ to be heterogeneous, instead of α = β = γ.
Yaël Dillies (Dec 27 2021 at 12:10):
It's like a binary mul_hom, but that's not the same as α →* β →* γ.
Eric Wieser (Dec 27 2021 at 13:22):
Is it the same as α × β →* γ?
Eric Wieser (Dec 27 2021 at 13:22):
It looks like it
Yaël Dillies (Dec 27 2021 at 13:24):
Oh yes probably. Do you want me to use that in #10907?
Eric Wieser (Dec 27 2021 at 13:28):
Your m.prod_hom₂ seems reasonable to keep, but it would be neat to prove it using maps from ×
Yaël Dillies (Dec 27 2021 at 13:29):
Do you mean changing the statement, or changing the proof? Because the proof is about as short as it can be.
Eric Wieser (Dec 27 2021 at 13:49):
I meant the proof, mainly to see if any machinery elsewhere is missing
Yaël Dillies (Dec 27 2021 at 13:54):
What's missing is * and / bundled as α × α →* α, but that's for the specific uses of prod_hom₂. I can't see how to shorten prod_hom₂ itself, because you need to build the mul_hom on the fly.
Eric Wieser (Dec 27 2021 at 14:09):
I was just about to say, it would be great to have those bundled homs
Eric Wieser (Dec 27 2021 at 14:13):
I assume there's also a version of α × β →* β that's true for smul
Yaël Dillies (Dec 27 2021 at 14:14):
I'm making all of them right now!
Yaël Dillies (Dec 27 2021 at 14:21):
Btw there's also the α × α →*₀ α version.
Yaël Dillies (Dec 27 2021 at 14:22):
which feels like it can be strengthened, because we not only have 0 / 0 = 0, but also a / 0 = 0 and 0 / a = 0
Kyle Miller (Dec 27 2021 at 14:33):
Johan Commelin said:
No, I'm quite certain we don't have that. Especially if you want
f : α → β → γto be heterogeneous, instead ofα = β = γ.
Core Lean only seems to have the homogeneous version: docs#is_left_distrib
I've got the impression that these typeclasses tend not to be used since the field name must be the generic one (like left_distrib), which isn't so nice if you want to extend the same typeclass multiple times for multiple operators.
Yaël Dillies (Dec 27 2021 at 14:35):
I think they tend not to be used because we switched to bundled homs. docs#is_mul_hom is pretty close in essence.
Yaël Dillies (Dec 27 2021 at 15:23):
Okay, I got them all I think. Where should they go?
Eric Wieser (Dec 27 2021 at 19:53):
Next to docs#add_monoid_hom.mul?
Yaël Dillies (Jan 05 2022 at 19:27):
Putting it in algebra.group.hom_instances is not quite nice, because nothing imports that.
Eric Wieser (Jan 06 2022 at 14:00):
Where you have them in prod seems fine
Last updated: Dec 20 2023 at 11:08 UTC