mem.span

Stream: Is there code for X?

[Scott Morrison]

(The linear algebra code makes me so sad...)

I have x ∈ submodule.span R S for some S : set M, and module R M.

How to I obtain a formula for x as a linear combination of finitely many elements of S? (Ideally in a way that it's then convenient to do induction on the size of that linear combination?)

[Scott Morrison]

I feel like grepping for linear combination should reveal this, but ...

[Scott Morrison]

The fact that the word "combination" doesn't even appear in linear_algebra.basic seems worrying.

[Johan Commelin]

Isn't there something like finsupp.total or something like that?

[Markus Himmel]

Does docs#submodule.span_induction help?

[Anne Baanen]

This is called docs#finsupp.mem_span_iff_total

[Anne Baanen]

finsupp.total does mention the words "linear combination" in its docstring, by the way :)

[Scott Morrison]

But even this has some business about an image of a set v '' s...

[Scott Morrison]

I have to make my set look like that? :-(

[Scott Morrison]

It seems submodule.span_induction will work smoothly for me.

[Adam Topaz]

I got frustrated with something like this a little while ago for another project I was working on, and ended up proving this

https://github.com/adamtopaz/comb_geom/blob/e16b629d6de3fbdea54a528755e7305dfb51e902/src/linear_algebra/lincomb.lean#L145

I could try to clean it up and integrate it into mathlib with a small PR if people think it is actually useful.

[Filippo A. E. Nuccio]

Has this finally got merged into mathlib?

[Adam Topaz]

No :(
It's still unclear what form of this should belong in mathlib (if at all!)

[Adam Topaz]

I guess some general stuff about linear combinations (defined as lists as in the above link) should also be added.

[Filippo A. E. Nuccio]

Ah, that's a pity. I am trying to build a proof using that every element in a product of modules is a linear combination and your file would be extremely useful.

[Adam Topaz]

I think this docs#finsupp.mem_span_iff_total is the way to do such things with what's in mathlib, as the above comments suggest.

[Filippo A. E. Nuccio]

Yes, I saw it. Your file looks much more transparent to me, though. Thanks again for the ref, at any rate.

[Adam Topaz]

Filippo A. E. Nuccio said:

Yes, I saw it. Your file looks much more transparent to me, though. Thanks again for the ref, at any rate.

I agree, of course.

[Filippo A. E. Nuccio]

Following the above discussion with @Adam Topaz , I was thinking about creating a lemma to the effect that the product of two ideals (or two R-submodules contained in a R-algebra A) consists of all linear combinations of products of an element of the first module times an element of the second module. But of course I don't want to reinvent the wheel, so I would like to double check that this does not exist already.

[Johan Commelin]

I think linear combinations need some love. I don't know exactly what, but whatever we have at the moment in mathlib is just not very intuitive to use.

[Johan Commelin]

But I don't have the time to experiment with this.

[Johan Commelin]

Probably it's not something that you get right at the first attempt. So maybe we just need several people to try things out. And hopefully it will converge to something useful.

[Filippo A. E. Nuccio]

I see. I will write down something for the above result, then, and we'll see if it is somehow useful.

[Filippo A. E. Nuccio]

At any rate, my impression with @Adam Topaz 's file is that it was useful and very nice. Yet (unless I misread it) it still does not immediately contain the result about products of sub-modules that I was referring to.

[Adam Topaz]

Personally I think defining linear combinations as lists (as in the above file) is very intuitive

[Mario Carneiro]

Johan Commelin said:

I think linear combinations need some love. I don't know exactly what, but whatever we have at the moment in mathlib is just not very intuitive to use.

As one of the authors of this part of the library I would be interested to know what the pain points are

[Mario Carneiro]

I think that finsupp is actually the mathematically correct way to represent the type of linear combinations, because unlike lists they have the right equality relation

[Adam Topaz]

how would you represent a linear combination where two of the vectors are the same?

[Mario Carneiro]

{v1 * (a - b)}?

[Mario Carneiro]

You can always express a linear combination as (l.map (\lam (vi, ai), finsupp.single vi ai)).sum where l is a list of vectors and coefficients that is not necessarily injective in the vi

[Mario Carneiro]

the summing of finsupps handles the job of putting all the coefficients of some fixed v into the same bucket

[Adam Topaz]

Okay. That's one point that's not intuitive for me.

[Adam Topaz]

Of course, I agree this can be done with finsupp, but I think representing them as lists is much closer to what I think of as a linear combination mathematically.

[Mario Carneiro]

The finsupp is just the normal form

[Mario Carneiro]

just like how polynomial only represents the polynomials in normal form

[Filippo A. E. Nuccio]

In particular, as a mathematician, the set over which I sum is often "irrelevant". I fully appreciate that it cannot be really irrelevant, but my impression is that this aspect plays a major role in finsupp.

[Mario Carneiro]

if you have a list, you can sum the list

[Adam Topaz]

But two polynomials are equal if and only if their coefficients are the same, and this is not true for the finsupp representation of linear combinations

[Mario Carneiro]

it is

[Adam Topaz]

Why is 1 * v + 0 * v the same as 1 * v ?

[Adam Topaz]

one is a linear combination of two vectors, and the other is a linear combination of one vector

[Mario Carneiro]

Okay we're clearly having a miscommunication then

[Adam Topaz]

probably :)

[Mario Carneiro]

that's not a linear combination of two vectors

[Mario Carneiro]

that's a linear combination of one vector

[Adam Topaz]

Oh, I would say it's a linear comb of two vectors which just so happen to be the same

[Mario Carneiro]

The thing is, the finsupp allows you to pick a more abstract notion of indexing type than just the vectors themselves

[Mario Carneiro]

In fact, this was a problem in the early versions of the linalg library that needed a major refactor

[Adam Topaz]

Oh, I thought you were identifying linear combinations with funsupp functions from the module to the ring

[Filippo A. E. Nuccio]

So did I.

[Mario Carneiro]

That depends on your use case

[Mario Carneiro]

Usually, when you have a basis, the basis vectors are themselves given by I -> V where I is an abstract indexing set

[Adam Topaz]

If you define it as a funsupp from some index type \iota to R \times M, that would be great, but I dont think what exists in mathlib right now actually does this.

[Mario Carneiro]

so you want the linear combinations to instead be I ->0 R

[Adam Topaz]

This docs#finsupp.mem_span_iff_total is a good example

[Mario Carneiro]

If you look at docs#finsupp.total (which is the "forgetful functor" from linear combinations of vectors to vectors), you will see that there is an abstract indexing type alpha

[Adam Topaz]

Yeah, I see now

[Filippo A. E. Nuccio]

But what should I "normally" chose as alpha? Nat?

[Mario Carneiro]

That depends on where the vectors come from

[Reid Barton]

Is this how finsupp.total was always defined?

[Mario Carneiro]

no

[Mario Carneiro]

It was once the way Adam said, V ->0 R

[Filippo A. E. Nuccio]

Mario Carneiro said:

That depends on where the vectors come from

Well, in my case at hand they are all elements of a ring, I am trying to say that every element of I * J (both ideals in R) is a linear combination of things, one from I and the other from J.

[Mario Carneiro]

As in, just two things?

[Mario Carneiro]

For that you don't need linear combinations at all, you just write a * x + b * y

[Filippo A. E. Nuccio]

Well, no, they are of the form $\sum _{i \in A} x_i * y_i$ for some (finite) $A$

[Adam Topaz]

That's the thing, with this finsupp formulation it's so cumbersome to state facts like "every element in the span of a set is a linear combination of the elements of the set"

[Mario Carneiro]

you can still do that though?

[Filippo A. E. Nuccio]

Same thing for the generic element of $M\otimes N$.

[Mario Carneiro]

if you really want to put in I = V you can

[Mario Carneiro]

@Filippo A. E. Nuccio what's the type of A

[Mario Carneiro]

Oh I understand now

[Filippo A. E. Nuccio]

Mario Carneiro said:

Filippo A. E. Nuccio what's the type of A

A finite subset of $\mathbb{N}$, typically (at least in my mind, I can come up with more complicated things; for instance I can index them over all elements in $R$)

[Mario Carneiro]

I think the indexing set in your example is ↑I × ↑J

[Mario Carneiro]

if you have a #mwe I can make something that typechecks

[Filippo A. E. Nuccio]

Mario Carneiro said:

I think the indexing set in your example is ↑I × ↑J

Possibly; but a part from being potentially very huge it seems hard to compare it with elements in $I*J$ *which I can see as $\mathrm{Span}(I*J)$ and would be indexed on $I*J$ (product of ideals, not cartesian product).

[Mario Carneiro]

being potentially very huge

It's just the index set, the range of possibilities for the vectors. These are usually infinite

[Filippo A. E. Nuccio]

For the https://leanprover-community.github.io/mwe.html: Well, I don't have it yet... I was figuring out how to prove my claim that every element of the product can be written in that way, and got lost in finsupp (with all the due respect, as I would have been totally incapable of coming up with anything, so no criticism at all is meant here)

[Mario Carneiro]

I mean if you can provide something with the context of your problem

[Mario Carneiro]

like imports and variables

[Filippo A. E. Nuccio]

Sure, give me a sec.

[Reid Barton]

docs#submodule.span_smul_span is pretty close to your statement

[Reid Barton]

since if I : ideal R then I = ideal.span (I : set R)

[Filippo A. E. Nuccio]

Reid Barton said:

docs#submodule.span_smul_span is pretty close to your statement

Indeed, it is. I was starting from there to try to construct the proof, but got a bit lost and begun wondering if what I was doing was worth it.

[Mario Carneiro]

Yeah I was going to point out next that this combination doesn't look very linear because there is no coefficient

[Reid Barton]

You don't need a coefficient because $2 \ge 1$--but it might be better to allow one anyways for uniformity

[Reid Barton]

If you multiply together n ideals then you need to allow a coefficient from R when n=0

[Mario Carneiro]

In that case, I would want to go for a more inductive formulation: if I = ideal.span (set.range a) and J = ideal.span (set.range b) then I * J = ideal.span (set.range (\lam (i,j), a i * b j)

[Filippo A. E. Nuccio]

This seems very nice, and I can take a = (I : set R) and b = (J : set R)

[Reid Barton]

Filippo, I'm curious what you intend to do next after applying this statement about linear combinations--normally I think the span formulation would be better

[Filippo A. E. Nuccio]

Reid Barton said:

Filippo, I'm curious what you intend to do next after applying this statement about linear combinations--normally I think the span formulation would be better

Well, I'm trying to prove the statement that for an invertible module M, M * (1 / M ) \le 1. Which is immediate if I can take an element in M * 1/M and write it as a linear combination $\sum x_i y_i$ with $x_i\in M$ and $y_i \in 1/M$, so that $x_iy_i\in R$ by definition of $1/M$

[Reid Barton]

Then you don't want to deal with linear combinations explicitly

[Filippo A. E. Nuccio]

Well, what do you mean by "explicitely"?

[Reid Barton]

just use the fact that if M is an R-submodule of something and S \sub M then span S \sub M

[Reid Barton]

I mean you don't need to mention things like finsupp.total

[Johan Commelin]

apply submodule.span_le

[Johan Commelin]

assuming that M * (1/M) is defined as a span (which I think it is).

[Reid Barton]

You can use the "universal algebra-style" characterization of the span (i.e. linear combinations) of S as the smallest ideal/submodule containing S

[Filippo A. E. Nuccio]

Well, that's what I was trying to do, but could not understand how to use the definition of the product to come up with elements.

[Filippo A. E. Nuccio]

This is what I read:

instance : has_mul (submodule R A) :=
⟨λ M N, ⨆ s : M, N.map $ algebra.lmul R A s.1⟩

[Reid Barton]

I agree the definition of the product is less convenient (though you could presumably do a similar argument with it)

[Mario Carneiro]

docs#ideal.mul_le

[Reid Barton]

i.e., it's a ⨆ so to prove it's \le 1 means to prove each summand is \le 1

[Johan Commelin]

Mario Carneiro said:

docs#ideal.mul_le

This doesn't work, I guess. because it's not about ideals.

[Mario Carneiro]

What is the type of anything?

[Filippo A. E. Nuccio]

Exactly, it's about submodules in a R-algebra

[Mario Carneiro]

#mwe please

[Filippo A. E. Nuccio]

both are submodules A R

[Filippo A. E. Nuccio]

Mario Carneiro said:

#mwe please

Working on it...

[Johan Commelin]

Can you use extract_goal to create the lemma that you want to prove?

[Mario Carneiro]

docs#submodule.mul_le

[Johan Commelin]

Then I can post a 5-line proof, and Mario will golf it into a 42-character proof

[Kevin Buzzard]

I was about to say the same as Reid. Consider how one might define the subgroup generated by a subset X of an abelian group A. I can think of three ways to do it.

1) intersection of all the subgroups of A that contain X

2) custom inductive type. Elements of X are in, 0 is in, sum of two elements which are in is in, negation of an element which is in, is in

3) something involving the image of some finsupp

[Filippo A. E. Nuccio]

Johan Commelin said:

Then I can post a 5-line proof, and Mario will golf it into a 42-character proof

Is this what you mean?

import algebra.algebra.basic

example {R : Type u} {A : Type v}
  [comm_semiring R]
  [comm_semiring A]
  [algebra R A]
  {I : submodule R A} :
  I * 1 / I ≤ 1 :=
begin
  admit,
end

[Mario Carneiro]

imports?

[Kevin Buzzard]

But what in practice does one want from these things? When I first learnt about inductive types etc I got super-excited about the idea of (2) and how the recursor was generated automatically and looked mathematically useful

[Kevin Buzzard]

But now more and more I am realising the power of (1). It's quite pleasant to prove things about definition (1)

[Filippo A. E. Nuccio]

But can you work with them "explicitely"? Or at least, would you admit it takes a bit to change our "usual" elements-based proofs into that language?

[Filippo A. E. Nuccio]

Which, of course, I am willing to...but still trying to learn.

[Mario Carneiro]

The idea behind having a big API is so that you can use any of (1) (2) or (3) depending on your current use case

[Kevin Buzzard]

You can construct the recursor yourself

[Filippo A. E. Nuccio]

What do you mean?

[Reid Barton]

right, in practice you want whichever one of the three is the most convenient in a given situation.
Textbooks in (say) commutative algebra will often use (3) everywhere even when using (1) is logically more efficient, because it costs so little to write $\sum_i x_i y_i$ on a page

[Mario Carneiro]

Your #mwe doesn't work

[Mario Carneiro]

Try copying it into a new file

[Mario Carneiro]

import algebra.algebra.operations
universes u v

example {R : Type u} {A : Type v}
  [comm_semiring R]
  [comm_semiring A]
  [algebra R A]
  {I : submodule R A} :
  I * 1 / I ≤ 1 :=
begin
  admit,
end

[Johan Commelin]

import algebra.algebra.operations

example {R A : Type*} [comm_semiring R] [comm_semiring A] [algebra R A] {I : submodule R A} :
  I * (1 / I) ≤ 1 :=
begin
  rw submodule.mul_le,
  intros m hm n hn,
  rw [submodule.mem_div_iff_forall_mul_mem] at hn,
  rw mul_comm,
  exact hn m hm,
end

[Johan Commelin]

5 lines, as promised

[Johan Commelin]

Note that I changed the import, and added (..) around 1 / I

[Filippo A. E. Nuccio]

Great, I tried for the whole morning... :silence:

[Kevin Buzzard]

Then inspect the proof carefully and figure out what you were missing

[Filippo A. E. Nuccio]

Sure, I will. Thanks.

[Kevin Buzzard]

As a beginner I would always unfold everything

[Kevin Buzzard]

And I have learnt more recently that whilst this teaches you a lot about how lean and type theory works

[Kevin Buzzard]

It is almost never the optimal way to prove things, because the way to prove things is to use the API

[Kevin Buzzard]

The way to prove things is to prove them mathematically and then to try and translate your 5 line maths proof into Lean

[Filippo A. E. Nuccio]

Well, that's what I was trying, but got stuck with my elements-based proof, as Reid said.

[Filippo A. E. Nuccio]

But I see your point, thanks.

[Kevin Buzzard]

My PhD student Ashvni made a short PR today about subalgebras and submodules and I think her proof was six lines long, and also used submodule.mul_le

[Kevin Buzzard]

Things like mul_le are great examples of the tricks that you can do when working with products of ideals

[Johan Commelin]

import algebra.algebra.operations

open submodule

example {R A : Type*} [comm_semiring R] [comm_semiring A] [algebra R A] {I : submodule R A} :
  I * (1 / I) ≤ 1 :=
mul_le.2 $ λ m hm n hn, (mul_comm n m) ▸ (mem_div_iff_forall_mul_mem.2 hn m hm)

80 chars... :worried:

[Kevin Buzzard]

The triangle works!

[Reid Barton]

4 of those ()s look unnecessary

[Reid Barton]

which is all of them I guess

[Johan Commelin]

Ooh, I don't need the parens... and I can rename hm and hn to h and H.

[Johan Commelin]

That's 72 chars

[Mario Carneiro]

example {R A : Type*} [comm_semiring R] [comm_semiring A] [algebra R A] {I : submodule R A} :
  I * (1 / I) ≤ 1 :=
mul_le.2 $ by finish [mem_div_iff_forall_mul_mem]

[Johan Commelin]

Is that 42?

[Mario Carneiro]

49

[Johan Commelin]

(deleted)

[Mario Carneiro]

by finish [mul_le, mem_div_iff_forall_mul_mem] is 47

[Johan Commelin]

and slow...

[Johan Commelin]

I guess we need to rename mem_div_iff_forall_mul_mem to something shorter :rofl:

[Mario Carneiro]

rfl

[Mario Carneiro]

I think it could just be mem_div_iff since it's the definition

[Johan Commelin]

That would even bring it below chars

[Johan Commelin]

What would happen if J and Lean had a child?

[Mario Carneiro]

L

[Johan Commelin]

We'd have seriously weird unicode symbols for tactics like finish

[Filippo A. E. Nuccio]

Mario Carneiro said:

example {R A : Type*} [comm_semiring R] [comm_semiring A] [algebra R A] {I : submodule R A} :
  I * (1 / I) ≤ 1 :=
mul_le.2 $ by finish [mem_div_iff_forall_mul_mem]

Thanks to both! I confess that while @Johan Commelin 's code was clear at first, now eveything seems less comprehensible. What does the $ mean (I see it everywhere, never dared to ask)?

[Johan Commelin]

foo $ bar x is the same as foo (bar x)

[Johan Commelin]

It just means "put parentheses around everything that follows me".

[Johan Commelin]

It doesn't even save us a character. But if you use it multiple times, then it avoids ending the line with )))))

[Filippo A. E. Nuccio]

Ah, ok!

[Kevin Buzzard]

The $ thing is a really cool trick. I read something about Pratt parsers and then it all made sense

[Filippo A. E. Nuccio]

Pratt parsers?

[Kevin Buzzard]

A $ B is literally defined to be A B but $ has precedence 1

[Kevin Buzzard]

In the UK we call it bidmas or bodmas

[Kevin Buzzard]

Pemdas in the US

[Kevin Buzzard]

It's about which operators to do first

[Adam Topaz]

$ is a Haskell thing right?

[Filippo A. E. Nuccio]

AH, go(ogle)t it!

[Kevin Buzzard]

Multiplication has higher priority than addition so we all know what a+b*c means

[Johan Commelin]

Adam Topaz said:

$ is a Haskell thing right?

It was a US thing before that (-;

[Kevin Buzzard]

$ literally means "do nothing, with priority 1" ie very low

[Kevin Buzzard]

You can write #print notation $ to see.

[Kevin Buzzard]

Compare with #print notation * which tells you multiplication has priority 70 or so

[Filippo A. E. Nuccio]

Kevin Buzzard said:

You can write #print notation $ to see.

Well, to see

_ `$`:1 _:0 := #1 #0

to which I still prefer your explanation...

[Kevin Buzzard]

So when lean is parsing everything, it leaves $ until last

[Kevin Buzzard]

https://xenaproject.wordpress.com/2019/01/20/a-word-on-bidmas/

[Kevin Buzzard]

mul_le is the universal property of product of ideals. If you use the universal property you don't have to get your hands dirty with elements

[Filippo A. E. Nuccio]

Right.

[Filippo A. E. Nuccio]

I'll have stuff to work on during my locked-down Sunday - thanks!

[Mario Carneiro]

Kevin Buzzard said:

$ literally means "do nothing, with priority 1" ie very low

It doesn't mean "do nothing", it means application, although adjacency (i.e. nothing) is also notation for application

[Kevin Buzzard]

This issue has come up again -- @Ashvni Narayanan has run into it. The proof that if all nonzero ideals are invertible in a comm ring R then R is Noetherian goes like this: Say $I$ is a non-zero ideal. Then $I\times I^{-1}=1$ so there exists $a_i\in I$ and $b_i\in I^{-1}$ such that $\sum_i a_i b_i = 1$ (a finite sum); multiplying both sides by an element of $I$ now shows that the $a_i$ generate $I$.

[Kevin Buzzard]

This time I don't immediately see how to use mul_le to get around this.

[Kevin Buzzard]

OK I think that there is a very natural proof of what Ashvni needs if we had the following weaker theorem: if $R$ is a ring and $M$ is an $R$-module (or semiwhathaveyou) and $S\subseteq M$ is a subset, and if $x$ is in span S then there's a finite subset $S'\subseteq S$ such that $x$ is in span S'. Do we have _this_? I can't spot it in mathlib.

[Kevin Buzzard]

This shouldn't be hard to prove using span_induction. Let's say this isn't in mathlib. Should we put in the version which has S' a finset or the version with S' a set which is also finite?

[Kevin Buzzard]

lemma submodule.mem_span_finset_of_mem_span (S : set M) (x : M) (hx : x ∈ span R S) :
  ∃ S' : finset M, (↑S' : set M) ⊆ S ∧ x ∈ span R (↑S' : set M) :=

I can prove this; is this the right form for mathlib?

[Mario Carneiro]

I would suggest using a finite set, because you only ever use it in the form (↑S' : set M). If the user wants it to be in that form then they can apply the theorem to unfold finite into that

[Kevin Buzzard]

Thanks. The proof was also nothing but coercions and I needed classical to take a union of two finsets (although perhaps I'll also need it to take a union of two finite sets)