Diamond in docs#pi.has_scalar'

Stream: general

[Eric Wieser]

The definition of docs#pi.has_scalar' (and the stronger smul-typeclass friends) forms a non-equal diamond with docs#pi.has_scalar when trying to find has_scalar (α → β) (α → (α → β)); for example:

import algebra.module.pi

variables {α β : Type*}

-- should these just be global?
attribute [ext] distrib_mul_action mul_action has_scalar

example [has_mul β] :
  (@pi.has_scalar' _ _ _ (λ _, infer_instance) : has_scalar (α → β) (α → (α → β)))
    = @pi.has_scalar _ _ _ (λ _, infer_instance) :=
begin
  ext fab faab a₁ a₂,
  dsimp at *,
  sorry -- `fab a₁ * faab a₁ a₂ = fab a₂ * faab a₁ a₂` is not true in general!
end

example [semiring β] :
  (@pi.distrib_mul_action' _ _ _ _ _ (λ _, infer_instance) : distrib_mul_action (α → β) (α → (α → β)))
    = @pi.distrib_mul_action _ _ _ _ _ (λ _, infer_instance) :=
begin
  ext fab faab a₁ a₂,
  dsimp at *,
  sorry -- `fab a₁ * faab a₁ a₂ = fab a₂ * faab a₁ a₂` is not true in general!
end

[Eric Wieser]

(my previous scary diamond thread: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/nat.20smul.20diamond.20in.20set.20actions/near/264004833)

[Eric Wieser]

Should we remove docs#pi.has_scalar'?

[Yury G. Kudryashov]

We can move it to a locale and add a library note explaining this diamond.

[Yury G. Kudryashov]

We definitely want the to_additive version of this action somewhere in affince_spaces.

[Yury G. Kudryashov]

I mean, we want Π i, P i to be an add_torsor over Π i, G i.

[Yury G. Kudryashov]

But IMHO it's OK if a user has to open_locale pi_elementwise to get this action.