s subset M is spanning iff R^s -> M is surjective

Stream: Is there code for X?

[Kenny Lau]

import Mathlib.LinearAlgebra.Finsupp.LSum
import Mathlib.Algebra.Module.Submodule.Range
import Mathlib.LinearAlgebra.Span.Defs

open Submodule

lemma Finsupp.image_lift (R : Type*) [Semiring R] {M : Type*} [AddCommMonoid M] [Module R M]
    {X : Type*} (f : X → M) : LinearMap.range (lift M R X f) = span R (Set.range f) := by
  refine le_antisymm (LinearMap.range_le_iff_comap.2 <| eq_top_iff'.2 fun c ↦ ?_)
    (span_le.2 <| Set.range_subset_iff.2 fun x ↦ ⟨single x 1, by simp⟩)
  simpa using sum_mem fun c hc ↦ smul_mem _ _ (subset_span <| Set.mem_range_self c)

lemma Finsupp.lift_surjective_iff (R : Type*) [Semiring R]
    {M : Type*} [AddCommMonoid M] [Module R M] {X : Type*} (f : X → M) :
    Function.Surjective (lift M R X f) ↔ span R (Set.range f) = ⊤ := by
  rw [← LinearMap.range_eq_top, image_lift]

/-- `s` spans a module `M` iff the corresponding map from `s →₀ R` is surjective. -/
lemma Finsupp.lift_surjective_iff' (R : Type*) [Semiring R]
    {M : Type*} [AddCommMonoid M] [Module R M] (s : Set M) :
    Function.Surjective (lift M R s Subtype.val) ↔ span R s = ⊤ := by
  rw [lift_surjective_iff, Subtype.range_coe_subtype, Set.setOf_mem_eq]

[Kenny Lau]

Do we currently have this result? Let M be an R-module, and s a subset of M. Then s spans iff the map $R^{\oplus s} \to M$ is surjective

[Antoine Chambert-Loir]

This is essentially the content of docs#Finsupp.range_linearCombination
In any case docs#Finsupp.linearCombination is the linear map that you denote by $R^{\oplus s}\to M$.

[Kenny Lau]

aha, thanks! It's quite confusing that we have two names linearCombination and lift when they are the same thing.

[Kenny Lau]

docs#Finsupp.lift:

noncomputable def Finsupp.lift (M : Type u_2)
    (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M]
    (X : Type u_9) :
  (X → M) ≃+ ((X →₀ R) →ₗ[R] M)

docs#Finsupp.linearCombination:

def Finsupp.linearCombination {α : Type u_1}
    {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M]
    (v : α → M) :
  (α →₀ R) →ₗ[R] M

[Kevin Buzzard]

One is the bare function, the other is the additive equivalence. It's not uncommon to have things like this in mathlib I guess.

[Eric Wieser]

We have that the span is the range of the linear combination, and that the range is top iff surjective

[Eric Wieser]

@loogle LinearMap.range, Submodule.span

[Eric Wieser]

@loogle LinearMap.range, Submodule.span

[loogle]

:search: LinearMap.range_toSpanSingleton, LinearMap.span_singleton_eq_range, and 42 more

[Eric Wieser]

docs#Finsupp.span_eq_range_linearCombination

[Eric Wieser]

Kevin Buzzard said:

One is the bare function, the other is the additive equivalence. It's not uncommon to have things like this in mathlib I guess.

As long as the bare function is simp normal