proposition: Lemma prl_inv_hyp_prop2 S S' u: prl_same_index S S' -> prl_map2_compat S S' u -> (forall i, inc i (psI S) -> bijection (Vg u i)) -> bijection (projective_limit_fun S S' u).
proof: Proof. move => h1 h2 h3. move: (prl_map2_prop h1 h2) => [ [ff sf tf] _]. split; first by apply:prl_inv_hyp_prop1 => // i /h3 []. split =>// y; rewrite sf tf => yp. move/prl_limitP: yp => [ghg dy yv yw]. have ssI:= prl_same_index_same_I h1. have dy': domain y = psI S by rewrite dy. pose x:= Lg (psI S) (fun i => Vf (inverse_fun (Vg u i)) (Vg y i)). have iii: psI S = domain (psE S) by rewrite ps_domain_E. move: (h2) => [h2a h2b h2c h2d]. rewrite - ssI in yv. have xi i: inc i (psI S) -> inc (Vg x i) (Vg (psE S) i). move => iI; rewrite /x LgV//. move:(h3 _ iI) (h2c _ iI) => bu [fu su tu]. by rewrite - su; apply: inverse_Vis => //; rewrite tu; apply: yv. have xp: inc x (productb (psE S)). apply /setXb_P; rewrite /x - iii;aw; split; fprops. have xps: inc x (projective_limit S). apply/Zo_P; split => // i j lij. have lij': gle (psr S') i j by rewrite - h1. move: (prl_prop0 lij) => [iI jI]. move: (h2c _ iI) => [fui sui tui]. move: (h2c _ jI) => [fuj suj tuj]. have co1: Vg (psf S') (J i j) \coP Vg u j. move:(ps_function_f lij') => [fij sij tij]. by split => //; rewrite sij tuj; aw. move:(ps_function_f lij) => [fij sij tij]. have co2:Vg u i \coP Vg (psf S) (J i j). by split => //; rewrite sui tij; aw. have sx1: inc (Vg x j) (source (Vg u j)) by rewrite suj; apply: xi. have sx2: inc (Vg x j) (source (Vg (psf S) (J i j))). by rewrite sij; aw; apply: xi. have ys1: inc (Vg y j) (target (Vg u j)) by rewrite tuj; apply: yv. have ys2: inc (Vf (Vg (psf S) (J i j)) (Vg x j)) (source (Vg u i)). by rewrite pr1_pair in tij; rewrite sui - tij; apply: (Vf_target fij sx2). move:(f_equal (Vf^~(Vg x j)) (h2d _ _ lij)); rewrite !compfV//. have ->: Vf (Vg u j) (Vg x j) = Vg y j. by rewrite /x LgV// (inverse_V (h3 _ jI) ys1). rewrite - (yw _ _ lij') {2}/x LgV// => <-. by rewrite (inverse_V2 (h3 _ iI)). move: (prl_map_ax (prl_map2_prop1 h1 h2)) => ax. exists x => //. rewrite /projective_limit_fun /projective_map LfV//. symmetry;rewrite /prl_map_val - ssI; apply: fgraph_exten. - fprops. - done. - by aw; rewrite dy'. - aw => i iI. move: (h2c _ iI) => [fu su tu]. rewrite LgV //(prl_map2_prop2 iI xps fu su) /x LgV// inverse_V //. exact: (h3 _ iI). by rewrite tu; apply: yv. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)