Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
From mathcomp Require Import all_ssreflect all_algebra. Local Open Scope ring_scope. Section Problem1. Import GRing.Theory. Variable K : realFieldType. Variable E : vectType K. Variable f : 'End(E). Theorem equiv1 : (limg f + lker f)%VS = fullv <-> limg f = limg (f \o f). Proof. split. + move/(f_equal (lfun_img f)). rewrite limg_comp limg_add. move/esym: (lkerE f (lker f)). rewrite subvv => /eqP ->. by rewrite addv0 => ->. + rewrite limg_comp => Hf'. have := limg_ker_dim f (limg f). rewrite -[RHS]add0n -Hf' => /eqP. rewrite eqn_add2r dimv_eq0 => /eqP /dimv_disjoint_sum. have := limg_ker_dim f fullv. rewrite capfv addnC => -> Hf. apply/eqP. by rewrite eqEdim subvf -Hf leqnn. Qed. End Problem1. Section Problem2. Import GRing.Theory. Variable K : realFieldType. Variable E : vectType K. Variable p q : 'End(E). Definition projection (f : 'End(E)) := forall x, f (f x) = f x. Lemma proj_idE {f} : projection f <-> {in limg f, f =1 id}. Proof. split => Hf x. + by move/limg_lfunVK => <-. + by rewrite Hf // memv_img ?memvf. Qed. Hypothesis proj_p : projection p. Hypothesis proj_q : projection q. Section a. Lemma f_g_0 f g x : projection f -> projection g -> projection (f+g) -> f (g x) = 0. Proof. move=> Pf Pg /(_ (g x)). rewrite !lfun_simp !linearD /=. rewrite !Pf !Pg => /eqP. rewrite -subr_eq !addrA addrK. rewrite addrAC eq_sym -subr_eq eq_sym subrr => /eqP Hfg. have := f_equal g Hfg. rewrite !linearD /= Pg linear0 => /eqP. rewrite -mulr2n -scaler_nat scaler_eq0. rewrite Num.Theory.pnatr_eq0 /= => /eqP Hgfg. by rewrite Hgfg addr0 in Hfg. Qed. Theorem equiv2 : projection (p + q) <-> (forall x, p (q x) = 0 /\ q (p x) = 0). Proof. split=> H x. by rewrite !f_g_0 // addrC. rewrite !lfun_simp !linearD /= proj_p proj_q. by rewrite (proj1 (H x)) (proj2 (H x)) addrA !addr0. Qed. End a. Section b. Hypothesis proj_pq : projection (p + q). Lemma b1a x : x \in limg p -> x \in limg q -> x = 0. Proof. move=> Hp Hq. by rewrite -(f_g_0 p q x) // !(proj1 proj_idE). Qed. Lemma b1b : directv (limg p + limg q). Proof. apply/directv_addP/eqP. rewrite -subv0. apply/subvP => u /memv_capP [Hp Hq]. by rewrite memv0 (b1a u). Qed. Lemma limg_sub_lker f g : projection f -> projection g -> projection (f+g) -> (limg f <= lker g)%VS. Proof. move=> proj_f proj_g proj_fg. apply/subvP => x /limg_lfunVK <-. by rewrite memv_ker f_g_0 // addrC. Qed. Lemma b1c : (limg p <= lker q)%VS. Proof. by apply limg_sub_lker. Qed. Lemma b1c' : (limg q <= lker p)%VS. Proof. by rewrite limg_sub_lker // addrC. Qed. Lemma limg_addv (f g : 'End(E)) : (limg (f + g)%R <= limg f + limg g)%VS. Proof. apply/subvP => x /memv_imgP [u _ ->]. by rewrite lfun_simp memv_add // memv_img ?memvf. Qed. Theorem b1 : limg (p+q) = (limg p + limg q)%VS. Proof. apply/eqP; rewrite eqEsubv limg_addv /=. apply/subvP => x /memv_addP [u Hu] [v Hv ->]. have -> : u + v = (p + q) (u + v). rewrite lfun_simp !linearD /=. rewrite (proj1 proj_idE) // (proj1 proj_idE proj_q v) //. move/(subvP b1c'): Hv. rewrite memv_ker => /eqP ->. move/(subvP b1c): Hu. rewrite memv_ker => /eqP ->. by rewrite addr0 add0r. by apply memv_img, memvf. Qed. Theorem b2 : lker (p+q) = (lker p :&: lker q)%VS. Proof. apply/vspaceP => x. rewrite memv_cap !memv_ker. rewrite lfun_simp. case Hpx: (p x == 0). by rewrite (eqP Hpx) add0r. case Hqx: (q x == 0). by rewrite (eqP Hqx) addr0. case/boolP: (_ == 0) => //. rewrite eq_sym -subr_eq eq_sym sub0r => /eqP Hpqx. rewrite (b1a (p x)) ?eqxx // in Hpx. by apply memv_img, memvf. rewrite Hpqx memvN. by apply memv_img, memvf. Qed. End b. End Problem2.