# Zulip Chat Archive

## 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):

`deriv`

s 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