is_hermitian vs is_self_adjoint

Stream: maths

[Eric Wieser]

docs#matrix.is_hermitian is defeq to the more general docs#is_self_adjoint; should we remove the former entirely, or keep it as an abbreviation of the latter?

[Frédéric Dupuis]

I would vote for removing it entirely.

[Jireh Loreaux]

I prefer removing it also, but I'm okay with an abbrev if others want it.

[Pedro Sánchez Terraf]

I think both names are commonly used, so keeping an abbreviation would make things easier for people searching for the concept (or wouldn't it? docstrings are enough for the search facilities?)

[Jireh Loreaux]

With an abbrev could we retain the current dot notation advantages of matrix.is_hermitian?

Looking at linear_algebra.matrix.hermitian there are several things which are duplicates of similar facts for is_self_adjoint (e.g., docs#matrix.is_hermitian_mul_conj_transpose_self and docs#is_self_adjoint.mul_star_self, or docs#matrix.is_hermitian_mul_mul_conj_transpose and docs#is_self_adjoint.conjugate, and plenty others), so there is quite a bit of duplication here.

[Eric Wieser]

Ah the very least we should replace all the proofs with calls to the is_self_adjoint lemmas

[Eric Wieser]

It turns out a lot of lemmas about is_self_adjoint are not stated generally enough to be used to prove the matrix results; I've tried to fix that in #18558

[Eric Wieser]

... and some instances about matrices are not general enough to apply the self-adjoint lemmas: #18563, #18557

[Eric Wieser]

#18565 replaces a handful of proofs of is_hermitian_foo with is_self_adjoint_foo _, and generalizes a few results in the other direction too.

[Eric Wieser]

Oh no: docs#matrix.is_self_adjoint

[Jireh Loreaux]

that's a genuinely distinct concept, but it would be nice if either it were named differently or else the docstring mentioned the relationship to is_self_adjoint, and maybe a lemma linking the concepts when they coincide.

[Eric Wieser]

I think the link is

example [has_trivial_star R] (A : matrix n n R) :
  matrix.is_self_adjoint 1 A ↔ is_self_adjoint A

[Eric Wieser]

Is the requirement that star is trivial expected?

[Jireh Loreaux]

oof, that's painful. Here's what I suspect, but I don't know for sure: this is a relic of stuff on bilinear forms that existed before the semilinear map refactor. At the time there would have been no way to "properly" handle sesquilinear forms, which is probably what you would really want in order not to need has_trivial_star.

The above is only my impression after a cursory glance. It may be wrong. Maybe just adding an appropriate note to the docstring would be enough for now, but I'm not really sure what to say.

[Eric Wieser]

Would you expect docs#matrix.is_adjoint_pair to be defined with ᴴ then instead?

[Jireh Loreaux]

maybe or else this: J.is_self_adjoint A₁ := J.is_adjoint_pair J A₁ A₁ᴴ

[Jireh Loreaux]

I'm tired, so I may not be thinking about this clearly at the moment.

[Anatole Dedecker]

The right way to think about docs#matrix.is_adjoint_pair is that it should be the matrix version of docs#linear_map.is_adjoint_pair right ?

[Anatole Dedecker]

If so then indeed I think the right thing is to apply the ring hom I (of docs#linear_map.is_adjoint_pair) to the transposed matrix in docs#matrix.is_self_adjoint

[Eric Wieser]

Do we keep around an I, or just assume that star_ring_end is the right I for matrices?

[Eric Wieser]

Eric Wieser said:

#18565 replaces a handful of proofs of is_hermitian_foo with is_self_adjoint_foo _, and generalizes a few results in the other direction too.

Also, it would be great if someone could take a look at this; once it's in, I plan to forward-port the changes to self_adjoint.lean that I made in some previous PRs.

[Jireh Loreaux]

I'll look at this and your quaternion PR now. I already briefly looked at the latter on mobile.

[Jireh Loreaux]

What do you mean by "keep around an I"?

[Jireh Loreaux]

I've left some comments on #18565

[Eric Wieser]

Jireh Loreaux said:

What do you mean by "keep around an I"?

I mean "parameterize the matrix version with an arbitrary ring hom" as opposed to 'use the canonical star one"

[Eric Wieser]

Jireh Loreaux said:

I'll look at this and your quaternion PR now. I already briefly looked at the latter on mobile.

Thanks!

[Anatole Dedecker]

Eric Wieser said:

Do we keep around an I, or just assume that star_ring_end is the right I for matrices?

I think that the two sides of the API (linear maps and matrices) should be as close as possible to each other, so I’d keep the I