Zulip Chat Archive

Stream: new members

Topic: free modules


view this post on Zulip Damiano Testa (Aug 29 2020 at 15:52):

Dear All,

I am trying to understand how to generate the free module of rank n over a commutative ring R. I do not understand how to use the \oplus notation, so I was wondering if the definition below constructs what I think it does!

Also, how to I construct a linear_map between free modules? Or, at least, how can I have a linear_map as a hypothesis of a lemma/theorem/proposition?

Thank you very much!

import algebra.direct_sum

universe u

def free (R : Type u) [comm_ring R] (n : ) := semimodule R (direct_sum {i :  // i  n} (λ (i : {i :  // i  n}), R))

view this post on Zulip Kevin Buzzard (Aug 29 2020 at 16:07):

def free (R : Type u) [comm_ring R] (n : ℕ) := fin n -> R probably works fine

view this post on Zulip Kevin Buzzard (Aug 29 2020 at 16:08):

You might want to import algebra.pi_instances if you haven't already; I think this is the import which gives it the module structure.

view this post on Zulip Damiano Testa (Aug 29 2020 at 16:12):

Thanks: I will try with algebra.pi_instances!

view this post on Zulip Johan Commelin (Aug 29 2020 at 16:22):

@Damiano Testa If you make your own definition, you will have to reprove all the basic lemmas

view this post on Zulip Johan Commelin (Aug 29 2020 at 16:22):

I think it is easier to try to learn how to use the free modules that are already in mathlib.

view this post on Zulip Damiano Testa (Aug 29 2020 at 16:28):

@Johan Commelin I have tried to use the symbols for direct_sums, but I have failed. I am happy to use what is available, but I am not able to...

view this post on Zulip Johan Commelin (Aug 29 2020 at 16:29):

I haven't used the symbols either

view this post on Zulip Johan Commelin (Aug 29 2020 at 16:29):

I would probably use finsupp

view this post on Zulip Kevin Buzzard (Aug 29 2020 at 16:30):

I think X -> R is the canonical product of R's over X, and X ->_0 R is the canonical direct sum.

view this post on Zulip Damiano Testa (Aug 29 2020 at 16:33):

Kevin Buzzard said:

I think X -> R is the canonical product of R's over X, and X ->_0 R is the canonical direct sum.

Ok, as I have only finitely generated free modules, I should be able to choose which one I prefer! Hopefully, I can also find an isomorphism between the two, in case I need to go back and forth...

view this post on Zulip Damiano Testa (Aug 29 2020 at 16:36):

In any case, all that I should need is the following statement: if f is an endomorphism of a free module of rank n over an integral domain and f^n is not the zero endomorphism, then no power of f is the zero endomorphism.

view this post on Zulip Kevin Buzzard (Aug 29 2020 at 16:37):

That's not true -- consider multiplication by 2 on (Z/2^{100}Z)^3

view this post on Zulip Kevin Buzzard (Aug 29 2020 at 16:37):

oh sorry! ID!

view this post on Zulip Kevin Buzzard (Aug 29 2020 at 16:37):

Yes that's totally true, and should be fun to prove in Lean.

view this post on Zulip Damiano Testa (Aug 29 2020 at 16:37):

I also made that mistake, integral domain is crucial!

view this post on Zulip Damiano Testa (Aug 29 2020 at 16:38):

and then is just a statement about nilpotent matrices and their characteristic polynomial

view this post on Zulip Kevin Buzzard (Aug 29 2020 at 16:38):

Right. I don't know if this stuff is in mathlib but it should be by now. Do we have Cayley Hamilton?

view this post on Zulip Damiano Testa (Aug 29 2020 at 16:38):

i saw it somewhere, but i was trying to get to define the modules, before i went further on how to prove stuff

view this post on Zulip Kevin Buzzard (Aug 29 2020 at 16:39):

You should prove it for fields first using CH and then deduce it for IDs using field of fractions

view this post on Zulip Damiano Testa (Aug 29 2020 at 16:39):

mathlib/src/linear_algebra/char_poly.lean:# Characteristic polynomials and the Cayley-Hamilton theorem
mathlib/src/linear_algebra/char_poly.lean:The Cayley-Hamilton theorem, that the characteristic polynomial of a matrix,

view this post on Zulip Damiano Testa (Aug 29 2020 at 16:39):

(i grepped Cayley-Hamilton)

view this post on Zulip Damiano Testa (Aug 29 2020 at 16:40):

Kevin Buzzard said:

You should prove it for fields first using CH and then deduce it for IDs using field of fractions

yes, that is what my strategy was, but i have been unable to start... even a vector space! ahahaha

view this post on Zulip Kevin Buzzard (Aug 29 2020 at 16:40):

You don't have to grep: ch.png

view this post on Zulip Kevin Buzzard (Aug 29 2020 at 16:41):

CH is proved for matrices in that file.

view this post on Zulip Kevin Buzzard (Aug 29 2020 at 16:42):

Note that the rows and columns are indexed by an arbitrary finite type n in that file.

view this post on Zulip Damiano Testa (Aug 29 2020 at 16:42):

Kevin Buzzard said:

You don't have to grep: ch.png

how did you open "search"?

view this post on Zulip Kevin Buzzard (Aug 29 2020 at 16:42):

Don't worry about the proofs but try and read the definitions and theorem statements in the Lean file.

view this post on Zulip Kevin Buzzard (Aug 29 2020 at 16:42):

I opened search with the magnifying glass in the toolbar on the left of VS Code. But there's a gotcha.

view this post on Zulip Damiano Testa (Aug 29 2020 at 16:43):

Kevin Buzzard said:

I opened search with the magnifying glass in the toolbar on the left of VS Code. But there's a gotcha.

indeed: my lean does not search mathlib...

view this post on Zulip Kevin Buzzard (Aug 29 2020 at 16:43):

Can you see the cog on my screenshot, which isn't blue? If the search doesn't work for you, then it might be because you're using Lean in a project which has mathlib as a dependency, and VS Code is not searching dependencies (because this is the default behaviour). Click on the three dots and then on the blue cog to unblue it.

view this post on Zulip Kevin Buzzard (Aug 29 2020 at 16:44):

I have told this to 100 students.

view this post on Zulip Damiano Testa (Aug 29 2020 at 16:47):

got it: thanks!!!

view this post on Zulip Kevin Buzzard (Aug 29 2020 at 16:49):

So now we have Cayley Hamilton for matrices, but if you really want to prove something for free modules you're going to have to learn about how to move between matrices and linear maps in Lean, and I have no idea how to do this.

view this post on Zulip Patrick Massot (Aug 29 2020 at 16:50):

https://leanprover-community.github.io/mathlib_docs/linear_algebra/matrix.html

view this post on Zulip Patrick Massot (Aug 29 2020 at 16:51):

That's the file you are looking for. And it will get better once #3919 is merged. And then a very nice project would be to split it into well documented smaller files.

view this post on Zulip Damiano Testa (Aug 29 2020 at 16:52):

Ok, I can probably reduce to the case of fields, if taking fields of fractions of integral domains is straightforward

view this post on Zulip Kevin Buzzard (Aug 29 2020 at 16:53):

Great! Thanks Patrick! So now here are some exercises.

1) Prove that if phi is a linear map from (n -> R) to (n -> R) and f is the char poly of the corresponding matrix, then f(phi)=0.

2) Prove that if phi=T^n then phi^n=0

3) Prove that if a matrix is nilpotent then its char poly is T^n (this might be in the library, but it might not be; it doesn't technically need eigenvalues but they might help)

view this post on Zulip Patrick Massot (Aug 29 2020 at 16:54):

I don't see what eigenvalues have to do with 3).

view this post on Zulip Damiano Testa (Aug 29 2020 at 16:55):

given two polynomials f g : polynomial R with g monic, i want to show that f is in the radical of g if f^(nat_degree g) is a multiple of g. This boils down to viewing f as a linear map on quotient (ideal.span {g}), which is a free R module...

view this post on Zulip Patrick Massot (Aug 29 2020 at 16:55):

I think mathlib knows that polynomial annihilating a given endormorphism form an ideal and K[X]K[X] is principal, so we have a minimal polynomial which if some XkX^k and divides the characteristic polynomial which has degree nn.

view this post on Zulip Patrick Massot (Aug 29 2020 at 16:56):

The previous message is still answering Kevin, not Damiano

view this post on Zulip Damiano Testa (Aug 29 2020 at 16:56):

Patrick Massot said:

The previous message is still answering Kevin, not Damiano

yes, but I am also following the side conversation!

view this post on Zulip Johan Commelin (Aug 29 2020 at 16:57):

Damiano Testa said:

Ok, I can probably reduce to the case of fields, if taking fields of fractions of integral domains is straightforward

Yes, this should be straight-forward. But I haven't thought about the rest of the steps. Is there tensoring involved?

view this post on Zulip Kevin Buzzard (Aug 29 2020 at 16:57):

The "down with determinants" (Axler) philosophy says "come on, this has nothing to do with determinants", and perhaps Patrick has signed up for this, but the determinant proof is "char poly = prod (T-eigenvalues) and if v is an eigenvector (work in an alg closure) with eigenvalue lambda then lambda^(big)=0 if phi is nilpotent so char poly = T^n".

view this post on Zulip Damiano Testa (Aug 29 2020 at 16:58):

Johan Commelin said:

Yes, this should be straight-forward. But I haven't thought about the rest of the steps. Is there tensoring involved?

Not necessarily, but you should convince Lean that multiplying by f on polynomial R descends to a linear endomorphism on the quotient by g.

view this post on Zulip Patrick Massot (Aug 29 2020 at 16:58):

I still prefer my proof :stuck_out_tongue:

view this post on Zulip Damiano Testa (Aug 29 2020 at 16:59):

(and possibly afterwards taking field of fractions: this could be viewed as tensoring, but it is also just including an integral domain in a larger field...)

view this post on Zulip Damiano Testa (Aug 29 2020 at 17:00):

(I guess that you can also view the quotient by g as a tensor product, though...)

view this post on Zulip Damiano Testa (Aug 29 2020 at 17:02):

Anyway, the biggest obstacle for me at the moment is to understand how to define free modules/vector spaces. if i can do one of these two, then it will likely be how to convert multiplication by an element into an endomorphism and after that, how to reduce to fields of fractions

view this post on Zulip Damiano Testa (Aug 29 2020 at 17:05):

how do you type the small \iota in

(f : (q  R) [R] p  R)

view this post on Zulip Patrick Massot (Aug 29 2020 at 17:06):

\l

view this post on Zulip Patrick Massot (Aug 29 2020 at 17:06):

It stand for "linear"

view this post on Zulip Patrick Massot (Aug 29 2020 at 17:06):

hence the l

view this post on Zulip Kevin Buzzard (Aug 29 2020 at 17:06):

It was at about this point when we realised that our naming conventions were not really scaling well.

view this post on Zulip Damiano Testa (Aug 29 2020 at 17:06):

\l types a left pointing arrow on my keyboard

view this post on Zulip Kevin Buzzard (Aug 29 2020 at 17:07):

Of course all this would be solved if we moved to categories

view this post on Zulip Kevin Buzzard (Aug 29 2020 at 17:07):

It might be \_l

view this post on Zulip Patrick Massot (Aug 29 2020 at 17:07):

oops, I meant \_l

view this post on Zulip Patrick Massot (Aug 29 2020 at 17:07):

I was too focused on getting the \ right (since I don't use backslash)

view this post on Zulip Damiano Testa (Aug 29 2020 at 17:07):

ah, \_l produces the symbol! i was convinced that it was a small \iota...

view this post on Zulip Damiano Testa (Aug 29 2020 at 17:08):

thank you both anyway!

view this post on Zulip Kevin Buzzard (Aug 29 2020 at 17:08):

Patrick's proof is much more lean-friendly, because we know k[X] is a PID and a UFD, and there is machinery there.

view this post on Zulip Damiano Testa (Aug 29 2020 at 17:08):

this was also the proof that i had in mind

view this post on Zulip Damiano Testa (Aug 29 2020 at 17:09):

anyway, i will go back to learning about free modules, whether over a commutative (semi-)ring which may or may not be an integral domain or a field!

view this post on Zulip Damiano Testa (Aug 29 2020 at 17:10):

in the end, the fractions are there just for psychological reasons: the given arguments almost never use them anyway... i guess this is the same with the semiring distinction, athough i have never thought about that seriously...

view this post on Zulip Kevin Buzzard (Aug 29 2020 at 17:11):

Damiano -- for your radical approach it's obvious that if f^(nat_degree g) is a multiple of g then f is in the radical of g. You mean the other way around, right? If f is in the radical of g then f^M is a multiple of g, so all prime factors of g in k[X] divide f^M and hence f, so g divides f^(number of prime factors of g counted with multiplicity) and now you have to show the number of prime factors of g is at most deg(g) because all primes have degree >= 1 -- it might be easier to work over a field here.

view this post on Zulip Damiano Testa (Aug 29 2020 at 17:13):

Yes, I want to show that if some power of f is in the radical (g), then f^(deg g) is in the radical (g). I am even thinking that i might do without knowing the explicit power, but I must check that the maths side of things does not actually rely on knowing a priori a fixed bound

view this post on Zulip Damiano Testa (Aug 29 2020 at 17:14):

(deleted)

view this post on Zulip Damiano Testa (Aug 29 2020 at 17:15):

if only i had access to a proof checker, to convince myself that not having an a priori bound still makes the proof go through...

view this post on Zulip Aaron Anderson (Aug 29 2020 at 17:17):

One potential stumbling block with @Patrick Massot’s method is that we have minimal_polynomial in mathlib, but only for elements of commutative algebras

view this post on Zulip Aaron Anderson (Aug 29 2020 at 17:18):

It’s probably still the best approach, but fixing that probably ought to happen first

view this post on Zulip Patrick Massot (Aug 29 2020 at 17:23):

Oh, I didn't know that. The "minimal polynomial" entry of the overview is completely misleading then.

view this post on Zulip Patrick Massot (Aug 29 2020 at 17:24):

Wait. Isn't it more general?

view this post on Zulip Damiano Testa (Aug 29 2020 at 17:25):

(to close up a hanging thread: i think that the the proof that i know does need some form of upper bound on the power of f that is in the ideal (g) that is independent on f.)

view this post on Zulip Damiano Testa (Aug 29 2020 at 17:29):

Patrick Massot said:

Oh, I didn't know that. The "minimal polynomial" entry of the overview is completely misleading then.

In my case, this seems what I want: B=R[x]/(g) is an A=R algebra and multiplication by f induces the element x. if i can convert this into lean, i should be good to go!

view this post on Zulip Damiano Testa (Aug 29 2020 at 17:30):

is polynomial R an algebra over R? Is quotient g an algebra over R?

view this post on Zulip Patrick Massot (Aug 29 2020 at 17:31):

I'm sure Lean knows about the first one at least.

view this post on Zulip Damiano Testa (Aug 29 2020 at 17:31):

assuming that g is monic, does lean know that quotient g is finite over R?

view this post on Zulip Damiano Testa (Aug 29 2020 at 17:32):

(i guess that these are the steps that i will need to understand, i am fleshing them out here, mostly for future reference for myself! of course, if someone can start ticking them off, i will gladly take the help!)

view this post on Zulip Patrick Massot (Aug 29 2020 at 17:33):

Oh no, I just realized the import word in Aaron's message is commutative.

view this post on Zulip Damiano Testa (Aug 29 2020 at 17:33):

my rings are always commutative

view this post on Zulip Patrick Massot (Aug 29 2020 at 17:33):

So yes, this need to be fixed first.

view this post on Zulip Patrick Massot (Aug 29 2020 at 17:33):

The base ring is not the issue.

view this post on Zulip Patrick Massot (Aug 29 2020 at 17:33):

The issue for minimal polynomial of an endomorphism is the endomorphism algebra is not commutative.

view this post on Zulip Damiano Testa (Aug 29 2020 at 17:35):

but I am ok with working with the endomorphisms that are linear combinations of multiples of a single one, so this is still commutative, no? am i missing something?

view this post on Zulip Damiano Testa (Aug 29 2020 at 17:36):

(i only have multiplication by a fixed element f, nothing else)

view this post on Zulip Patrick Massot (Aug 29 2020 at 17:36):

That sounds fine.

view this post on Zulip Patrick Massot (Aug 29 2020 at 17:36):

I'm only complaining we can't use the minimal_polynomial we have in mathlib.

view this post on Zulip Patrick Massot (Aug 29 2020 at 17:38):

It's a bit sad that our brand new docs#linear_algebra.eigenspace file doesn't include existence of the minimal polynomial.

view this post on Zulip Aaron Anderson (Aug 29 2020 at 17:39):

Our minimal_polynomial file also doesn’t really use PID or UFD theory very explicitly, for better or worse

view this post on Zulip Damiano Testa (Aug 29 2020 at 17:40):

Patrick Massot said:

It's a bit sad that our brand new docs#linear_algebra.eigenspace file doesn't include existence of the minimal polynomial.

...and that the link is broken...

view this post on Zulip Patrick Massot (Aug 29 2020 at 17:40):

https://leanprover-community.github.io/mathlib_docs/linear_algebra/eigenspace.html

view this post on Zulip Patrick Massot (Aug 29 2020 at 17:40):

I don't know how to use the linkifier for file names.


Last updated: May 13 2021 at 05:21 UTC