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