Making `StarOrderedRing` a mixin

Stream: mathlib4

[Jireh Loreaux]

@Eric Wieser @Frédéric Dupuis @Anatole Dedecker : I think that docs#StarOrderedRing should be a mixin class that takes StarRing as a parameter. The reasoning comes down to two issues.

The first is that we need to be able to make C(α, R) into a star-ordered ring for certain values of R. Right now, we can do this only for particular values of R, but we have no type class assumptions that we can put on R (at least, no existing ones, and any new one would be ad-hoc) to guarantee that C(α, R) is a star-ordered ring. This is problematic for working with the functional calculus (because we want to be able to say that cfcHom is monotone on functions, which follows from the fact that it is star homomorphism, but only if the domain and codomain are star-ordered rings.

The second is that we will eventually want C(α, A) to be a star-ordered ring whenever A is a C⋆-algebra, but, as I indicated before, there will be no way to assume this as a hypothesis.

Do any of you have qualms about this change?

[Frédéric Dupuis]

I'm OK with it!

[Eric Wieser]

Sounds fine by me Sounds harmless, but I don't understand the motivation yet.

[Eric Wieser]

Though I don't immediately understand why making it a mixin helps with your first point

[Eric Wieser]

The second is that we will eventually want C(α, A) to be a star-ordered ring whenever A is a C⋆-algebra, but, as I indicated before, there will be no way to assume this as a hypothesis.

Can this work? I forget the spelling of "C⋆-algebra" in mathlib, but on the assumption it has a base ring argument, you can't conclude StarOrderedRing from it because that typeclass does not have that argument. (it's the Module R M not being allowed to imply AddCommMonoid M thing)

[Jireh Loreaux]

For the second point, it"s not a problem because the scalar ring is a fixed type (\C for now, and later \R too).

[Jireh Loreaux]

For the first point, I want to be able to say that docs#cfcHom is order preserving when the domain and codomain are star ordered rings. But (a) there is no hypothesis I can currently assume on R to make the continuous R-valued functions a star-ordered ring, and (b) I can't just assume [StarOrderedRing C(\alpha, R)] because that puts a second star operation on the continuous functions.

[Anatole Dedecker]

To me it makes sense, I’ve always found it a bit weird to bundle algebra and order instead of having compatibility mixins (which we can do now with docs#CovariantClass and friends).