feat(LinearAlgebra/Matrix/Hermitian): add IsSkewHermitian predicate

[JohnnyTeutonic]

Adds IsSkewHermitian predicate for matrices satisfying Aᴴ = -A.

---

[github-actions]

PR summary 2c8f930e22

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ IsSkewHermitian
+ IsSkewHermitian.add
+ IsSkewHermitian.apply
+ IsSkewHermitian.eq
+ IsSkewHermitian.ext
+ IsSkewHermitian.ext_iff
+ IsSkewHermitian.neg
+ IsSkewHermitian.star_diag
+ IsSkewHermitian.sub
+ IsSkewHermitian.transpose
+ isSkewHermitian_diagonal_iff
+ isSkewHermitian_transpose_iff

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[themathqueen]

Some notes:

• The definition should only require Star α and Neg α, not an additive group.
• You should add a lot more API. I would look at the Hermitian API and add the skew-Hermitian analogs of them. Not everything. Just the important stuff, I guess?

[JohnnyTeutonic]

Where should IsSkewHermitian.add and IsSkewHermitian.sub live?

The proofs need neg_add : -(a + b) = -a + -b which requires SubtractionCommMonoid. The current AddGroup section only has [AddGroup α] [StarAddMonoid α]. Should I:

Add a SubtractionCommMonoid section for these theorems?
Put them in a Ring section where this is available?
Skip them for now?

[JohnnyTeutonic]

@themathqueen - sorry to be a bother, but whenever you are free, please let me know how you'd like me to proceed =)

[themathqueen]

Add a SubtractionCommMonoid section for these theorems? Put them in a Ring section where this is available? Skip them for now?

Probably a new section? Seems reasonable. Do what you think is best :)

[JohnnyTeutonic]

Regarding add/sub: I attempted adding these in a SubtractionCommMonoid section, but ran into a typeclass issue:

The proof needs neg_add : -(a + b) = -a + -b which requires SubtractionCommMonoid
However, Matrix n n α doesn't have a SubtractionCommMonoid instance when we only have [AddGroup α] [StarAddMonoid α]
conjTranspose_sub also requires AddGroup
I can either:

Add these in a Ring section where all the instances are available
Skip them for now and add in a follow-up PR
Something else you'd suggest?

[themathqueen]

Looking at https://en.wikipedia.org/wiki/Skew-Hermitian_matrix, there's some more nice properties you can add here. In particular, A is skew-Hermitian iff iA is Hermitian (I think the appropriate place for this would be in Analysis/Matrix/Hermitian?). There's also that the diagonal of a skew-Hermitian has to be pure imaginary (again, in Analysis/Matrix/Hermitian).
But actually, I think you can just generalize the second to:

@[simp] theorem isSkewHermitian_diagonal_iff [SubtractionMonoid α] [StarAddMonoid α]
    [DecidableEq n] (A : n → α) :
    (diagonal A).IsSkewHermitian ↔ star A = -A := by
  simp [IsSkewHermitian, funext_iff]

theorem IsSkewHermitian.star_diag [SubtractionMonoid α] [StarAddMonoid α]
    {A : Matrix n n α} (hA : A.IsSkewHermitian) :
    star (diag A) = -(diag A) := by
  classical
  simp_all [← isSkewHermitian_diagonal_iff, IsSkewHermitian, ← conjTranspose_apply]

[JohnnyTeutonic]

Added isSkewHermitian_diagonal_iff and star_diag as suggested - thanks for the clean proof!

Current PR now includes the full basic API:

Definition + eq, ext, apply, ext_iff
transpose, isSkewHermitian_transpose_iff
isSkewHermitian_diagonal_iff, star_diag
add (SubtractionCommMonoid), neg (AddGroup), sub (Ring)

For the I • A ↔ Hermitian theorem and eigenvalue properties - these involve RCLike proofs in Analysis/Matrix/Hermitian. Happy to add them here if you'd like, or tackle them in a follow-up PR to keep this one scoped to LinearAlgebra/Matrix. What's your preference?

[JohnnyTeutonic]

@themathqueen - ready for review unless you'd like more changes.

[themathqueen]

I think you could probably connect this to skewAdjoint.

We don't have an IsSkewAdjoint definition though and maybe there's a reason for that, or maybe we should have that? @eric-wieser, should we have this?

[JohnnyTeutonic]

Good point — IsSkewHermitian is to skewAdjoint as IsHermitian is to IsSelfAdjoint. I can add:

theorem isSkewHermitian_iff_mem_skewAdjoint :
    A.IsSkewHermitian ↔ A ∈ skewAdjoint (Matrix n n α) := Iff.rfl

Can add that here if warranted.
Whether a standalone IsSkewAdjoint definition is warranted seems like a separate question — happy to defer to @eric-wieser on that.

[j-loreaux]

@JohnnyTeutonic can you please comment on the reason you want this predicate, aside from parallelism? In particular, which types α do you care about? I'm quite hesitant to add it, because new definition creates more API surface area, which leads to more friction. Depending on your ultimate use case, I may be able to make some suggestions to simplify things for you.

[JohnnyTeutonic]

@j-loreaux
The use case is Lie algebra theory — su(n) is characterized as the skew-Hermitian matrices in Matrix n n ℂ. I'm cool to just use A ∈ skewAdjoint _ if you think that's sufficient. Should I close this and instead contribute lemmas about skewAdjoint for Matrix?