Zulip Chat Archive

Stream: Is there code for X?

Topic: Linear combinations stay in a submodule


view this post on Zulip Sophie Morel (Jul 18 2020 at 15:39):

Is there a lemma in the library that says that a linear combination of elements of a submodule is still in the submodule ? I wanted to use that result when doing one of the lftcm2020 linear algebra exercises, but I only found submodule.sum_mem that works for a sum, and submodule.smul_mem that works for a scalar product. (There's a related result called finsupp.mem_span_iff_total that says that the span of a family if the set of its linear combinations, but you'd need to combine it with the fact that a submodule is the span of the family of all its elements. Also, it assumes that the base semiring is a ring for some reason, which I don't think is necessary.) Anyway, I ended up adding this in my local copy of module.lean :

lemma linear_combination_mem {t : finset ι} {f : ι → M} (r : ι → R) :
(∀ c ∈ t, f c ∈ p) → (∑ i in t, r i • f i) ∈ p :=
λ hyp, submodule.sum_mem _ (λ i hi, submodule.smul_mem _ _ (hyp i hi))

(Just after smul_mem_iff' on line 504. Here R is a semiring, M is a semimodule over R, ι is a type, p is a submodule of M.)

view this post on Zulip Anne Baanen (Jul 18 2020 at 16:00):

I don't believe this lemma existed yet - the model solution uses a combination of sum_mem and smul_mem as in your proof for linear_combination_mem.

view this post on Zulip Kevin Buzzard (Jul 18 2020 at 16:18):

@Sophie Morel this would be a helpful PR and if you golf it a bit by changing : (∀ c ∈ t, f c ∈ p) → to (hyp : ∀ c ∈ t, f c ∈ p) : and deleting λ hyp, ("move as much as possible to the left of the colon") then it looks mathlib-ready. Do you have push rights to non-master branches of mathlib? If you don't know, then you probably don't -- what is your github login?

view this post on Zulip Johan Commelin (Jul 18 2020 at 17:03):

@Sophie Morel Also, small tip: if you want syntax highlighting in your Zulip posts, then you can use #backticks like so

```
lean code goes here
```

view this post on Zulip Sophie Morel (Jul 18 2020 at 17:21):

@Johan Commelin Thanks !

view this post on Zulip Sophie Morel (Jul 18 2020 at 17:21):

@Kevin Buzzard, do you mean something like this :

lemma linear_combination_mem {t : finset ι} {f : ι  M} (r : ι  R)
    (hyp :  c  t, f c  p) : ( i in t, r i  f i)  p :=
submodule.sum_mem _ (λ i hi, submodule.smul_mem  _ _ (hyp i hi))

My github login is smorel394, and I am pretty confident that I don't have push rights to anything.

view this post on Zulip Kevin Buzzard (Jul 18 2020 at 17:22):

@maintainers could Sophie have push rights to non-master branches of mathlib?

view this post on Zulip Kevin Buzzard (Jul 18 2020 at 17:23):

Yes that looks great. A three line PR adding a missing lemma in an appropriate place is the best kind of PR. The maintainers have a better eye than I do however

view this post on Zulip Chris Hughes (Jul 18 2020 at 17:24):

Kevin Buzzard said:

@maintainers could Sophie have push rights to non-master branches of mathlib?

Done

view this post on Zulip Sophie Morel (Jul 18 2020 at 17:32):

@Kevin Buzzard @Chris Hughes Thank ! I'll try to figure out the git stuff after dinner. (Scott told me about this page https://leanprover-community.github.io/contribute/index.html, so I should be ok.)


Last updated: May 16 2021 at 05:21 UTC