free modules

Stream: new members

[Damiano Testa]

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))

[Kevin Buzzard]

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

[Kevin Buzzard]

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.

[Damiano Testa]

Thanks: I will try with algebra.pi_instances!

[Johan Commelin]

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

[Johan Commelin]

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

[Damiano Testa]

@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...

[Johan Commelin]

I haven't used the symbols either

[Johan Commelin]

I would probably use finsupp

[Kevin Buzzard]

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

[Damiano Testa]

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...

[Damiano Testa]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

oh sorry! ID!

[Kevin Buzzard]

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

[Damiano Testa]

I also made that mistake, integral domain is crucial!

[Damiano Testa]

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

[Kevin Buzzard]

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

[Damiano Testa]

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

[Kevin Buzzard]

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

[Damiano Testa]

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,

[Damiano Testa]

(i grepped Cayley-Hamilton)

[Damiano Testa]

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

[Kevin Buzzard]

You don't have to grep: ch.png

[Kevin Buzzard]

CH is proved for matrices in that file.

[Kevin Buzzard]

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

[Damiano Testa]

Kevin Buzzard said:

You don't have to grep: ch.png

how did you open "search"?

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Damiano Testa]

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...

[Kevin Buzzard]

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.

[Kevin Buzzard]

I have told this to 100 students.

[Damiano Testa]

got it: thanks!!!

[Kevin Buzzard]

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.

[Patrick Massot]

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

[Patrick Massot]

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.

[Damiano Testa]

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

[Kevin Buzzard]

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)

[Patrick Massot]

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

[Damiano Testa]

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...

[Patrick Massot]

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

[Patrick Massot]

The previous message is still answering Kevin, not Damiano

[Damiano Testa]

Patrick Massot said:

The previous message is still answering Kevin, not Damiano

yes, but I am also following the side conversation!

[Johan Commelin]

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?

[Kevin Buzzard]

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".

[Damiano Testa]

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.

[Patrick Massot]

I still prefer my proof :stuck_out_tongue:

[Damiano Testa]

(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...)

[Damiano Testa]

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

[Damiano Testa]

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

[Damiano Testa]

how do you type the small \iota in

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

[Patrick Massot]

\l

[Patrick Massot]

It stand for "linear"

[Patrick Massot]

hence the l

[Kevin Buzzard]

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

[Damiano Testa]

\l types a left pointing arrow on my keyboard

[Kevin Buzzard]

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

[Kevin Buzzard]

It might be \_l

[Patrick Massot]

oops, I meant \_l

[Patrick Massot]

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

[Damiano Testa]

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

[Damiano Testa]

thank you both anyway!

[Kevin Buzzard]

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

[Damiano Testa]

this was also the proof that i had in mind

[Damiano Testa]

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!

[Damiano Testa]

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...

[Kevin Buzzard]

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.

[Damiano Testa]

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

[Damiano Testa]

(deleted)

[Damiano Testa]

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...

[Aaron Anderson]

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

[Aaron Anderson]

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

[Patrick Massot]

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

[Patrick Massot]

Wait. Isn't it more general?

[Damiano Testa]

(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.)

[Damiano Testa]

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!

[Damiano Testa]

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

[Patrick Massot]

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

[Damiano Testa]

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

[Damiano Testa]

(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!)

[Patrick Massot]

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

[Damiano Testa]

my rings are always commutative

[Patrick Massot]

So yes, this need to be fixed first.

[Patrick Massot]

The base ring is not the issue.

[Patrick Massot]

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

[Damiano Testa]

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?

[Damiano Testa]

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

[Patrick Massot]

That sounds fine.

[Patrick Massot]

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

[Patrick Massot]

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

[Aaron Anderson]

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

[Damiano Testa]

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...

[Patrick Massot]

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

[Patrick Massot]

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