Zulip Chat Archive

Stream: Is there code for X?

Topic: mem.span


Scott Morrison (Sep 08 2020 at 10:51):

(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 (Sep 08 2020 at 10:51):

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

Scott Morrison (Sep 08 2020 at 10:52):

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

Johan Commelin (Sep 08 2020 at 10:52):

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

Markus Himmel (Sep 08 2020 at 10:53):

Does docs#submodule.span_induction help?

Anne Baanen (Sep 08 2020 at 10:54):

This is called docs#finsupp.mem_span_iff_total

Anne Baanen (Sep 08 2020 at 10:57):

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

Scott Morrison (Sep 08 2020 at 11:03):

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

Scott Morrison (Sep 08 2020 at 11:04):

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

Scott Morrison (Sep 08 2020 at 11:06):

It seems submodule.span_induction will work smoothly for me.

Adam Topaz (Sep 08 2020 at 12:12):

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 (Oct 30 2020 at 17:21):

Has this finally got merged into mathlib?

Adam Topaz (Oct 30 2020 at 18:03):

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

Adam Topaz (Oct 30 2020 at 18:04):

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

Filippo A. E. Nuccio (Oct 30 2020 at 18:46):

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 (Oct 30 2020 at 18:50):

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 (Oct 30 2020 at 18:51):

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

Adam Topaz (Oct 30 2020 at 18:51):

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 (Oct 31 2020 at 17:46):

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 (Oct 31 2020 at 18:00):

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 (Oct 31 2020 at 18:01):

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

Johan Commelin (Oct 31 2020 at 18:01):

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 (Oct 31 2020 at 18:02):

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 (Oct 31 2020 at 18:02):

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 (Oct 31 2020 at 18:03):

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

Mario Carneiro (Oct 31 2020 at 18:05):

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 (Oct 31 2020 at 18:06):

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 (Oct 31 2020 at 18:07):

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

Mario Carneiro (Oct 31 2020 at 18:08):

{v1 * (a - b)}?

Mario Carneiro (Oct 31 2020 at 18:09):

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 (Oct 31 2020 at 18:10):

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

Adam Topaz (Oct 31 2020 at 18:11):

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

Adam Topaz (Oct 31 2020 at 18:11):

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 (Oct 31 2020 at 18:12):

The finsupp is just the normal form

Mario Carneiro (Oct 31 2020 at 18:12):

just like how polynomial only represents the polynomials in normal form

Filippo A. E. Nuccio (Oct 31 2020 at 18:12):

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 (Oct 31 2020 at 18:12):

if you have a list, you can sum the list

Adam Topaz (Oct 31 2020 at 18:13):

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 (Oct 31 2020 at 18:13):

it is

Adam Topaz (Oct 31 2020 at 18:13):

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

Adam Topaz (Oct 31 2020 at 18:14):

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

Mario Carneiro (Oct 31 2020 at 18:14):

Okay we're clearly having a miscommunication then

Adam Topaz (Oct 31 2020 at 18:14):

probably :)

Mario Carneiro (Oct 31 2020 at 18:14):

that's not a linear combination of two vectors

Mario Carneiro (Oct 31 2020 at 18:15):

that's a linear combination of one vector

Adam Topaz (Oct 31 2020 at 18:15):

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

Mario Carneiro (Oct 31 2020 at 18:15):

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

Mario Carneiro (Oct 31 2020 at 18:16):

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

Adam Topaz (Oct 31 2020 at 18:16):

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

Filippo A. E. Nuccio (Oct 31 2020 at 18:16):

So did I.

Mario Carneiro (Oct 31 2020 at 18:16):

That depends on your use case

Mario Carneiro (Oct 31 2020 at 18:17):

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

Adam Topaz (Oct 31 2020 at 18:17):

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 (Oct 31 2020 at 18:17):

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

Adam Topaz (Oct 31 2020 at 18:18):

This docs#finsupp.mem_span_iff_total is a good example

Mario Carneiro (Oct 31 2020 at 18:19):

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 (Oct 31 2020 at 18:19):

Yeah, I see now

Filippo A. E. Nuccio (Oct 31 2020 at 18:20):

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

Mario Carneiro (Oct 31 2020 at 18:20):

That depends on where the vectors come from

Reid Barton (Oct 31 2020 at 18:20):

Is this how finsupp.total was always defined?

Mario Carneiro (Oct 31 2020 at 18:20):

no

Mario Carneiro (Oct 31 2020 at 18:21):

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

Filippo A. E. Nuccio (Oct 31 2020 at 18:21):

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 (Oct 31 2020 at 18:22):

As in, just two things?

Mario Carneiro (Oct 31 2020 at 18:22):

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

Filippo A. E. Nuccio (Oct 31 2020 at 18:23):

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

Adam Topaz (Oct 31 2020 at 18:23):

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 (Oct 31 2020 at 18:24):

you can still do that though?

Filippo A. E. Nuccio (Oct 31 2020 at 18:24):

Same thing for the generic element of MNM\otimes N.

Mario Carneiro (Oct 31 2020 at 18:24):

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

Mario Carneiro (Oct 31 2020 at 18:24):

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

Mario Carneiro (Oct 31 2020 at 18:25):

Oh I understand now

Filippo A. E. Nuccio (Oct 31 2020 at 18:25):

Mario Carneiro said:

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

A finite subset of N\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 RR)

Mario Carneiro (Oct 31 2020 at 18:26):

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

Mario Carneiro (Oct 31 2020 at 18:26):

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

Filippo A. E. Nuccio (Oct 31 2020 at 18:28):

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 IJI*J *which I can see as Span(IJ)\mathrm{Span}(I*J) and would be indexed on IJI*J (product of ideals, not cartesian product).

Mario Carneiro (Oct 31 2020 at 18:29):

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 (Oct 31 2020 at 18:29):

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 (Oct 31 2020 at 18:30):

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

Mario Carneiro (Oct 31 2020 at 18:30):

like imports and variables

Filippo A. E. Nuccio (Oct 31 2020 at 18:31):

Sure, give me a sec.

Reid Barton (Oct 31 2020 at 18:31):

docs#submodule.span_smul_span is pretty close to your statement

Reid Barton (Oct 31 2020 at 18:32):

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

Filippo A. E. Nuccio (Oct 31 2020 at 18:32):

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 (Oct 31 2020 at 18:32):

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

Reid Barton (Oct 31 2020 at 18:33):

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

Reid Barton (Oct 31 2020 at 18:34):

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

Mario Carneiro (Oct 31 2020 at 18:36):

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 (Oct 31 2020 at 18:37):

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

Reid Barton (Oct 31 2020 at 18:37):

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 (Oct 31 2020 at 18:39):

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 xiyi\sum x_i y_i with xiMx_i\in M and yi1/My_i \in 1/M, so that xiyiRx_iy_i\in R by definition of 1/M1/M

Reid Barton (Oct 31 2020 at 18:39):

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

Filippo A. E. Nuccio (Oct 31 2020 at 18:40):

Well, what do you mean by "explicitely"?

Reid Barton (Oct 31 2020 at 18:40):

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

Reid Barton (Oct 31 2020 at 18:41):

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

Johan Commelin (Oct 31 2020 at 18:41):

apply submodule.span_le

Johan Commelin (Oct 31 2020 at 18:41):

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

Reid Barton (Oct 31 2020 at 18:42):

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 (Oct 31 2020 at 18:43):

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 (Oct 31 2020 at 18:44):

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 (Oct 31 2020 at 18:45):

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

Mario Carneiro (Oct 31 2020 at 18:45):

docs#ideal.mul_le

Reid Barton (Oct 31 2020 at 18:45):

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

Johan Commelin (Oct 31 2020 at 18:45):

Mario Carneiro said:

docs#ideal.mul_le

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

Mario Carneiro (Oct 31 2020 at 18:46):

What is the type of anything?

Filippo A. E. Nuccio (Oct 31 2020 at 18:46):

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

Mario Carneiro (Oct 31 2020 at 18:46):

#mwe please

Filippo A. E. Nuccio (Oct 31 2020 at 18:46):

both are submodules A R

Filippo A. E. Nuccio (Oct 31 2020 at 18:46):

Mario Carneiro said:

#mwe please

Working on it...

Johan Commelin (Oct 31 2020 at 18:46):

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

Mario Carneiro (Oct 31 2020 at 18:47):

docs#submodule.mul_le

Johan Commelin (Oct 31 2020 at 18:47):

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

Kevin Buzzard (Oct 31 2020 at 18:47):

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 (Oct 31 2020 at 18:49):

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 (Oct 31 2020 at 18:49):

imports?

Kevin Buzzard (Oct 31 2020 at 18:49):

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 (Oct 31 2020 at 18:50):

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 (Oct 31 2020 at 18:51):

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 (Oct 31 2020 at 18:51):

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

Mario Carneiro (Oct 31 2020 at 18:51):

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 (Oct 31 2020 at 18:51):

You can construct the recursor yourself

Filippo A. E. Nuccio (Oct 31 2020 at 18:52):

What do you mean?

Reid Barton (Oct 31 2020 at 18:53):

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 ixiyi\sum_i x_i y_i on a page

Mario Carneiro (Oct 31 2020 at 18:53):

Your #mwe doesn't work

Mario Carneiro (Oct 31 2020 at 18:53):

Try copying it into a new file

Mario Carneiro (Oct 31 2020 at 18:53):

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 (Oct 31 2020 at 18:54):

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 (Oct 31 2020 at 18:54):

5 lines, as promised

Johan Commelin (Oct 31 2020 at 18:54):

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

Filippo A. E. Nuccio (Oct 31 2020 at 18:54):

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

Kevin Buzzard (Oct 31 2020 at 18:55):

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

Filippo A. E. Nuccio (Oct 31 2020 at 18:55):

Sure, I will. Thanks.

Kevin Buzzard (Oct 31 2020 at 18:55):

As a beginner I would always unfold everything

Kevin Buzzard (Oct 31 2020 at 18:56):

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

Kevin Buzzard (Oct 31 2020 at 18:56):

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

Kevin Buzzard (Oct 31 2020 at 18:57):

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 (Oct 31 2020 at 18:58):

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

Filippo A. E. Nuccio (Oct 31 2020 at 18:58):

But I see your point, thanks.

Kevin Buzzard (Oct 31 2020 at 18:59):

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 (Oct 31 2020 at 19:00):

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

Johan Commelin (Oct 31 2020 at 19:00):

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 (Oct 31 2020 at 19:00):

The triangle works!

Reid Barton (Oct 31 2020 at 19:02):

4 of those ()s look unnecessary

Reid Barton (Oct 31 2020 at 19:02):

which is all of them I guess

Johan Commelin (Oct 31 2020 at 19:02):

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

Johan Commelin (Oct 31 2020 at 19:02):

That's 72 chars

Mario Carneiro (Oct 31 2020 at 19:02):

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 (Oct 31 2020 at 19:02):

Is that 42?

Mario Carneiro (Oct 31 2020 at 19:02):

49

Johan Commelin (Oct 31 2020 at 19:03):

(deleted)

Mario Carneiro (Oct 31 2020 at 19:03):

by finish [mul_le, mem_div_iff_forall_mul_mem] is 47

Johan Commelin (Oct 31 2020 at 19:04):

and slow...

Johan Commelin (Oct 31 2020 at 19:04):

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

Mario Carneiro (Oct 31 2020 at 19:05):

rfl

Mario Carneiro (Oct 31 2020 at 19:05):

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

Johan Commelin (Oct 31 2020 at 19:06):

That would even bring it below :37: chars

Johan Commelin (Oct 31 2020 at 19:07):

What would happen if J and Lean had a child?

Mario Carneiro (Oct 31 2020 at 19:07):

L

Johan Commelin (Oct 31 2020 at 19:07):

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

Filippo A. E. Nuccio (Oct 31 2020 at 19:10):

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 (Oct 31 2020 at 19:11):

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

Johan Commelin (Oct 31 2020 at 19:11):

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

Johan Commelin (Oct 31 2020 at 19:12):

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 (Oct 31 2020 at 19:12):

Ah, ok!

Kevin Buzzard (Oct 31 2020 at 19:12):

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

Filippo A. E. Nuccio (Oct 31 2020 at 19:12):

Pratt parsers?

Kevin Buzzard (Oct 31 2020 at 19:12):

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

Kevin Buzzard (Oct 31 2020 at 19:13):

In the UK we call it bidmas or bodmas

Kevin Buzzard (Oct 31 2020 at 19:13):

Pemdas in the US

Kevin Buzzard (Oct 31 2020 at 19:13):

It's about which operators to do first

Adam Topaz (Oct 31 2020 at 19:13):

$ is a Haskell thing right?

Filippo A. E. Nuccio (Oct 31 2020 at 19:13):

AH, go(ogle)t it!

Kevin Buzzard (Oct 31 2020 at 19:13):

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

Johan Commelin (Oct 31 2020 at 19:14):

Adam Topaz said:

$ is a Haskell thing right?

It was a US thing before that (-;

Kevin Buzzard (Oct 31 2020 at 19:14):

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

Kevin Buzzard (Oct 31 2020 at 19:15):

You can write #print notation $ to see.

Kevin Buzzard (Oct 31 2020 at 19:15):

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

Filippo A. E. Nuccio (Oct 31 2020 at 19:15):

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 (Oct 31 2020 at 19:16):

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

Kevin Buzzard (Oct 31 2020 at 19:16):

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

Kevin Buzzard (Oct 31 2020 at 19:17):

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 (Oct 31 2020 at 19:19):

Right.

Filippo A. E. Nuccio (Oct 31 2020 at 19:20):

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

Mario Carneiro (Oct 31 2020 at 19:22):

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 (Nov 04 2020 at 13:51):

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 II is a non-zero ideal. Then I×I1=1I\times I^{-1}=1 so there exists aiIa_i\in I and biI1b_i\in I^{-1} such that iaibi=1\sum_i a_i b_i = 1 (a finite sum); multiplying both sides by an element of II now shows that the aia_i generate II.

Kevin Buzzard (Nov 04 2020 at 13:52):

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

Kevin Buzzard (Nov 04 2020 at 16:29):

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

Kevin Buzzard (Nov 04 2020 at 16:35):

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 (Nov 04 2020 at 17:06):

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 (Nov 04 2020 at 18:54):

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 (Nov 04 2020 at 22:52):

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)


Last updated: Dec 20 2023 at 11:08 UTC