## 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?

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

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