Zulip Chat Archive

Stream: Is there code for X?

Topic: linear map of subspace ne top


view this post on Zulip 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?

view this post on Zulip Yury G. Kudryashov (Feb 06 2021 at 01:55):

upd: f ≠ 0

view this post on Zulip Heather Macbeth (Feb 06 2021 at 02:27):

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

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Feb 06 2021 at 02:30):

It's a purely algebraic fact.

view this post on Zulip Yury G. Kudryashov (Feb 06 2021 at 02:31):

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

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Feb 06 2021 at 02:39):

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

view this post on Zulip Adam Topaz (Feb 06 2021 at 02:40):

Oh.

view this post on Zulip Heather Macbeth (Feb 06 2021 at 02:41):

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

view this post on Zulip Yury G. Kudryashov (Feb 06 2021 at 02:45):

I'll prove it using docs#linear_map.exists_left_inverse_of_injective

view this post on Zulip 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