Symplectic Linear Algebra

Stream: new members

[Moritz]

Hi there,
I am Moritz, postdoc in Bremen, and got recently interested in Lean. I work mainly in (microlocal) analysis and would like to contribute contribute to the distribution theory and functional analysis parts of lean. To get a feel for proving stuff in lean I am starting out with some easy linear algebra results (with a symplectic form) and I wanted to ask what is a reasonable size for a first PR. Plus my github account is mcdoll.

[Patrick Massot]

Hi! You are very welcome here! We have lots of people doing algebraic geometry here. This is great but we would also love to see more analysis. You should talk to @Heather Macbeth who is currently working and coordinating work both in linear algebra and Fourier theory.

[Patrick Massot]

To answer your specific question, you should start with very small PRs. And first you should discuss your intended topic in a more detailed way here.

[Moritz]

I defined symplectic vector spaces and was going to define the various types of subspaces (isotropic, coisotropic, and Lagrangian) and prove some facts about dimensions and different characterizations of these subspaces and that taking the symplectic orthogonal of a subspace W is equal to W. Basically, I wanted to formalize the content of the homework 1 of the book of Cannas da Silva.
I need the fact that a skewsymmetric bilinear form is reflexive, this is only three lines of proof (and it is very likely that it can be reduced to 1 or 2 lines), so if you want to have very small PRs I could start with that.

[Eric Wieser]

I need the fact that a skewsymmetric bilinear form is reflexive, this is only three lines of proof (and it is very likely that it can be reduced to 1 or 2 lines), so if you want to have very small PRs I could start with that.

That sounds like a good start to me; lemmas are usually easier to review than new definitions

[Kevin Buzzard]

If you still need an invite then ping the maintainers

[Moritz]

@Eric Wieser perfect, could you add me to github? (mcdoll)

[Eric Wieser]

Invite sent!

[Eric Wieser]

Thanks for the first PR!

[Moritz]

Thank you for reviewing it so fast :-) The refactoring you suggested sounds good, I will look at it tomorrow.

[Moritz]

Concerning https://github.com/leanprover-community/mathlib/pull/10304#pullrequestreview-805284143 is it possible to find all files in mathlib where a lemma is used? I crashed my laptop several times today by trying to build mathlib..

[Moritz]

also I feel like there is the general question whether properties of structures should go into the file/namespace where the structure was defined or in the file/namespace where stuff is proved in the case that the structure has this property

[Eric Wieser]

Usually the thing to do is just change the lemma in the first place you find it, push the PR, and then wait for CI to tell you what you missed

[Eric Wieser]

You can run leanproject get-cache after CI fails to get a precompiled build up to the point it failed

[Eric Wieser]

Moritz said:

also I feel like there is the general question whether properties of structures should go into the file/namespace where the structure was defined or in the file/namespace where stuff is proved in the case that the structure has this property

I'm not entirely sure what you have in mind here, but note that decisions about filenames are quite different to decisions about namespaces

[Eric Rodriguez]

I think using VSCode's project search with the lemma name (with and without dot notation) is a good first-order approximation though

[Moritz]

@Eric Wieser I think the question whether the property x of a structure A belongs to the A-namespace or the A_with_x-namespace is very general and maybe this should be consistent throughout mathlib.

[Eric Wieser]

Definitely the former, because if you call it A.is_something, then given a : A you can write a.is_something instead of having to with A_with_x.is_something a