## Stream: Is there code for X?

### Topic: Identify span of vector with field

#### Heather Macbeth (Jun 08 2020 at 03:47):

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 (Jun 08 2020 at 03:47):

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 (Jun 08 2020 at 03:51):

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 (Jun 08 2020 at 04:23):

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

#### Yury G. Kudryashov (Jun 08 2020 at 04:35):

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

#### Yury G. Kudryashov (Jun 08 2020 at 04:36):

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

#### Yury G. Kudryashov (Jun 08 2020 at 04:38):

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

#### Heather Macbeth (Jun 08 2020 at 05:02):

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 (Jun 08 2020 at 05:03):

I have no ideas. @Sebastien Gouezel ?

#### Johan Commelin (Jun 08 2020 at 05:07):

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

#### Johan Commelin (Jun 08 2020 at 05:07):

But everything I can think of becomes ugly

#### Heather Macbeth (Jun 08 2020 at 05:08):

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

Last updated: May 07 2021 at 22:14 UTC