getting a linear map from a span

Stream: Is there code for X?

[Ashvni Narayanan]

This is just an idea, I think it should be accurate. If I want to construct a linear map f : A -> B, on a submodule A, and if I have A to be a span of a set s (finite, in my case), then as long as f satisfies the relations between the generators, defining f on s should be sufficient. Is there any preexisting code for this?

[Adam Topaz]

If S is a set in a module M and N is any other module, you can look at the free module on S, call it F. Linear maps from F to N correspond to functions S to N, which we have as docs#finsupp.total

The inclusion S in M induces a linear map F to M whose image is the span of S by docs#finsupp.span_eq_range_total and the kernel of this map is exactly the "relations" that you mention. So now you can probably combine with with docs#submodule.liftq to get something close to what you're looking for.

[Adam Topaz]

In any case, it would be worthwhile to combine all of these ingredients to obtain the description you're after

[Adam Topaz]

This is helpful too: docs#linear_map.quot_ker_equiv_range

[Anne Baanen]

You could use something like docs#basis.constr on the basis of span s that is a subset of s

[Adam Topaz]

Well, span S need not have a basis in general

[Anne Baanen]

Oh yeah, forgot we're dealing with submodules, not subspaces. Sorry!

[Adam Topaz]

Maybe Ashvni is working over a field, in which case using such a basis would certainly simplify things!

[Ashvni Narayanan]

Thanks, @Adam Topaz and @Anne Baanen , they're useful suggestions! Unfortunately I am not working over a field :(. I could restrict to that case but I would prefer not to, if possible.

[Eric Wieser]

Do you have a lean statement for your question in mind, or is stating what you want itself proving troublesome?

[Adam Topaz]

Here's a sketch I came up with

import linear_algebra.finsupp

variables (R M N : Type*) [ring R] [add_comm_group M] [add_comm_group N]
  [module R M] [module R N] (S : set M)

noncomputable
def linear_map_from_span (η : S → N)
  (cond : ∀ (f : S →₀ R), finsupp.total S M R coe f = 0 → finsupp.total S N R η f = 0) :
  submodule.span R S →ₗ[R] N :=
begin
  let F := finsupp.total S M R coe,
  let K := F.ker,
  let e := linear_map.quot_ker_equiv_range F,
  let ee : F.range ≃ₗ[R] submodule.span R S :=
    linear_equiv.of_eq _ _ (finsupp.span_eq_range_total _ _).symm,
  refine linear_map.comp _ ee.symm.to_linear_map,
  refine linear_map.comp _ e.symm.to_linear_map,
  refine F.ker.liftq (finsupp.total S N R η) _,
  apply cond,
end

[Ashvni Narayanan]

Eric Wieser said:

Do you have a lean statement for your question in mind, or is stating what you want itself proving troublesome?

I had not given it much thought. It would be ideal if I could prove this, but there are alternative approaches to the (final) problem, I think.

[Ashvni Narayanan]

Adam Topaz said:

Here's a sketch I came up with

import linear_algebra.finsupp

variables (R M N : Type*) [ring R] [add_comm_group M] [add_comm_group N]
  [module R M] [module R N] (S : set M)

noncomputable
def linear_map_from_span (η : S → N)
  (cond : ∀ (f : S →₀ R), finsupp.total S M R coe f = 0 → finsupp.total S N R η f = 0) :
  submodule.span R S →ₗ[R] N :=
begin
  let F := finsupp.total S M R coe,
  let K := F.ker,
  let e := linear_map.quot_ker_equiv_range F,
  let ee : F.range ≃ₗ[R] submodule.span R S :=
    linear_equiv.of_eq _ _ (finsupp.span_eq_range_total _ _).symm,
  refine linear_map.comp _ ee.symm.to_linear_map,
  refine linear_map.comp _ e.symm.to_linear_map,
  refine F.ker.liftq (finsupp.total S N R η) _,
  apply cond,
end

This seems to work, thank you!