exists_extends of linear_pmap

Stream: Is there code for X?

[Moritz Doll]

I want to define a linear map, which takes some (fixed) value on a given non-zero vector. I found linear_pmap.mk_span_singleton, which gives the partially defined map and linear_map.exists_extend which does the extension, but it seems awfully convoluted to prove
f := classical.some (linear_pmap.mk_span_singleton x y _).to_fun.exists_extend satisfies f x = y. It feels like I am not doing the correct thing here, is there a better way to do this?

[Kevin Buzzard]

You could extend to a basis and send all basis elements to the fixed value and then extend linearly

[Moritz Doll]

I thought there might something like that already for linearly independent sets.

[Kevin Buzzard]

docs#linear_map.exists_extend

[Kevin Buzzard]

I would just use classical.some and immediately use classical.some_spec to get the API for the classical.some; you can take it from there.

[Kevin Buzzard]

My basis idea, you'll still need classical.some to get the basis so it's no better

[Kevin Buzzard]

classical.some is one of these things which is much easier to use once you've figured out the trick, which is to let f := classical.some h and then to immediately write have hf : P f := classical.some_spec h where h : ∃ g, P g.

[Kevin Buzzard]

Then you have everything you need with hf and never need to write classical.some or start guessing what an underscore stands for ever again

[Kevin Buzzard]

Does this solve your problem?

[Moritz Doll]

I did not get it to work yet, but it certainly helps.

[Kevin Buzzard]

lol mk_span_singleton seems to have 0 API!

[Yaël Dillies]

You better not have a look at docs#DFA then :grinning:

[Kevin Buzzard]

import linear_algebra.basis

variables (k : Type) [field k] {V W : Type} [add_comm_group V] [module k V]
  [add_comm_group W] [module k W] {v : V} (hv : v ≠ 0) (w : W)

-- seems to be missing; this should be in mathlib.

lemma linear_pmap.mk_span_singleton_apply' :
  (linear_pmap.mk_span_singleton v w hv).to_fun ⟨v, (submodule.mem_span_singleton_self v : v ∈ submodule.span k {v})⟩ = w :=
begin
  convert linear_pmap.mk_span_singleton_apply v w _ (1 : k) _;
  simp [submodule.mem_span_singleton_self],
end

-- your function
noncomputable def f  : V →ₗ[k] W :=
classical.some (linear_map.exists_extend (linear_pmap.mk_span_singleton v w hv).to_fun)

-- immediately make the proof
lemma f_spec : (f k hv w).comp (k ∙ v).subtype = (linear_pmap.mk_span_singleton v w hv).to_fun :=
classical.some_spec (linear_map.exists_extend (linear_pmap.mk_span_singleton v w hv).to_fun)

-- now it's not so bad
example : (f k hv w) v = w :=
begin
  have h := f_spec k hv w,
  rw linear_map.ext_iff at h,
  specialize h ⟨v, submodule.mem_span_singleton_self v⟩,
  convert h,
  symmetry,
  apply linear_pmap.mk_span_singleton_apply',
end

[Kevin Buzzard]

@Moritz Doll

[Moritz Doll]

thank you so much

[Kevin Buzzard]

Thank you for your recent PRs.

[Reid Barton]

In a tactic block you can also use tactic#choose to get f and f_spec at once, even when (as here) there aren't any foralls involved.

[Kevin Buzzard]

In fact the docstring for choose is somehow way too complex; it never showcases the simplest use case, which is proving that a surjection has a one-sided inverse; it's on my job list to make a PR adding that example. All the examples have two \forall s, I thought the base case was one but I've just learnt that in fact it's zero :-)