From mathcomp Require Import all_ssreflect all_algebra zmodp.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import GRing.Theory.
Open Scope ring_scope.
Section CPGE.
(** #
#
* 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.
#
#
*)
Lemma pinvmx_on_key : unit. Proof. exact: tt. Qed.
Definition pinvmx_on (F : fieldType) (m n : nat) (S : 'M_m)
(A : 'M[F]_(m, n)) : 'M_(n, m) :=
locked_with pinvmx_on_key (pinvmx A *m proj_mx S (kermx A)).
Lemma pinvmx_on_sub (F : fieldType) (m n : nat) (S : 'M_(m))
(A : 'M[F]_(m, n)) : (pinvmx_on S A <= S)%MS.
Proof.
rewrite [pinvmx_on _ _]unlock.
by rewrite (submx_trans (proj_mx_sub _ _ _)) ?genmxE.
Qed.
Lemma mulmxKpV_on (F : fieldType) (m1 m2 n : nat) (S : 'M_(m2))
(A : 'M[F]_(m1, n)) (B : 'M_(m2, n)) :
(S :&: kermx B)%MS = 0 ->
(S + kermx B == 1%:M)%MS ->
(A <= B)%MS -> A *m pinvmx_on S B *m B = A.
Proof.
move=> SIkB0 SDkB1 subAB; rewrite [pinvmx_on _ _]unlock -[RHS](mulmxKpV subAB).
symmetry; apply: subr0_eq; rewrite -mulmxBl -mulmxBr.
apply/sub_kermxP; rewrite mulmx_sub // proj_mx_compl_sub //.
by rewrite (eqmxP SDkB1) submx1.
Qed.
(**
#
#
#
#
*)
(** -------------------------------------------- *)
(** ##
* 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).
#
#
*)
Section ex_6_12.
Variables (F : fieldType) (n' : nat).
Let n := n'.+1.
Section Q1.
(**
#
#
** 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
#
# *)
Variable (u : 'M[F]_n) (S : 'M[F]_n).
Hypothesis eq_keru_imu : (kermx u :=: u)%MS.
Hypothesis S_u_direct : (S :&: u)%MS = 0.
Hypothesis S_u_eq1 : (S + u == 1)%MS.
Fact S_ku_direct : (S :&: kermx u)%MS = 0.
Proof.
apply/eqmx0P.
rewrite !(cap_eqmx (_ : S :=: S)%MS eq_keru_imu) //.
Admitted.
Hint Resolve S_ku_direct.
Fact S_ku_eq1 : (S + kermx u == 1)%MS.
Admitted.
Hint Resolve S_ku_eq1.
Implicit Types (x y z : 'rV[F]_n).
(** #
# *)
(** -------------------------------------------- *)
(** #
#
*** 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.
#
# *)
Definition w := locked (proj_mx S u).
Definition v := locked (proj_mx u S * pinvmx_on S u).
(** #
#
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.
#
# *)
Lemma wS x : (x *m w <= S)%MS.
Proof.
unlock w.
Admitted.
Lemma vS x : (x *m v <= S)%MS.
Proof.
unlock v.
Admitted.
Lemma w_id x : (x <= S)%MS -> x *m w = x.
Proof.
unlock w => xS.
Admitted.
(** #
#
**** Question 1.a.ii.
#
# *)
Lemma Su_rect x : x = x *m w + (x *m v) *m u.
Proof.
unlock v w.
Admitted.
(** #
# #
# *)
(** -------------------------------------------- *)
(** #
#
**** Question 1.a.iii.
From the following lemma
#
# *)
Lemma Su_dec_eq0 y z : (y <= S)%MS -> (z <= S)%MS ->
(y + z *m u == 0) = (y == 0) && (z == 0).
Proof.
move=> yS zS; apply/idP/idP; last first.
by move=> /andP[/eqP -> /eqP ->]; rewrite add0r mul0mx.
rewrite addr_eq0 -mulNmx => /eqP eq_y_Nzu.
have : (y <= S :&: u)%MS by rewrite sub_capmx yS eq_y_Nzu submxMl.
rewrite S_u_direct // submx0 => /eqP y_eq0.
move/eqP: eq_y_Nzu; rewrite y_eq0 eq_sym mulNmx oppr_eq0 eqxx /= => /eqP.
move=> /sub_kermxP; rewrite eq_keru_imu => z_keru.
have : (z <= S :&: u)%MS by rewrite sub_capmx zS.
by rewrite S_u_direct // submx0.
Qed.
(** #
#
deduce
#
# *)
Lemma Su_dec_uniq y y' z z' : (y <= S)%MS -> (z <= S)%MS ->
(y' <= S)%MS -> (z' <= S)%MS ->
(y + z *m u == y' + z' *m u) = (y == y') && (z == z').
Proof.
Admitted.
(** #
# #
# *)
(** -------------------------------------------- *)
(** #
#
**** Question 1.a.iii.
Show some simplification lemmas
- the two first are direct
- the two last use Su_dec_uniq.
#
# *)
Lemma u2_eq0 : u *m u = 0.
Admitted.
Lemma u2K m (a : 'M_(m,n)) : a *m u *m u = 0.
Lemma uv x : (x <= S)%MS -> (x *m u) *m v = x.
Proof.
Admitted.
Lemma uw x : (x <= S)%MS -> (x *m u) *m w = 0.
Proof.
Admitted.
(** #
# #
# *)
(** -------------------------------------------- *)
(** #
#
*** 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
#
#
#
# *)
Lemma add_uv_vu : v *m u + u *m v = 1.
Proof.
Admitted.
(** #
#
*** 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
#
#
#
# *)
Lemma add_wu_uw : w *m u + u *m w = u.
Proof.
Admitted.
End Q1.
(** #
# #
# *)
(** -------------------------------------------- *)
(** #
#
** 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).
#
#
*)
Section Q2.
Variable (u : 'M[F]_n).
Lemma u20_eq_u_kermx v : u ^+ 2 = 0 -> v *m u + u *m v = 1 -> (u == kermx u)%MS.
Proof.
Admitted.
End Q2.
Section Q3.
Hypothesis charF_neq2 : [char F]^'.-nat 2.
Let u : 'M[F]_3 :=
Let w : 'M[F]_3 :=
Lemma u_neq0 : u != 0.
Admitted.
Lemma wuDuw_eq_u : w *m u + u *m w = u.
Proof.
Admitted.
Lemma neq_u_kermxu : (u != kermx u)%MS.
Proof.
Admitted.
End Q3.
End ex_6_12.
End CPGE.