Identify span of vector with field

Stream: Is there code for X?

[Heather Macbeth]

I have some draft code for the topological dual of a normed space, including the corollary of Hahn-Banach needed for the isometric inclusion in the double dual. (Hopefully this is not stepping on @Yury G. Kudryashov 's toes.) For the Hahn-Banach corollary, I wrote out many, many facts which might well exist already, somewhere in the linear algebra libraries. Summary to follow. Any pointers?

[Heather Macbeth]

Summary: If E is a vector space over 𝕜 and x is a nonzero element, we can identify span x with 𝕜. Moreover, if E is a normed space, this identification preserves norms.

[Heather Macbeth]

I rolled-my-own span for now, because I could not find a library entry for the natural map from 𝕜 to span x.

[Johan Commelin]

Couldn't you reuse the existing span, but add the natural map?

[Yury G. Kudryashov]

derivs use linear_map.id.smul_right x for span_map. Possibly we should have a def for this.

[Yury G. Kudryashov]

Instead of using def span please add lemma span_map_range : range (span_map x) = span {x}.

[Yury G. Kudryashov]

I'm not going to formalize any corollaries of Hahn-Banach in the nearest future.

[Heather Macbeth]

Great, I will do this tomorrow. I will put span_map and friends in linear_algebra.basic, and perhaps the facts about the norm-preserving properties of span_map belong in normed_space.basic. Any opinions on conventionalizing the names? The maps needing baptism are span_map, its linear_equiv version (currently span_equiv), its inverse (currently coord), and its inverse considered as a bounded linear map (currently coord_bdd).

[Yury G. Kudryashov]

I have no ideas. @Sebastien Gouezel ?

[Johan Commelin]

It would be good if we could think of something that will also give the natural map for span {x,y}

[Johan Commelin]

But everything I can think of becomes ugly

[Heather Macbeth]

Yes, absolutely. Please tell me if you think of something! I will pick it up tomorrow.