Zulip Chat Archive

Stream: Is there code for X?

Topic: mem.span


view this post on Zulip 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?)

view this post on Zulip Scott Morrison (Sep 08 2020 at 10:51):

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

view this post on Zulip Scott Morrison (Sep 08 2020 at 10:52):

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

view this post on Zulip Johan Commelin (Sep 08 2020 at 10:52):

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

view this post on Zulip Markus Himmel (Sep 08 2020 at 10:53):

Does docs#submodule.span_induction help?

view this post on Zulip Anne Baanen (Sep 08 2020 at 10:54):

This is called docs#finsupp.mem_span_iff_total

view this post on Zulip Anne Baanen (Sep 08 2020 at 10:57):

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

view this post on Zulip Scott Morrison (Sep 08 2020 at 11:03):

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

view this post on Zulip Scott Morrison (Sep 08 2020 at 11:04):

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

view this post on Zulip Scott Morrison (Sep 08 2020 at 11:06):

It seems submodule.span_induction will work smoothly for me.

view this post on Zulip 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.

view this post on Zulip Filippo A. E. Nuccio (Oct 30 2020 at 17:21):

Has this finally got merged into mathlib?

view this post on Zulip Adam Topaz (Oct 30 2020 at 18:03):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Oct 31 2020 at 18:01):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Oct 31 2020 at 18:03):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Adam Topaz (Oct 31 2020 at 18:07):

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

view this post on Zulip Mario Carneiro (Oct 31 2020 at 18:08):

{v1 * (a - b)}?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Adam Topaz (Oct 31 2020 at 18:11):

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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Oct 31 2020 at 18:12):

The finsupp is just the normal form

view this post on Zulip Mario Carneiro (Oct 31 2020 at 18:12):

just like how polynomial only represents the polynomials in normal form

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Oct 31 2020 at 18:12):

if you have a list, you can sum the list

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 31 2020 at 18:13):

it is

view this post on Zulip Adam Topaz (Oct 31 2020 at 18:13):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 31 2020 at 18:14):

Okay we're clearly having a miscommunication then

view this post on Zulip Adam Topaz (Oct 31 2020 at 18:14):

probably :)

view this post on Zulip Mario Carneiro (Oct 31 2020 at 18:14):

that's not a linear combination of two vectors

view this post on Zulip Mario Carneiro (Oct 31 2020 at 18:15):

that's a linear combination of one vector

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Filippo A. E. Nuccio (Oct 31 2020 at 18:16):

So did I.

view this post on Zulip Mario Carneiro (Oct 31 2020 at 18:16):

That depends on your use case

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Oct 31 2020 at 18:17):

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

view this post on Zulip Adam Topaz (Oct 31 2020 at 18:18):

This docs#finsupp.mem_span_iff_total is a good example

view this post on Zulip 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

view this post on Zulip Adam Topaz (Oct 31 2020 at 18:19):

Yeah, I see now

view this post on Zulip Filippo A. E. Nuccio (Oct 31 2020 at 18:20):

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

view this post on Zulip Mario Carneiro (Oct 31 2020 at 18:20):

That depends on where the vectors come from

view this post on Zulip Reid Barton (Oct 31 2020 at 18:20):

Is this how finsupp.total was always defined?

view this post on Zulip Mario Carneiro (Oct 31 2020 at 18:20):

no

view this post on Zulip Mario Carneiro (Oct 31 2020 at 18:21):

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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Oct 31 2020 at 18:22):

As in, just two things?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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"

view this post on Zulip Mario Carneiro (Oct 31 2020 at 18:24):

you can still do that though?

view this post on Zulip Filippo A. E. Nuccio (Oct 31 2020 at 18:24):

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

view this post on Zulip Mario Carneiro (Oct 31 2020 at 18:24):

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

view this post on Zulip Mario Carneiro (Oct 31 2020 at 18:24):

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

view this post on Zulip Mario Carneiro (Oct 31 2020 at 18:25):

Oh I understand now

view this post on Zulip 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)

view this post on Zulip Mario Carneiro (Oct 31 2020 at 18:26):

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

view this post on Zulip Mario Carneiro (Oct 31 2020 at 18:26):

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

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Mario Carneiro (Oct 31 2020 at 18:30):

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

view this post on Zulip Mario Carneiro (Oct 31 2020 at 18:30):

like imports and variables

view this post on Zulip Filippo A. E. Nuccio (Oct 31 2020 at 18:31):

Sure, give me a sec.

view this post on Zulip Reid Barton (Oct 31 2020 at 18:31):

docs#submodule.span_smul_span is pretty close to your statement

view this post on Zulip Reid Barton (Oct 31 2020 at 18:32):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Reid Barton (Oct 31 2020 at 18:39):

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

view this post on Zulip Filippo A. E. Nuccio (Oct 31 2020 at 18:40):

Well, what do you mean by "explicitely"?

view this post on Zulip 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

view this post on Zulip Reid Barton (Oct 31 2020 at 18:41):

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

view this post on Zulip Johan Commelin (Oct 31 2020 at 18:41):

apply submodule.span_le

view this post on Zulip Johan Commelin (Oct 31 2020 at 18:41):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Mario Carneiro (Oct 31 2020 at 18:45):

docs#ideal.mul_le

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Oct 31 2020 at 18:46):

What is the type of anything?

view this post on Zulip Filippo A. E. Nuccio (Oct 31 2020 at 18:46):

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

view this post on Zulip Mario Carneiro (Oct 31 2020 at 18:46):

#mwe please

view this post on Zulip Filippo A. E. Nuccio (Oct 31 2020 at 18:46):

both are submodules A R

view this post on Zulip Filippo A. E. Nuccio (Oct 31 2020 at 18:46):

Mario Carneiro said:

#mwe please

Working on it...

view this post on Zulip Johan Commelin (Oct 31 2020 at 18:46):

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

view this post on Zulip Mario Carneiro (Oct 31 2020 at 18:47):

docs#submodule.mul_le

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 31 2020 at 18:49):

imports?

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip Filippo A. E. Nuccio (Oct 31 2020 at 18:51):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Oct 31 2020 at 18:51):

You can construct the recursor yourself

view this post on Zulip Filippo A. E. Nuccio (Oct 31 2020 at 18:52):

What do you mean?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 31 2020 at 18:53):

Your #mwe doesn't work

view this post on Zulip Mario Carneiro (Oct 31 2020 at 18:53):

Try copying it into a new file

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Oct 31 2020 at 18:54):

5 lines, as promised

view this post on Zulip Johan Commelin (Oct 31 2020 at 18:54):

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

view this post on Zulip Filippo A. E. Nuccio (Oct 31 2020 at 18:54):

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

view this post on Zulip Kevin Buzzard (Oct 31 2020 at 18:55):

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

view this post on Zulip Filippo A. E. Nuccio (Oct 31 2020 at 18:55):

Sure, I will. Thanks.

view this post on Zulip Kevin Buzzard (Oct 31 2020 at 18:55):

As a beginner I would always unfold everything

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Filippo A. E. Nuccio (Oct 31 2020 at 18:58):

But I see your point, thanks.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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:

view this post on Zulip Kevin Buzzard (Oct 31 2020 at 19:00):

The triangle works!

view this post on Zulip Reid Barton (Oct 31 2020 at 19:02):

4 of those ()s look unnecessary

view this post on Zulip Reid Barton (Oct 31 2020 at 19:02):

which is all of them I guess

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Oct 31 2020 at 19:02):

That's 72 chars

view this post on Zulip 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]

view this post on Zulip Johan Commelin (Oct 31 2020 at 19:02):

Is that 42?

view this post on Zulip Mario Carneiro (Oct 31 2020 at 19:02):

49

view this post on Zulip Johan Commelin (Oct 31 2020 at 19:03):

(deleted)

view this post on Zulip Mario Carneiro (Oct 31 2020 at 19:03):

by finish [mul_le, mem_div_iff_forall_mul_mem] is 47

view this post on Zulip Johan Commelin (Oct 31 2020 at 19:04):

and slow...

view this post on Zulip Johan Commelin (Oct 31 2020 at 19:04):

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

view this post on Zulip Mario Carneiro (Oct 31 2020 at 19:05):

rfl

view this post on Zulip Mario Carneiro (Oct 31 2020 at 19:05):

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

view this post on Zulip Johan Commelin (Oct 31 2020 at 19:06):

That would even bring it below :37: chars

view this post on Zulip Johan Commelin (Oct 31 2020 at 19:07):

What would happen if J and Lean had a child?

view this post on Zulip Mario Carneiro (Oct 31 2020 at 19:07):

L

view this post on Zulip Johan Commelin (Oct 31 2020 at 19:07):

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

view this post on Zulip 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)?

view this post on Zulip Johan Commelin (Oct 31 2020 at 19:11):

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

view this post on Zulip Johan Commelin (Oct 31 2020 at 19:11):

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

view this post on Zulip 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 )))))

view this post on Zulip Filippo A. E. Nuccio (Oct 31 2020 at 19:12):

Ah, ok!

view this post on Zulip 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

view this post on Zulip Filippo A. E. Nuccio (Oct 31 2020 at 19:12):

Pratt parsers?

view this post on Zulip Kevin Buzzard (Oct 31 2020 at 19:12):

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

view this post on Zulip Kevin Buzzard (Oct 31 2020 at 19:13):

In the UK we call it bidmas or bodmas

view this post on Zulip Kevin Buzzard (Oct 31 2020 at 19:13):

Pemdas in the US

view this post on Zulip Kevin Buzzard (Oct 31 2020 at 19:13):

It's about which operators to do first

view this post on Zulip Adam Topaz (Oct 31 2020 at 19:13):

$ is a Haskell thing right?

view this post on Zulip Filippo A. E. Nuccio (Oct 31 2020 at 19:13):

AH, go(ogle)t it!

view this post on Zulip Kevin Buzzard (Oct 31 2020 at 19:13):

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

view this post on Zulip Johan Commelin (Oct 31 2020 at 19:14):

Adam Topaz said:

$ is a Haskell thing right?

It was a US thing before that (-;

view this post on Zulip Kevin Buzzard (Oct 31 2020 at 19:14):

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

view this post on Zulip Kevin Buzzard (Oct 31 2020 at 19:15):

You can write #print notation $ to see.

view this post on Zulip Kevin Buzzard (Oct 31 2020 at 19:15):

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

view this post on Zulip 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...

view this post on Zulip Kevin Buzzard (Oct 31 2020 at 19:16):

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

view this post on Zulip Kevin Buzzard (Oct 31 2020 at 19:16):

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

view this post on Zulip 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

view this post on Zulip Filippo A. E. Nuccio (Oct 31 2020 at 19:19):

Right.

view this post on Zulip Filippo A. E. Nuccio (Oct 31 2020 at 19:20):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Nov 04 2020 at 13:52):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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: May 19 2021 at 00:40 UTC