Commit 2023-12-27 12:26 120ddecb

feat: OrderIso between finite-codimensional subspaces and finite-dimensional subspaces in the dual (#9124)

Introduce the nondegenerate pairing ((flip_)quotDualCoannihilatorToDual_injective) between M ⧸ W.dualCoannihilator and W . If M is a vector space and W is a finite-dimensional subspace of its dual, this is a perfect pairing (quotDualCoannihilatorToDual_bijective), and W is equal to the annihilator of its coannihilator.
Use this pairing to show that dualAnnihilator and dualCoannihilator give an antitone order isomorphism orderIsoFiniteCodimDim between finite-codimensional subspaces in a vector space and finite-dimensional subspaces in its dual. This result can be e.g. found in Bourbaki's Algebra. For a finite-dimensional vector space, this gives an OrderIso between all subspaces and all subspaces of the dual.
Add some lemmas about the image and preimage of annihilators and coannihilators under Dual.eval.
Expand the docstring of basis_finite_of_finite_spans with comments on generalizations.