# Zulip Chat Archive

## Stream: new members

### Topic: free modules

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

#### Kevin Buzzard (Aug 29 2020 at 16:07):

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

probably works fine

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

#### Damiano Testa (Aug 29 2020 at 16:12):

Thanks: I will try with algebra.pi_instances!

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

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

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

#### Johan Commelin (Aug 29 2020 at 16:29):

I haven't used the symbols either

#### Johan Commelin (Aug 29 2020 at 16:29):

I would probably use `finsupp`

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

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

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

#### Kevin Buzzard (Aug 29 2020 at 16:37):

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

#### Kevin Buzzard (Aug 29 2020 at 16:37):

oh sorry! ID!

#### Kevin Buzzard (Aug 29 2020 at 16:37):

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

#### Damiano Testa (Aug 29 2020 at 16:37):

I also made that mistake, *integral domain* is crucial!

#### Damiano Testa (Aug 29 2020 at 16:38):

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

#### 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?

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

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

#### 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,

#### Damiano Testa (Aug 29 2020 at 16:39):

(i grepped Cayley-Hamilton)

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

#### Kevin Buzzard (Aug 29 2020 at 16:40):

You don't have to grep: ch.png

#### Kevin Buzzard (Aug 29 2020 at 16:41):

CH is proved for matrices in that file.

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

#### Damiano Testa (Aug 29 2020 at 16:42):

Kevin Buzzard said:

You don't have to grep: ch.png

how did you open "search"?

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

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

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

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

#### Kevin Buzzard (Aug 29 2020 at 16:44):

I have told this to 100 students.

#### Damiano Testa (Aug 29 2020 at 16:47):

got it: thanks!!!

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

#### Patrick Massot (Aug 29 2020 at 16:50):

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

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

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

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

#### Patrick Massot (Aug 29 2020 at 16:54):

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

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

#### Patrick Massot (Aug 29 2020 at 16:55):

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 (Aug 29 2020 at 16:56):

The previous message is still answering Kevin, not Damiano

#### 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!

#### 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?

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

#### 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`

.

#### Patrick Massot (Aug 29 2020 at 16:58):

I still prefer my proof :stuck_out_tongue:

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

#### Damiano Testa (Aug 29 2020 at 17:00):

(I guess that you can also view the quotient by `g`

as a tensor product, though...)

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

#### Damiano Testa (Aug 29 2020 at 17:05):

how do you type the small \iota in

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

#### Patrick Massot (Aug 29 2020 at 17:06):

`\l`

#### Patrick Massot (Aug 29 2020 at 17:06):

It stand for "linear"

#### Patrick Massot (Aug 29 2020 at 17:06):

hence the l

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

#### Damiano Testa (Aug 29 2020 at 17:06):

`\l`

types a left pointing arrow on my keyboard

#### Kevin Buzzard (Aug 29 2020 at 17:07):

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

#### Kevin Buzzard (Aug 29 2020 at 17:07):

It might be `\_l`

#### Patrick Massot (Aug 29 2020 at 17:07):

oops, I meant `\_l`

#### Patrick Massot (Aug 29 2020 at 17:07):

I was too focused on getting the `\`

right (since I don't use backslash)

#### Damiano Testa (Aug 29 2020 at 17:07):

ah, `\_l`

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

#### Damiano Testa (Aug 29 2020 at 17:08):

thank you both anyway!

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

#### Damiano Testa (Aug 29 2020 at 17:08):

this was also the proof that i had in mind

#### 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!

#### 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 *semi*ring distinction, athough i have never thought about that seriously...

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

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

#### Damiano Testa (Aug 29 2020 at 17:14):

(deleted)

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

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

#### Aaron Anderson (Aug 29 2020 at 17:18):

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

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

#### Patrick Massot (Aug 29 2020 at 17:24):

Wait. Isn't it more general?

#### 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`

.)

#### 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!

#### Damiano Testa (Aug 29 2020 at 17:30):

is `polynomial R`

an algebra over `R`

? Is `quotient g`

an algebra over `R`

?

#### Patrick Massot (Aug 29 2020 at 17:31):

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

#### Damiano Testa (Aug 29 2020 at 17:31):

assuming that `g`

is monic, does lean know that `quotient g`

is finite over `R`

?

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

#### Patrick Massot (Aug 29 2020 at 17:33):

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

#### Damiano Testa (Aug 29 2020 at 17:33):

my rings are *always* commutative

#### Patrick Massot (Aug 29 2020 at 17:33):

So yes, this need to be fixed first.

#### Patrick Massot (Aug 29 2020 at 17:33):

The base ring is not the issue.

#### Patrick Massot (Aug 29 2020 at 17:33):

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

#### 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?

#### Damiano Testa (Aug 29 2020 at 17:36):

(i only have multiplication by a fixed element `f`

, nothing else)

#### Patrick Massot (Aug 29 2020 at 17:36):

That sounds fine.

#### Patrick Massot (Aug 29 2020 at 17:36):

I'm only complaining we can't use the `minimal_polynomial`

we have in mathlib.

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

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

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

#### Patrick Massot (Aug 29 2020 at 17:40):

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

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