complex conj vs has_star.star

Stream: maths

[Yury G. Kudryashov]

Is there any reason to have both? I understand that mathematicians care about notation but we can have

notation `conj` := @has_star.star complex complex.has_star

or something like that.

[Heather Macbeth]

I think star as currently defined goes between a ring and its opposite, right? I might worry that some unexpected messes would arise with type synonyms.

[Frédéric Dupuis]

Heather Macbeth said:

I think star as currently defined goes between a ring and its opposite, right? I might worry that some unexpected messes would arise with type synonyms.

No, has_star.star is just some function R → R.

[Yury G. Kudryashov]

docs#has_star.star docs#star_ring

[Frédéric Dupuis]

I can't really think of a good reason to keep conj, this sounds like a good idea.

[Yury G. Kudryashov]

Also, with unified has_star.star approach we won't have to duplicate code between complex semilinear maps and semilinear maps between star rings.

[Yury G. Kudryashov]

I think, the only reason complex.conj exists is that star_rings were not there, and nobody cared to do a refactor.

[Yury G. Kudryashov]

Opened an issue #9421

[Heather Macbeth]

I actually tried (... not very hard) rewriting star_ring using semilinear stuff last weekend. I found the star hierarchy a bit awkward to use -- I wonder whether it would be better to have separate classes star_ring equipped with a ring equiv star, star_algebra equipped with an algebra star, etc.

[Yury G. Kudryashov]

Sorry, I don't understand. What exactly is wrong with current setup?

[Heather Macbeth]

Here is the point I found tricky: how do you translate

class star_algebra (R : Type u) (A : Type v)
  [comm_semiring R] [star_ring R] [semiring A] [star_ring A] [algebra R A] :=
(star_smul : ∀ (r : R) (a : A), star (r • a) = (@has_star.star R _ r) • star a)

to a semilinear statement? I couldn't think of a simpler way than saying, "there exists an R-star-semilinear-map from A to itself, which we will call star', and whose underlying function is equal to star."

[Frédéric Dupuis]

Hmm, I guess you would want star to be a bundled semilinear map.

[Heather Macbeth]

Yes. (Eventually more ... we want to define semilinear algebra-maps and then star will be such a thing.)

[Heather Macbeth]

But this is why I said above that I wondered if the star hierarchy would work better if star was not just a function, introduced using this has_star class, but came with more structure -- add hom, ring hom, different for each algebraic object.

[Frédéric Dupuis]

Right, but there's a bootstrap problem here, in the sense that the ring hom we want star to be semilinear over should itself be the star of something else.

[Yury G. Kudryashov]

Why not define linear_equiv.star to be a bundled semilinear equivalence, and leave star to be unbundled?

[Heather Macbeth]

I don't think I understand either Frédéric's comment (i.e., I agree that "the ring hom we want star to be semilinear over should itself be the star of something else" but I don't see yet why it's a problem) or Yury's.

[Frédéric Dupuis]

My point was that if we look at i.e. the complex numbers, and we define has_star.star to be a semilinear equivalence, what is it semilinear over? I guess we would have to keep complex.conj. (Which isn't really a problem.)

[Heather Macbeth]

I was thinking it would run more as follows: in the instance of the complex numbers as a star-algebra, the star operation is a semilinear-algebra-equiv-involution, semilinear over the ring-equiv-involution which is the star operation of the complex numbers considered as a star-ring.

[Heather Macbeth]

(!)

[Frédéric Dupuis]

Ah, so you would have totally separate star operations, as opposed to has_star to which we add more properties in separate classes?

[Yury G. Kudryashov]

We have things like mul_equiv.inv etc. We can define ring_equiv.star and/or star_ring_equiv.star too.

[Heather Macbeth]

Frédéric Dupuis said:

Ah, so you would have totally separate star operations, as opposed to has_star to which we add more properties in separate classes?

Yes. (If we even do it at all ... I'm not sure yet whether we really want to upgrade star-theory from "convenient formalism invented by Scott to prove a form of Clauser-Horne-Shimony-Holt" to "core part of the algebraic hierarchy")

[Heather Macbeth]

Yury, your idea is that we have both the unbundled star as a function, and the bundled version?

[Heather Macbeth]

(With the bundled version constructed from the unbundled version using the axioms.)

[Frédéric Dupuis]

I think it would be worth expanding this part of the library actually -- things like C*-algebras are definitely worth having and this is a good start.

[Heather Macbeth]

That's true -- as another possible point of use: when I was proving complex Stone-Weierstrass I wished that the results I was proving ad-hoc about the involution of $C(X, \mathbb{C})$ defined by pointwise conjugation were in fact general results about conjugate-linear involutions of complex modules.

[Yury G. Kudryashov]

@Heather Macbeth I think that we should choose some minimal interface (has_star? star_ring? something else?) and define star to be the corresponding bundled automorphism.

[Yury G. Kudryashov]

Note that we can have an unbundled has_star.star and all lemmas restated in terms of a bundled automorphism.

[Yury G. Kudryashov]

(and use only the bundled version outside of instance definitions)

[Frédéric Dupuis]

I was also thinking a bit about how to formalize information theory in a way that covers all cases of interest. The challenge here is to define the relative entropy in a uniform way for probability measures and for quantum states. I think a general definition involving some sort of star algebra might work but I haven't fully thought it through.

[Scott Morrison]

I certainly agree that we shouldn't be afraid of messing with the CHSH design. :-) Whatever makes C-star algebras work best!

[Heather Macbeth]

@Scott Morrison, when you decided to make the star hierarchy a mixin hierarchy,

These are implemented as "mixin" typeclasses, so to summon a star ring (for example)
one needs to write (R : Type) [ring R] [star_ring R].
This avoids difficulties with diamond inheritance.

did you do this mainly because you wanted something quick and lightweight? Would you have made star_{monoid, ring, ...} extend {monoid, ring, ...} if you'd had the energy?

[Scott Morrison]

I did that because it seemed at that time we wanted to escape combinatorial explosion of the algebra hierarchy, and people were working on the refactors of both ordered_* and topological_* to a mixin model. I didn't want to cause another problem.

[Scott Morrison]

So no, I don't think I would have, energy permitting. :-)

[Heather Macbeth]

I guess what seems odd to me is that the axioms on star in star_monoid amound to is_mul_hom (modulo commutativity), in star_add_monoid they amount to is_add_hom, in star_ring they amount to is_ring_hom, etc.

[Heather Macbeth]

And unbundled morphisms are very unfashionable :)

[Eric Wieser]

You could say the same thing about semiring looking like is_add_hom (* a) though, right?

[Eric Wieser]

I've PR'd #9426 which adds star_linear_equiv as a semilinear equiv

[Eric Wieser]

I ran into some typeclass inference problems with the semilinear equivalence here.

I'm not particularly invested in what remains in this PR; perhaps someone more involved in the semilinear refactor should adopt it?

[Heather Macbeth]

I'll look at it later, but in the meantime look at how it's done in our "test" file src/linear_algebra/conjugate_linear.lean in the branch#semilinear-surjective.

[Frédéric Dupuis]

@Eric Wieser I could adopt #9426 if you want.

[Eric Wieser]

Please do! I'll wrap up the last dependent PR, but the rest can be yours

[Frédéric Dupuis]

I just opened a PR to replace complex.conj and is_R_or_C.conj with star_ring_aut: #9640. It works quite well!

[Eric Wieser]

I'm a little wary of not making star_ring_aut_apply simp any more, as now all the lemmas about star won't apply to it.

[Eric Wieser]

How much breaks if you leave that as simp?

[Frédéric Dupuis]

The main problem with that lemma being a simp lemma is that simp always unbundles star_ring_aut, leaving us with the bare function star. We definitely don't want this.

[Frédéric Dupuis]

I removed the simp attribute because it got annoying very quickly.