# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: linear map of subspace ne top

#### Yury G. Kudryashov (Feb 06 2021 at 01:54):

Do we have `∀ (p : subspace K V) (hp : p ≠ ⊤), ∃ f : V →ₗ[K] K, p ≤ ker f`

?

#### Yury G. Kudryashov (Feb 06 2021 at 01:55):

upd: `f ≠ 0`

#### Heather Macbeth (Feb 06 2021 at 02:27):

Can you use docs#exists_extension_of_le_sublinear (which you wrote :wink: )?

#### Heather Macbeth (Feb 06 2021 at 02:30):

Let `v`

be a vector not in `p`

; construct a linear map `f : span K (p ∪ v) →ₗ[K] K`

which kills `p`

and sends `v`

to 1. Use the theorem to extend this to a `g : V →ₗ[K] K`

with the same properties.

#### Yury G. Kudryashov (Feb 06 2021 at 02:30):

It's a purely algebraic fact.

#### Yury G. Kudryashov (Feb 06 2021 at 02:31):

I can prove it. I was not sure that it is not in `mathlib`

#### Adam Topaz (Feb 06 2021 at 02:37):

Does mathlib have the fact that a nontrivial vector space has a nontrivial linear map to the field? If so, you can use that and factor through the quotient by `p`

.

#### Yury G. Kudryashov (Feb 06 2021 at 02:39):

I'm not sure that we have `nontrivial p.quotient <-> p \ne \top`

#### Adam Topaz (Feb 06 2021 at 02:40):

Oh.

#### Heather Macbeth (Feb 06 2021 at 02:41):

Nor, for that matter, that `nontrivial V`

implies `nontrivial (module.dual K V)`

.

#### Yury G. Kudryashov (Feb 06 2021 at 02:45):

I'll prove it using docs#linear_map.exists_left_inverse_of_injective

#### Yury G. Kudryashov (Feb 06 2021 at 02:45):

And

```
/-- Any linear map `f : p →ₗ[K] V'` defined on a subspace `p` can be extended to the whole
space. -/
lemma linear_map.exists_extend {p : submodule K V} (f : p →ₗ[K] V') :
∃ g : V →ₗ[K] V', g.comp p.subtype = f :=
let ⟨g, hg⟩ := p.subtype.exists_left_inverse_of_injective p.ker_subtype in
⟨f.comp g, by rw [linear_map.comp_assoc, hg, f.comp_id]⟩
```

Last updated: May 16 2021 at 05:21 UTC