proposition: Remark exercise6_7 G0 G1 H0 H1 E x: equivalence G0 -> substrate G0 = E -> equivalence H0 -> substrate H0 = E -> equivalence G1 -> substrate G1 = E -> equivalence H1 -> substrate H1 = E -> G1 \cap H0 = G0 \cap H1 -> G1 \cg H0 = G0 \cg H1 -> inc x E -> ( let G1x := direct_image G1 (singleton x) in let H1x := direct_image H1 (singleton x) in let R0 := induced_relation G0 G1x in let S0 := induced_relation H0 H1x in equipotent (quotient R0) (quotient S0)).
proof: Proof. Abort. Lemma exercise6_8 f r: equivalence r -> function f -> target f = substrate r -> (exists g, bijection_prop g (quotient (inv_image_relation f r)) (quotient (induced_relation r (Imf f)))). Proof. move => er ff tf. set (s := inv_image_relation f r). set (A:= Imf f). set (Ra := induced_relation r A). have ia: (iirel_axioms f r) by []. have [es _]:= (iirel_relation ia). have iA: induced_rel_axioms r A. by split =>//; rewrite -tf; apply: Imf_Starget. have [eR _]:=(induced_rel_equivalence iA). set (f1:= fun x y => [/\ classp r y, nonempty (y \cap A) & x = Vfi f y]). have qsp:forall x, inc x (quotient s) -> exists y, f1 x y. by move=> x /(setQ_P es); move /(iirel_classP ia). set (f2:= fun x => choose (fun y => f1 x y)). have f2p: (forall x, inc x (quotient s) -> f1 x (f2 x)). move=> x xq; rewrite /f2;apply: choose_pr; apply: (qsp _ xq). set (f3:= fun x => (f2 x) \cap A). have f3p: (forall x, inc x (quotient s) -> inc (f3 x) (quotient Ra)). move=> x xs; rewrite /Ra; move: (f2p _ xs) => [pa pb pc]. apply/(setQ_P eR); apply/(induced_rel_classP iA). by exists (f2 x). set (g:= Lf f3 (quotient s) (quotient Ra)). have sgf: sgraph (graph f) by fprops. exists g; rewrite /g;saw; apply: lf_bijective => //. move => u v uq vq; rewrite /f3 => ii. move: (f2p _ uq)(f2p _ vq); rewrite /f1; move=> [cfu niu uv][cfv niv vv]. move: niv=> [y] /setI2_P [y2v yiA]. have y2u: inc y (f2 u). apply: (@setI2_1 (f2 u) A);rewrite ii; fprops. move: yiA;rewrite [A](ImfE ff); move /(rangeP sgf)=> [x Jg]. have xb: (inc x v) by rewrite vv; apply/iim_graph_P;ex_tac. have xu:(inc x u) by rewrite uv; apply/iim_graph_P; ex_tac. move : uq vq; move/(setQ_P es) => c1 /(setQ_P es) => c2. by case: (class_dichot es c1 c2) => // dj; empty_tac1 x. move=> y; move /(setQ_P eR) /(induced_rel_classP iA)=> [x [cx nex yi]]. set (u:= Vfi f x). have uq: inc u (quotient s) by apply/ (setQ_P es) /(iirel_classP ia); exists x. ex_tac. rewrite /f3 yi. move:(f2p _ uq); rewrite /f1; move=> [cf2 ni ui]. move: nex=> [t] /setI2_P [tx]. rewrite {1} [A](ImfE ff) ; move/ (rangeP sgf)=> [z Jg]. have: inc z u by apply/iim_graph_P; ex_tac. rewrite {1} ui; move/iim_graph_P => [t' t'2u Jg']. have tt': t = t' by move: (Vf_pr ff Jg) (Vf_pr ff Jg') => <-. suff: f2 u = x by move->. case:(class_dichot er cf2 cx)=> // di. by empty_tac1 t ;rewrite tt'. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)