proposition: Lemma prl_product_can_fun_bij S S' (sd: prl_same_index S S') (E:= projective_limit S) (E' := projective_limit S') (f:= projective_map (prl_system_product sd) (prl_product_can_fun S S') (E \times E')): bijection_prop f (E \times E') (projective_limit (prl_system_product sd)).
proof: Proof. move:(prl_system_product_prop sd) => [pa pb pc pd]. move:(prl_product_can_fun_compat sd) => ha. move:(prl_map_prop ha) (prl_map_ax ha). have ssI:= (prl_same_index_same_I sd). rewrite -/E -/E' -/f; move =>[hc hd ] he. rewrite /f/projective_map; saw; apply:lf_bijective. - exact:he. - move => u v ua va. move: (ua)=>/setX_P[pu p1u p2u]; move:(va)=> /setX_P[pv p1v p2v]. rewrite /prl_map_val pb => ww. have hh i: inc i (psI S) -> J (Vg (P u) i) (Vg (Q u) i) = J (Vg (P v) i) (Vg (Q v) i). move => iI. move:(iI); rewrite ssI => iI'. move:(prl_can_fun_fp iI) => [ffi sf tf]. move:(prl_can_fun_fp iI') => [ffi' sf' tf']. move:(prl_proj_ax iI)(prl_proj_ax iI') => ax ax'. move:(f_equal (Vg ^~i) ww);rewrite /prl_product_can_fun !LgV//. rewrite ext_to_prod_V2 // ? ext_to_prod_V2 //. + rewrite /prl_can_fun !LfV//. + by rewrite sf sf'. + by rewrite sf sf'. move/prl_limitP:p1u => [ha1 hb1 hc1 hd1]. move/prl_limitP:p2u => [ha2 hb2 hc2 hd2]. move/prl_limitP:p1v => [ha3 hb3 hc3 hd3]. move/prl_limitP:p2v => [ha4 hb4 hc4 hd4]. apply: pair_exten => //; apply: fgraph_exten => //. + by rewrite hb1 hb3. + rewrite hb1;move => i iI; exact: (pr1_def (hh _ iI)). + by rewrite hb2 hb4. + rewrite hb2 - ssI => i iI; exact: (pr2_def (hh _ iI)). move => y yi. move /Zo_P: yi => [/setXb_P []]. rewrite pa pc pd /prl_product_E; aw => fgy dy yv yw. set x1 := Lg (psI S) (fun i => P (Vg y i)). set x2 := Lg (psI S) (fun i => Q (Vg y i)). have yv1 i: inc i (psI S) -> [/\ pairp (Vg y i), inc (P (Vg y i)) (Vg (psE S) i) & inc (Q (Vg y i)) (Vg (psE S') i)]. by move => iI; move:(yv _ iI); rewrite LgV//; case/setX_P. have x1p:inc x1 (projective_limit S). rewrite /x1;apply/Zo_P; split. apply/setXb_P;split; fprops;rewrite ps_domain_E; aw; trivial. by move => i iI; rewrite !LgV//; case: (yv1 _ iI). move => i j lij. move: (prl_prop0 lij) => [iI jI]. move:(ps_function_f lij) => [ff sf tf]. move: (yw _ _ lij); rewrite /prl_product_f ! LgV//. rewrite sd in lij; move:(ps_function_f lij) => [ff' sf' tf']. rewrite (ext_to_prod_V2 ff ff'); first by move => ->; rewrite pr1_pair. by rewrite sf sf';move: (yv _ jI); rewrite LgV//; aw. have x2p:inc x2 (projective_limit S'). rewrite /x2;apply/Zo_P; split. apply/setXb_P;split; fprops;rewrite ps_domain_E ssI; aw; trivial. by move => i iI; rewrite ! LgV//; rewrite - ssI in iI;case: (yv1 _ iI). move => i j lij. move:(ps_function_f lij) => [ff' sf' tf']. rewrite - sd in lij;move: (prl_prop0 lij) => [iI jI]. move: (yw _ _ lij); rewrite /prl_product_f !LgV//. move:(ps_function_f lij) => [ff sf tf]. rewrite (ext_to_prod_V2 ff ff'); first by move => ->; rewrite pr2_pair. by rewrite sf sf';move: (yv _ jI); rewrite LgV//; aw. set x:= (J x1 x2); exists x; first by apply: setXp_i. rewrite /prl_map_val /x pb. apply:fgraph_exten => //; aww. rewrite dy; move => i iI /=; rewrite LgV//. move:(prl_can_fun_fp iI) => [ffi sf tf]. move: (iI); rewrite ssI => iI'. move:(prl_can_fun_fp iI') => [ffi' sf' tf']. move: (prl_proj_ax iI)(prl_proj_ax iI') => ax ax'. rewrite /prl_product_can_fun LgV//; rewrite ext_to_prod_V2 //. rewrite /prl_can_fun -(proj31 (yv1 _ iI)) /x /x1 /x2. rewrite pr1_pair pr2_pair ! LfV// !LgV//. by rewrite sf sf'; apply: setXp_i. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)