real complex smul_comm_class

Stream: Is there code for X?

[Jireh Loreaux]

This instance I don't think exists, although I didn't try import all. Any reason not to have it? I mean, it's just a Prop so there's no data. This would be the final piece for us to automatically inherit a (non-unital) ℝ-algebra instance from a (non-unital) ℂ-algebra instance.

instance complex.real_smul_comm_class {E F : Type*} [add_comm_group E] [module ℂ E]
  [add_comm_group F] [module ℂ F] [has_smul E F] [smul_comm_class ℂ E F] : smul_comm_class ℝ E F :=
{ smul_comm := λ r _ _, by simpa only [complex.coe_smul] using smul_comm (r : ℂ) _ _ }

[Eric Wieser]

I think that likely forms an instance cycle with docs#complex.smul_comm_class nevermind, the argument order is different

[Eric Wieser]

I also maintain that inheriting the real instance from the complex one (that is, the module instance that already exists) goes against the design of docs#smul_assoc_class, even though it may be convenient

[Jireh Loreaux]

Well, it would even be nice to know that a ℂ-algebra is an ℝ≥0-algebra without having to state it explicitly (which would come for free from this I think).

[Eric Wieser]

In the algebra sense of the word algebra (read: canonical ring hom) that would be a bad idea because the canonical hom found through transitivity is likely not to be defeq to one that already exists

[Eric Wieser]

A more extreme case of your request would be inferring module ℝ M from module ℝ[X] M

[Eric Rodriguez]

I'm confused why this is an isuse, if smul_comm_class works then the algebra instance must already too

[Jireh Loreaux]

(deleted)

[Jireh Loreaux]

Eric R, I think Eric W is worried about definitional equality, where smul_comm_class would only be propositional.

[Eric Rodriguez]

What I'm trying to say is that if your code already compiles, then this "harmful" algebra instance that turns algebra \C E into algebra \R E (or somewhere further down the hierarchy) is already there; I agree that a Prop-valued class cannot cause further issues.

[Jireh Loreaux]

Eric W, I guess I see there may be some difficulties in "inheriting downwards" like this in more abstract classes, but for ℝ≥0, ℝ, ℂ I feel like this is less of an issue. In particular, I can't really imagine a scenario where you would need to first declare a scalar action by ℝ and then another by ℂ in a definitionally different but propositionally equal way where you couldn't just declare the action by ℂ first. I have a similar feeling about ℝ≥0 and ℝ. Nevertheless, I'm open to being enlightened by hypothetical or actual situations.

[Jireh Loreaux]

Agreed, I think Eric W is taking issue with those data-carrying instances that already exist, not my smul_comm_class instance above in particular; only that it is indicative of what he feels is a larger problem.

[Jireh Loreaux]

well, since we have these data-carrying instances for now: #16513