linear map of subspace ne top

Stream: Is there code for X?

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

upd: f ≠ 0

[Heather Macbeth]

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

[Heather Macbeth]

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]

It's a purely algebraic fact.

[Yury G. Kudryashov]

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

[Adam Topaz]

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]

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

[Adam Topaz]

Oh.

[Heather Macbeth]

Nor, for that matter, that nontrivial V implies nontrivial (module.dual K V).

[Yury G. Kudryashov]

I'll prove it using docs#linear_map.exists_left_inverse_of_injective

[Yury G. Kudryashov]

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]⟩