Exercices de mathématiques oraux X-ens Algebre 1

Exercise 6.12: Endomorphisms u such that Ker u = Im u.

Let E be a vector space (any dimension, but in Coq we reason in finite dimension).

Question 1.

Let u be an endomorphism of E, such that Ker u = Im u and S be a complement of Im u (supplémentaire in french), so that E is the direct sum of S and Im u.

Question 1.a.

Show that for all x in E, there is a unique pair (y, z) in S² such that x = y + u (z), and pose v and z so that y = v(x) and z = w(x).

Instead of defining y and z for each x, we now define explicitly the matrix that computes y and z from x.

  • A direct consequence of this is that v and w will be morphisms by construction, you can thus skip the part of the paper proof that deals with this.

  • Every morphism induces an ismorphism between a complement of its kernel and its image. The function pinvmx is the inverse of this isomporhism, but since the complement of the kernel that was used to produce pinvmx is arbitrary, we must project the result of pinvmx on S in order to get the specific inverse with image S.

Note that we used locking in order to protect w and v from expanding unexpectedly during proofs.

Question 1.a.i.

Prove the following lemmas.

Question 1.a.ii.

Reuse and adapt and the proof in the course.

  • (hint: use mulmxKpV)

Question 1.a.iii.

From the proof


Question 1.a.iii.

Show some simplification lemmas

  • the two first are direct
  • the two last use Su_dec_uniq.

Question 1.b.

  • Show that v is linear.
  • Show that u o v + v o u = 1.

Question 1.c.

  • Show that w is linear.
  • Show that u o w + w o u = u.

State and prove question 2, and then 3...

save script