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

From the proof

deduce

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