To play this document inside your browser use ALT-N and ALT-P. If you get stack overflow errors, try to use Google Chrome or Chromium with the command line option --js-flags="--harmony-tailcalls".

You can save your edits inside your browser and load them back (edits are also saved when you close the window). Finally you can download the file for offline editing.

Preliminaries

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.
We thus define a matrix pinvmx_on S u, which represents the partial inverse of u that maps the image of u (represented by u) to S, and which is correct only when S is indeed a complement of kermx u.

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, so that E is the direct sum of S and Im u.

First, prove that E is the direct sum of S and Ker 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.

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.

Question 1.a.iii.

From the following lemma

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. (by definition)
Show that u o v + v o u = 1.

Indeed u (v x) + v (u x)
  = u (v x) + v (u (w x)) + v (u (u (v x))) by Su_rect
  = u (v x) + v (u (w x)) by u2K
  = u (v x) + w x by uv
  = x by -Su_rect

Question 1.c.

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

Indeed u (w x) + w (u x)
  = u (w x) + w (u (w x)) + w (u (u (v x))) by Su_rect
  = u (w x) + w (u (w x)) by u2K
  = u (w x) by uw
  = u (x - u (v x)) by  Su_rect
  = u x by u2K

Questions 2 and 3

Let u be a endomorphism of E such that u^2 = 0.

Q2. Suppose there is a v such that u v + v u = 1, prove the kernel and image of u are equal.
Q3. Suppose u != 0 and suppose there is a w such that uw + wu = u. Find a counter example of Ker u = Im u. (Hint: take u e1 = 0, u e2 = 0 and u e3 = e2 in 'M_3 and use a dimension argument).