## Stream: general

### Topic: nat smul diamond in set actions

#### Eric Wieser (Dec 07 2021 at 14:00):

docs#set.add_monoid forms a smul diamond with docs#set.has_scalar_set: 2 • {1, 2} is either {2, 4} or {2, 3, 4} depending on which instance you find

#### Yaël Dillies (Dec 07 2021 at 14:05):

I must say that pointwise smul is the one I would expect here. Can we somehow override repeated addition?

#### Yaël Dillies (Dec 07 2021 at 14:05):

A simple way would be to turn docs#set.has_scalar_set in a definition set.smul : set α → set β → set β.

#### Kevin Buzzard (Dec 07 2021 at 14:10):

Whoever had the crazy idea that 2 • X = X + X? :laughing:

#### Eric Wieser (Dec 07 2021 at 14:24):

Proof:

import algebra.pointwise

open_locale pointwise

example : (set.has_scalar_set : has_scalar ℕ (set ℕ)) ≠ (add_monoid.has_scalar_nat) :=
begin
intro h,
replace h := congr_arg (@has_scalar.smul _ _) h,
replace h := iff_of_eq (congr_arg (λ h : ℕ → set ℕ → set ℕ, 1 ∈ h 2 {0, 1}) h),
simpa [succ_nsmul, ←set.image_smul, set.image_insert_eq, ←set.image2_add] using h,
end


#### Notification Bot (Dec 07 2021 at 14:26):

This topic was moved here from #Is there code for X? > Pointwise set division by Eric Wieser

#### Anne Baanen (Dec 07 2021 at 15:34):

I don't know whether this diamond is a good illustration of why add_monoid.nsmul is a good idea, or of why it is a bad idea. It certainly illustrates that add_monoid.nsmul is an idea. :P

#### Yakov Pechersky (Dec 07 2021 at 15:37):

Maybe having pointwise binops on sets should be opt-in.

#### Yaël Dillies (Dec 07 2021 at 15:45):

As an example, I made open_locale lex switch between docs#sigma.has_le and docs#sigma.lex.has_le. I don't know whether that's the correct way, but at least it's doable.

#### Eric Wieser (Dec 07 2021 at 16:38):

Yakov Pechersky said:

Maybe having pointwise binops on sets should be opt-in.

It is opt-in, via open_locale pointwise. It just happens to be the same opt in as the scalar action, so you either have both conflicting instances or neither.

#### Yakov Pechersky (Dec 07 2021 at 16:55):

Ah, but to me, the scalar one isn't a binop between sets.

#### Eric Wieser (Dec 07 2021 at 18:39):

Well true, but open_locale pointwise is still the opt in for binop between sets you asked for, it just happens to opt into other things too.

#### Eric Wieser (Dec 07 2021 at 18:39):

More agressive would be to make the nat-action opt-in

#### Eric Wieser (Dec 07 2021 at 18:39):

Or even all the non-transitive actions

#### Reid Barton (Dec 07 2021 at 18:56):

Can't we just set instance priorities or something?

#### Eric Rodriguez (Dec 07 2021 at 19:04):

I still think assuming there's just one action/multiplication/order/whatever on a space will be quite annoying to work with in many cases :/ I wish ther was a better solution

#### Yaël Dillies (Dec 07 2021 at 19:07):

What about making the has_scalar α (set β) instance a definition?

#### Sebastien Gouezel (Dec 07 2021 at 19:15):

It's really useful, so I'd rather keep it as an instance (inside open_locale pointwise). I agree that we should just put some priorities here (and it's sufficiently uncommon that it shouldn't be an issue in general).

#### Eric Wieser (Dec 07 2021 at 20:04):

For now, perhaps I'll just add a comment to the docstring of set.add_monoid noting the diamond that appears

Last updated: Aug 03 2023 at 10:10 UTC