submodule span of a subset is finite linear combinations

Stream: Is there code for X?

[Kevin Buzzard]

Let $R$ be a commutative ring, let $M$ be an $R$-module, and let $S\subseteq M$ be a subset. The submodule submodule.span R S, a.k.a. the $R$-span of $S$ within $M$ can be defined abstractly as the intersection of all the submodules of $M$ containing $S$. Occasionally we get people asking how to prove the standard "formula" for the span known and loved by mathematicians the world over, namely that an element of the span is simply a finite $R$-linear combination of elements of $S$. Whenever this question comes up, me or someone else usually says "whatever you think you need this for, you might find it easier to just prove what you want using submodule.span_induction."

Today I've run into a situation where I can't figure out how to use submodule.span_induction, so my question is whether we actually do have anything of the following form (I'm flexible with the exact form, below is two examples):

import linear_algebra.basic

variables (R : Type*) [comm_ring R] [M : Type*] [add_comm_group M] [module R M]

lemma submodule.mem_span_iff_finset_sum (S : set M) (m : M) :
  m ∈ submodule.span R S ↔
  ∃ (F : finset S) (φ : S → R), F.sum (λ s, φ s • s.1) = m :=
begin
  sorry
end

lemma submodule.mem_span_iff_finset_sum' (S : set M) (m : M) :
  m ∈ submodule.span R S ↔
  ∃ (F : finset M) (φ : M → R), (F : set M) ⊆ S ∧ F.sum (λ s, φ s • s) = m :=
begin
  sorry
end

I could certainly prove them myself (using submodule.span_induction), I just want to check they're not there already.

---

The reason I need them is the following. Say $R$ is an internally graded ring, i.e. $R$ has subgroups $R_a$ indexed by a : A with A an add_comm_group such that $R=\bigoplus_a R_a$ (this is mathematician's $=$ a.k.a. internal direct sum), with the axioms $1\in R_0$ and $R_aR_b\subseteq R_{a+b}$. One checks easily that $R_0$ is a subring and $R_a$ is an $R_0$-submodule of $R$. My claim is that if $M\subseteq R_a$ is a sub-$R_0$-module then $RM\cap R_a=M$ (here $RM$ is the $R$-span of $M$), and the $\subseteq$ inclusion can be proved by writing an element of the left hand side as $\sum_i r_im_i$, then taking the $$a$$th graded piece (which doesn't change the element) and observing that the sum collapses to $\sum_i (r_i)_0 m_i\in R_0M=M$.

[Johan Commelin]

There is finsupp.total or whatever it is called.

[Johan Commelin]

That's what you're supposed to use when you want to get your hands on a linear combination, I think.

[Eric Wieser]

Right, the lemma will almost certainly have docs#finsupp.total on the RHS

[Eric Wieser]

docs#finsupp.mem_span_iff_total ?

[Kevin Buzzard]

Aah wonderful, thanks! I was looking in the wrong namespace.

[Eric Wieser]

Perhaps if that's "the standard "formula" for the span known and loved by mathematicians" we should reference that lemma from the span docstring

[Kevin Buzzard]

I would reckon that in an undergraduate lecture introducing the span, the chances are that the definition given would be finite linear combinations. Certainly I remember in UG ring theory being told that the definition of the product of two ideals $IJ$ was finite sums of elements $ij$ and spending some time thinking about it afterwards (convincing myself, for example, that the set $\{ij:i\in I, j\in J\}$ was not in general an ideal).

[Anne Baanen]

You have to squint a bit, but that definition corresponds to docs#finsupp.span_eq_map_total: finsupp.supported R R s is the set of all finite coefficients indexed by s, and finsupp.total turns a family of coefficients into a linear combination.

[Scott Morrison]

I've always found finsupp.total does not fit well in the existing linear algebra slots in my brain, and I struggle to understand any statement involving it. :-(

[Scott Morrison]

I guess I have to squint harder...

[Anne Baanen]

It's not (yet?) intuitive for me either :(

[Mario Carneiro]

The definition of linear combinations and linear independence used to be a lot more complicated. Once I understood finsupp.total and the free module it was a real eye opener, so many things are easier to state using it. It's like filters in topology

[Anne Baanen]

By the way, I am considering that we could redefine span as the set of all linear combinations. If we instantiate it early enough, the galois insertion with set should allow us to derive the complete lattice structure on submodules for free.

[Mario Carneiro]

Isn't span currently using the "easy" definition using the lattice structure already?

[Anne Baanen]

Yes

[Anne Baanen]

But we could also have the lattice structure derive from span

[Mario Carneiro]

how is it defined now?

[Anne Baanen]

first docs#submodule.has_inf and docs#submodule.has_Inf, then constructing all fields from those: https://github.com/leanprover-community/mathlib/blob/5a91d05e3b457aac6f656f8b02acb893f96341fa/src/algebra/module/submodule_lattice.lean#L106

[Mario Carneiro]

we probably want to retain the definitions for top, bot and inf since those are easy, but we can do without the others

[Mario Carneiro]

It looks like the general principle being used here is that a moore algebra aka closure system is a complete lattice

[Anne Baanen]

OTOH, deriving them from the galois insertion should give us a full API on how they combine with span

[Mario Carneiro]

I don't see linear combinations coming up in that definition at all though, so I don't think that a definition of span using linear combinations will make span + complete lattice structure easier on the whole

[David Wärn]

finsupp.total is 'just' one direction of $\textup{Hom}_R( R^{\oplus A}, M) \cong M^A$ right?

[Anne Baanen]

We had a thread a couple days ago about this topic, btw: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Closure.20operators

[Kevin Buzzard]

For what it's worth, I just seem to have spent 15 minutes changing my m \in submodule.span R [thing] to m \in submodule.span R (set.image thing thing) so I could rewrite with this lemma :-)

[Eric Wieser]

Just take the image by id ;)

[Kevin Buzzard]

If that's the right answer then I claim that that finsupp.span_eq_map_total is not correctly stated, or at least there should be another version where one doesn't have to do this? I didn't do this anyway, I was taking the span of something which could reasonably be re-interpreted as an image after some kerfuffle.

[Eric Wieser]

I think the docs#finsupp.mem_span_iff_total lemma should probably be called finsupp.mem_span_image_iff_total

[Eric Wieser]

And then we can take the original name for the version when v = id