sylvester's law of inertia

Stream: general

[Johan Commelin]

If there are people looking for an interesting first project to work on, with the aim of making a PR to mathlib, I'm willing to coach #2551 on Sylvester's law of inertia

[Sam Lichtenstein]

I was looking at that PR and when trying to figure out what ingredients are already in mathlib, I realized that I don't really know how experts navigate the library. Do you typically grep the source tree directly? Use the google search on the mathlib docs webpage? Some better method I don't know about (maybe a VSCode or emacs trick)? Relatedly, google search for "eigenvector" turned up no hits in the mathlib docs, and the same when searching the github repo (which I guess would also turn up PRs that mentioned this term, if there were any?) -- this seemed surprising to me. So I grepped and found only the following [using a terminal with poor unicode support]

$ grep -r eigenv .
./archive/sensitivity.lean:lemma exists_eigenvalue (H : set (Q (m + 1))) (hH : Card H ≥ 2^m + 1) :
./archive/sensitivity.lean:  rcases exists_eigenvalue H hH with ⟨y, ⟨⟨y_mem_H, y_mem_g⟩, y_ne⟩⟩,

Am I somehow missing a bunch of linear algebra stuff, or is the current state of the art quite barebones?

[Mario Carneiro]

Eigenvalues are not developed. I think this was blocked on the characteristic polynomial, but that might be solved now

[Mario Carneiro]

I suppose that the eigenvalues of a linear map are relatively easy to define

[Mario Carneiro]

although maybe it is more complicated if you want the eigenvalues to live in an algebraic extension of the scalar ring of the module

[Sam Lichtenstein]

" I think this was blocked on the characteristic polynomial, but that might be solved now"

Does this imply that there is a bunch of quasi-written code out there in various people's clones? In general, is there a way to distinguish cases where (supposedly simple thing X) is missing from mathlib because nobody has bothered to formalize it, from other cases where it is missing because there is some key technical bottleneck or disagreement about the implementation, and once that's resolved X is already effectively done?

[Mario Carneiro]

the best way is to ask here

[Mario Carneiro]

if you are lucky there might be an issue about it, or it could be on a docs or project page, but I would say that is the minority

[Sam Lichtenstein]

I guess that is a good pragmatic answer but doesn't seem like an ideal, scalable solution? I see now that the "undergraduate math list" thread in #general started with some complaints related to mine above, about navigability / discoverability

[Sam Lichtenstein]

also, to clarify, am I correct that the community's convention is NOT to allow sorry in committed .lean files in mathlib, nor to clutter these files with comments containing long TODO lists of lemmas/theorems that would be nice to have eventually? so github issues are the "canonical" place to look for known missing features (aside from asking here)

[Bryan Gin-ge Chen]

sorry is definitely not allowed, except possibly in the roadmap/ directory where there's some trick for using it.

[Sam Lichtenstein]

ah, I had not noticed the roadmap/ directory, which is a nice idea -- but seems sparsely populated :)

[Bryan Gin-ge Chen]

I don't know what to say about long TODOs. I guess I don't see why anyone would want to add very long TODOs.

GitHub issues is the right place to look outside of Zulip for now. We should make an effort to document more things there, since Zulip is definitely less accessible.

[Sam Lichtenstein]

I guess with only 80 open issues, all of mathematics is close to being complete :-)

[Bryan Gin-ge Chen]

Lots of things we do now aren't scalable. I think we can worry about optimizing our processes when we have more contributors and contributions.

[Mario Carneiro]

Sam Lichtenstein said:

I guess that is a good pragmatic answer but doesn't seem like an ideal, scalable solution? I see now that the "undergraduate math list" thread in #general started with some complaints related to mine above, about navigability / discoverability

Does this scale? Probably not, but that doesn't mean it's not the appropriate solution at this scale. Mathlib procedures have changed as we have grown, and they will continue to change

[Sam Lichtenstein]

yeah that makes sense -- I'm just trying to figure out how to understand the lay of the land as a newbie

[Mario Carneiro]

Anyway, here's something to get you started on eigenvectors:

import linear_algebra.basic

variables {R : Type*} {M : Type*}
variables [comm_ring R] [add_comm_group M] [module R M]

def eigenvectors (f : M →ₗ[R] M) (Λ : R) : submodule R M :=
{ carrier := {v | f v = Λ • v},
  zero := f.map_zero.trans (smul_zero _).symm,
  add := λ a b ha hb, by simp [*, smul_add] at *,
  smul := λ c a ha, by simp [*, smul_comm] at * }

@[simp] theorem mem_eigenvectors {f : M →ₗ[R] M} {Λ : R} {v} :
  v ∈ eigenvectors f Λ ↔ f v = Λ • v := iff.rfl

[Sam Lichtenstein]

thanks!

[Mario Carneiro]

def eigenvalues (f : M →ₗ[R] M) : set R := {Λ | eigenvectors f Λ ≠ ⊥}

[Scott Morrison]

Regarding TODO, roadmap/, and the issues page: I think we'd be very happy with contributions in any of these three directions (as long as they are specific enough to be useful: a list of aspirations is only helpful if you're planning on working on them soon). I think for now everyone is open minded about which system works best, and if one of those three gains significant momentum then we can formalise that as the preferred approach.

[Yury G. Kudryashov]

roadmap/ works like an issue + branch with some preliminary work.

[Scott Morrison]

I would love to see more roadmaps. I think it's much more accessible to get started on something if someone with more mathlib design experience has already made a guess about how the primary definitions should be structured, and indicated which lemmas to aim for.

[Kevin Buzzard]

I wanted some basic number theory and algebra done at some point, and wanted to flag that it was not done, and so I just made a project. Nobody is working hard on it but if it's still in that state in July I'll see if I can get some students working on it

[Patrick Massot]

We can't do eigenvalues until Lean 4, because λ is a reserved symbol in Lean 3.

[Mario Carneiro]

I think it's reserved in lean 4 too :/

[Patrick Massot]

What? I thought this was gone. And you can override anything in Lean 4 so you can probably unreserve it

[Mario Carneiro]

Nope: https://github.com/leanprover/lean4/blob/master/src/Init/Lean/Parser/Term.lean#L99

[Patrick Massot]

It doesn't say you can't unreserve it in favor of $\mapsto$

[Kevin Buzzard]

It's ok we can just fork