Exterior powers

Stream: Is there code for X?

[Sophie Morel]

What is know about exterior powers in mathlib ? So far the best I found is https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/ExteriorAlgebra/Grading.html, which defines the exterior algebra as a graded algebra.

I asked lean to synthesize a FiniteDimensional instance on the nth exterior of a finite-dimensional vector space and got an error. That is not very hard to fix, but does this mean that mathlib doesn't have the formula for the dimension of the nth exterior power of a finite-dimensional vector space (or a free module of finite rank) ?

Still about exterior powers but unrelated, what about the NormedSpace case ? Is the topological vector space structure on exterior powers defined ?

The reason of all these questions, of course, is that I am trying to define the Plücker embedding from a Grassmannian to a projective space, and I want to do it coordinate-free. Hence exterior powers.

[Sebastien Gouezel]

I don't think we have anything serious there. Maybe @Yury G. Kudryashov or @Heather Macbeth have something more on a branch, towards de Rham cohomology, but not PRed yet if I understand correctly.

[Sophie Morel]

Okay, I can sorry the results I need about dimension of exterior powers for now.

I can also work in finite dimension so the exterior power has a canonical topological vector space structure. But now I have another question, as I don't just need a tvs structure to define the manifold structure, I need a NormedSpace instance: is there some preferred way to put a NormedSpace instance on a finite-dimensional vector space over a NontriviallyNormedField ? I have been looking at the NormedSpace files in mathlib but I haven't found anything yet. (Of course I can do it myself: use choice to pick an isomorphism with a Fin r → 𝕜 (where 𝕜 is my base field) and then transport the norm. I was just wondering is there's a better way.)

[Antoine Chambert-Loir]

Even if you choose a basis, what norm will you choose on ‘Fin r to k‘?

[Sebastien Gouezel]

I would avoid using finite-dimensionality to choose a norm and arguing that since all norms are equivalent it gives the right topology. Instead I'd rather put the correct norm on exterior products of a normed space-- whatever that is. For the exterior product of a dual space, I know what this should be: the operator norm on multilinear maps. For the exterior product of a space, maybe embed it into its bidual and use the previous sentence -- or do that in a more canonical way I am not thinking of for now, probably.

[Sebastien Gouezel]

Note that it would make sense to do that for tensor products first. There are two canonical norms on tensor products, but only one of them comes from the point of view of multilinear maps, so that's probably the one whose analogue we want to use here.

[Eric Wieser]

There's an open issue about putting an inner product space structure on the tensor product, with some links to previous work

[Eric Wieser]

Regarding exterior powers:

• we have them today as LinearMap.range (ι R : M →ₗ[R] ExteriorAlgebra R M) ^ i, but that's obviously not very convenient
• probably we want them as a a quotient of docs#TensorPower
• I think @Amelia Livingston has some work on them in https://github.com/leanprover-community/mathlib/tree/koszul_cx

[Sophie Morel]

Antoine Chambert-Loir said:

Even if you choose a basis, what norm will you choose on ‘Fin r to k‘?

Lean does it for me, it's the sup norm:
https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/NormedSpace/Basic.html#Pi.normedSpace
(And it's an instance, so if I did something else it would require extra effort.)

[Heather Macbeth]

Sebastien Gouezel said:

I don't think we have anything serious there. Maybe Yury G. Kudryashov or Heather Macbeth have something more on a branch, towards de Rham cohomology, but not PRed yet if I understand correctly.

Yury and I have avoided this issue by working with the antisymmetric k-multilinear maps from V rather than the k-th exterior power of V-dual. And FWIW, I've come to think of this not as a formalization hack but as a reflection of mathematical reality ...

[Yury G. Kudryashov]

Indeed, this way we don't have to assume [FiniteDimensional] here and there.

[Yury G. Kudryashov]

The project is on hold for now but we're going to CMU in November for a week to collaborate on it.

[Sophie Morel]

Okay, this is giving me some ideas. First, I need to generalize things a little bit from Fin r to general fintypes.

[Sophie Morel]

I think that all this really is an argument in favor of using the "algebraic geometry" Grassmannian, i.e. the set of dimension $r$ subspaces of the dual of $E$. I cannot say that I am displeased by this. :grinning_face_with_smiling_eyes:

[Yaël Dillies]

Sophie Morel said:

Okay, this is giving me some ideas. First, I need to generalize things a little bit from Fin r to general fintypes.

I am always in favour of this!