undergrad todo trivial target Linear Algebra / Duality /

Stream: Is there code for X?

[Justin Thomas]

On the wiki, the top trivial target is

Duality
orthogonality This should be a definition together with at least basic lemmas about the orthogonal of the bottom and top subspaces, of an intersection, union, sum.

I am checking in to see if

1. this is already done but I have missed it
2. clarify: the wiki defines the annihilator of an arbitrary set in a vector space and mentions the orthogonal complement is isomorphic to the annihilator in the finite dimensional case. Following wikipedia, the approach would be to define annihilator for general R-modules, prove general lemmas, then specialize and link up to orthogonality, etc. However, I got the impression from the mathlib github wiki that a definition of orthogonal complement is the desired thing. No mention of annihilator of a set there.

[Justin Thomas]

update: found definition dual_annihilator in linear_algebra/dual.lean

[Patrick Massot]

This is indeed the definition that we are talking about now. So we could simply edit undergrad.yaml to mention it. However it would be nice to add a couple more basic lemmas. For instance I see docs#submodule.dual_annihilator_sup_eq_inf_dual_annihilator but this is only for two subspaces, and I don't see the dual of top or bottom. And then indeed there is extra credit for linking this with bilinear algebra (for instance scalar products), maybe asking @Heather Macbeth for help.

[Eric Wieser]

Do we need an intermediate "definition exist but obvious lemmas missing" state for the yaml file?

[Eric Wieser]

For instance, the recent annihilating polynomials PR doesn't address everything in the wikipedia page introduction, but at least provides the definition