More stuff about kernels/ranges of matrices

Stream: Is there code for X?

[Alex Meiburg]

I need, in particular, this fact:

theorem ker_range_antitone {d : Type*} [Fintype d] [DecidableEq d] {A B : Matrix d d ℂ}
  (hA : A.IsHermitian) (hB : B.IsHermitian) :
    LinearMap.range A.toLin' ≤ LinearMap.range B.toLin' ↔
    LinearMap.ker B.toLin' ≤ LinearMap.ker A.toLin' := by
  sorry

and I've got a number of other places where I'm running into similar facts I need. Two questions:

• Tips to go about proving this? I'm not very comfortable with some of the pretty general linear algebra in mathlib. (I'm so used to just thinking about real/complex matrices that I start to stumble when I go beyond that.) I thought there would be at least some facts in Mathlib relating LinearMap.ker and LinearMap.range`, but I can't find basically any! I expected at least the fact that they're complementary subspaces, but I couldn't find that anywhere.
• The theorem statement above is, of course, really just about the 0-eigenspace of a Hermitian operator. All I "really" am saying is that "[nonzero eigenspace of A] <= [nonzero eigenspace of B] iff [zero eigenspace of B] <= [zero eigenspace of A]", which is maybe easier to do. There is docs#Module.End.eigenspace, but I similarly have a hard time eliciting useful stuff from that.

[Kevin Buzzard]

My instinct would be to write down the proof for Hermitian linear maps and deduce the result for matrices. Here's one direction: if $AV\subseteq BV$ and $v\in ker(B)$ then for all $w$ we have $Bv=0$ so for all w we have $(Bw,v)=(w,Bv)=0$, and $AV\subseteq BV$ means that for all $x$ we have $(Ax,v)=0$ meaning $(x,Av)=0$ and hence $Av=0$ (no finite-dimensionality hypotheses needed).

[Alex Meiburg]

Hmm, I guess I hadn't actually thought about trying to do that 'directly', I thought I would need to appeal to something more powerful. Well, here's that first half then:

import Mathlib

theorem LinearMap.ker_range_antitone {V 𝕜 : Type*} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {A B : V →ₗ[𝕜] V}
  (hA : A.IsSymmetric) (hB : B.IsSymmetric) :
    LinearMap.range A ≤ LinearMap.range B ↔ LinearMap.ker B ≤ LinearMap.ker A := by
  constructor
  · intro h v hv
    rw [LinearMap.mem_ker] at hv ⊢
    obtain ⟨y, hy⟩ : ∃ y, B y = A (A v) := by simpa using @h (A (A v))
    rw [← inner_self_eq_zero (𝕜 := 𝕜), ← hA, ← hy, hB, hv, inner_zero_right]
  · sorry

so that's progress. But then applying to Matrices seems like some sort of instance hell, which means I'm probably doing something wrong.

theorem Matrix.ker_range_antitone {d : Type*} [Fintype d] [DecidableEq d] {A B : Matrix d d ℂ}
  (hA : A.IsHermitian) (hB : B.IsHermitian) :
    LinearMap.range A.toLin' ≤ LinearMap.range B.toLin' ↔
    LinearMap.ker B.toLin' ≤ LinearMap.ker A.toLin' := by
  have _ : InnerProductSpace ℂ (d → ℂ) := sorry--PiLp.innerProductSpace (𝕜 := ℂ) (fun (i : d) ↦ ℂ)
  have := LinearMap.ker_range_antitone (V := d → ℂ) (𝕜 := ℂ) (A := A.toLin') (B := B.toLin')
/-
application type mismatch
  @LinearMap.ker_range_antitone (d → ℂ) ℂ ?m.61525 ?m.61526 ?m.61527 (toLin' A)
argument
  toLin' A
has type
  @LinearMap ℂ ℂ CommSemiring.toSemiring CommSemiring.toSemiring (RingHom.id ℂ) (d → ℂ) (d → ℂ) Pi.addCommMonoid
    Pi.addCommMonoid (Pi.Function.module d ℂ ℂ) (Pi.Function.module d ℂ ℂ) : Type u_1
but is expected to have type
  @LinearMap ℂ ℂ DivisionSemiring.toSemiring DivisionSemiring.toSemiring (RingHom.id ℂ) (d → ℂ) (d → ℂ)
    ENormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule
    NormedSpace.toModule : Type u_1Lean 4
  -/
  sorry

:(

[Alex Meiburg]

which makes me wonder, again, if this is a sign I should be stating this differently to start with. :/

[Eric Wieser]

You maybe want docs#Matrix.toEuclideanLin

[Eric Wieser]

That is, you need to first move to euclidean space (by mapping / comapping through WithLp.linearEquiv), then you should be able to apply the lemma

[Kenny Lau]

@Alex Meiburg here is the steps I took to debug (which resulted in the same conclusion as Eric):

1. I first noted that the error started at A.toLin', so I replaced it with by convert A.toLin' to see what the conflicting instance was, and it gave me NormedSpace.toModule = Pi.Function.module d ℂ ℂ.
2. I tried to trace that a bit to no avail, so this step was not fruitful.
3. Then I think about what the main connection between the two lemmas are: it's the fact that symmetric matrices are supposed to correspond to Hermitian matrices (i.e. the main difference between the two lemmas).
4. Then I went to the docs for Hermitian, where this equivalence is likely defined.
5. Then I searched (Ctrl+F) for "symmetric", and finally found the lemma Matrix.isHermitian_iff_isSymmetric: A.IsHermitian ↔ (toEuclideanLin A).IsSymmetric.
6. This suggests that toEuclideanLin is actually the idiomatic way to convert between matrices and linear maps (under the context of inner product), and this lemma gives you exactly the key you needed to translate between the two objects.

[Eric Wieser]

Really you got in trouble as soon as you wrote have _ : InnerProductSpace ℂ (d → ℂ) :=

[Kenny Lau]

oh wow I don't know how I missed that line

[Eric Wieser]

Ending with PiLp.innerProductSpace is obviously a bad idea because it defeats the type synonym, ending with sorry is just as bad but less obviously so

[Alex Meiburg]

Alright thanks guys! Yeah the PiLp stuff is still a bit confusing to me and I haven't sat down and learned how to work with it properly. And I hadn't ever seen toEuclideanLin.

[Alex Meiburg]

@Kenny Lau thanks especially for showing me your thinking/debugging process, that was very helpful

[Kenny Lau]

Alex Meiburg said:

Yeah the PiLp stuff is still a bit confusing to me and I haven't sat down and learned how to work with it properly.

Since it hasn't been spelled out to you explicitly yet, instances contain data (e.g. how to add stuff together), and have destroys data (at least in my understanding, I could be wrong here). If you're stuck because of instances, it isn't a good idea to provide them using have. let is preferred over have, but it is still not preferred. It is usually caused by an entirely different problem that cannot be solved locally just by using let.

And I hadn't ever seen toEuclideanLin.

And neither have I, and that's why loogle and the docs etc. exist, so that you can find idiomatic ways to do the things you want, in this case to convert between IsHermitian and IsSymmetric.

[Alex Meiburg]

Yeah, that have was just while I was trying to debug it myself, I know it's trouble :sweat_smile:
And I used loogle -- plenty! And the docs. But I think I still need practice picking the right "culprits" to home in on

[Eric Wieser]

Kenny Lau said:

Since it hasn't been spelled out to you explicitly yet, instances contain data (e.g. how to add stuff together), and have destroys data (at least in my understanding,

This is morally close enough, but in this particular case the data was sorry so you're already hosed whether the data is forgotten or not.

[Eric Wieser]

@Paul Lezeau was working towards a refactor that would make WithLp harder to trip over, but has been busy and this reviewer hasn't been very prompt either

[Paul Lezeau]

The PR for that refactor is #24261. If this is blocking other people I can make this a priority:)

[Alex Meiburg]

Got back to this now, got it done. (The reverse direction was definitely uglier, maybe there's a better way.)

I'm still surprised though, to me this is an "early undergrad fact" so it's weird that it's missing, and that's what maxes me wonder if I "should" be doing it an entirely different way.

The undergrad proof I'm familiar with is: kernel and range are orthogonal complements, and orthogonal complements reverse containment of subspaces. One liner! I thought.

When I try to write down this proof, I'm confounded with what the right kind of "orthogonal complement" to use. There's BilinForm.orthogonal, Submodule.orthogonalBilin, HasOrthogonalProjection, and Submodule.orthogonal.

I try looking for things that relate one of these to range/kernel or the submodule ordering, and have little luck, e.g.

@loogle _ ≤ _, Submodule.HasOrthogonalProjection

@loogle LinearMap.range, Submodule.orthogonal

and none of those look relevant. :(

Is this just a 'gap' in mathlib? Is this an example of, the undergrad approach not matching the 'mature' approach to the topic? Am I doing something wrong?

[loogle]

:search: Submodule.sup_orthogonal_inf_of_completeSpace, Submodule.orthogonalProjection_norm_le, and 4 more