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