dual spaces

Stream: new members

[Fabian Glöckle]

Hello everyone, I am Fabian Glöckle, masters student at University of Freiburg, Germany. I just got excited for formal theorem proving, know some (graduate level) number theory and sheaf theory and will be happy to learn and join in the movement! Currently, I am working with @Johan Commelin on a small file about dual vector spaces.

[Patrick Massot]

Last time Johan mentioned dual vector spaces he seemed pretty depressed. Is it better now? It's a pretty important topic

[Fabian Glöckle]

Yes, we could prove that for finite dimensional vector spaces, a basis induces an isomorphism from the vector space to its dual. The proofs are a bit lengthy though and may need some refactoring before going to the library. I think we should also include the canonical injection into the bidual space into the file, this yet has to be done.

[Kevin Buzzard]

It seemed to me that for finite-dimensional spaces, people often think of a basis as a sequence (so order matters), whereas for infinite-dimensional spaces they often think of a basis as a subset. The behaviour of dual spaces depends on whether the space is finite-dimensional or not -- you have basic observations about the dual space which work in general, but then these extra facts coming from the fact that duality is an equivalence of categories for the category of finite-dimensional spaces but this is no longer true for general spaces. So will you make the general theory for general spaces and then put extra theorems in under a finite-dimensionality hypothesis? I guess this is the way to go. Is there an ordered_basis for a finite-dimensional space? The dual of a finite-dimensional space with an ordered basis naturally gets an ordered basis -- usually called "the dual basis" but now I see it could really be called the dual ordered basis.

[Fabian Glöckle]

Yes, we are aiming at both the basis-free theorems that work in general and the dual basis approach in the finite-dimensional case, and their relationship.
If mathlib currently does not make use of ordered bases, we will not start that now; however, there is the map taking a basis vector to its corresponding dual basis vector (which could then be used to transport an order on the first onto the latter).

[Mario Carneiro]

One thing I would like to look into is porting the stuff about bases to families of elements rather than subsets of the vector space. You get ordered bases for free this way if the index type happens to be ordered