exercise7
Exercices de mathématiques oraux X-ens Algebre 1
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).
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
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.
Endomorphisms u such that Ker u = Im u.
- What are the morphisms such that u o v = 0 and v + u is invertible ?