nat smul diamond in set actions

Stream: general

[Eric Wieser]

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]

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

[Yaël Dillies]

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

[Kevin Buzzard]

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

[Eric Wieser]

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]

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

[Anne Baanen]

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]

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

[Yaël Dillies]

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]

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]

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

[Eric Wieser]

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]

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

[Eric Wieser]

Or even all the non-transitive actions

[Reid Barton]

Can't we just set instance priorities or something?

[Eric Rodriguez]

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]

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

[Sebastien Gouezel]

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]

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