proposition: Lemma subgraph_embedding (G H : sgraph) (D : hypermap) (g : D -> H) : subgraph G H -> no_isolated G -> embedding g -> exists (D' : hypermap) (g' : D' -> G), embedding g' /\ genus D' <= genus D.
proof: Proof. case => h inj_h hom_h no_isoG emb_g. have plainD := emb_plain emb_g. pose V := h @: G. pose h' (x : H) : option G := if boolP (x \in codom h) is AltTrue b then Some (iinv b) else None. pose r := [rel u v : H | if (h' u, h' v) is (Some u', Some v') then u' -- v' else false]. pose p := [pred x : D | r (g x) (g (edge x))]. pose e := frestrict (skip_hom p edgeI). pose n := frestrict (skip_hom p nodeI). pose f := finv n \o finv e. have can3 : cancel3 e n f. { by move=> x; rewrite /f/= f_finv ?finv_f //; apply/frestrict_inj/skip_inj. } pose D' := Hypermap can3. have cl_p : fclosed edge p. { move=> x y /eqP <- {y}. rewrite !inE plain_eq // /h'. case: {-}_ / boolP => [gx_h|gxNh]; case: {-}_ / boolP => [gex_h|gexNh] => //. by rewrite sgP. } have eE (x : D') : val (edge x) = edge (val x). { rewrite val_frestrict skip1 // -(fclosed1 cl_p); exact: (valP x). } have imG : forall x : D', g (val x) \in codom h. { move=> x. have:= valP x. rewrite /p/=/h'. by case: {-}_ / boolP. } pose g' (x : D') := iinv (imG x). have leq_genus : genus D' <= genus D by apply: sub_genus => x; rewrite val_frestrict. suff emb_g' : @embedding G D' g' by exists D',g'. have cnE (x y : D') : cnode x y = (g' x == g' y). { rewrite fconnect_frestrict fconnect_skip //; try apply: valP. rewrite /g' -(inj_eq inj_h) !f_iinv; exact/emb_vertex. } split => //. - apply/plainP => x _; split; last by rewrite -val_eqE eE plain_neq. by apply: val_inj; rewrite !eE plain_eq. - move=> x; have [y xy] := no_isoG x. move/hom_h: (xy); rewrite inj_eq // sg_edgeNeq // => /(_ isT) hx_hy. have/codomP [dx hx_dx] := emb_surj emb_g (h x). have/codomP [dy hy_dy] := emb_surj emb_g (h y). move: hx_hy; rewrite hx_dx hy_dy -(emb_edge emb_g). case/exists_inP => [dz]; rewrite !inE => cn_xz cn_yz. suff pz : p dz. { apply/codomP; exists (Sub dz pz). apply: inj_h. rewrite f_iinv /=. by rewrite hx_dx (rwP eqP) -(emb_vertex emb_g). } rewrite !(emb_vertex emb_g) in cn_xz cn_yz. rewrite /p/=/h' altT -?(eqP cn_xz) -?hx_dx ?codom_f // => codom_x. rewrite altT -?(eqP cn_yz) -?hy_dy ?codom_f // => codom_y. by rewrite !iinv_f. - move=> x y; apply/exists_inP/idP => [[z]|]. + rewrite !inE !cnE /g' => /eqP-> /eqP->; have:= valP z; rewrite /p/=/h'. case : {-}_ /boolP => // gz_h; case : {-}_ /boolP => // gez_h. move: (imG (e z)); rewrite /= eE => gez_h'. by rewrite (bool_irrelevance gz_h (imG z)) (bool_irrelevance gez_h gez_h'). + move=> g'_xy. move/hom_h : (g'_xy); rewrite inj_eq // (sg_edgeNeq g'_xy) => /(_ isT) hg'_xy. move: (hg'_xy); rewrite !f_iinv => g_xy. move: (g_xy); rewrite -(emb_edge emb_g) => /exists_inP[z]. rewrite !inE => cn_xz cn_yz. suff pz : p z. { exists (Sub z pz); rewrite inE fconnect_frestrict fconnect_skip // ?eE //; try apply: valP. by rewrite -(fclosed1 cl_p). } rewrite !(emb_vertex emb_g) in cn_xz cn_yz. rewrite /p/=/h' altT -(eqP cn_xz) ?imG // => codom_x. rewrite altT -(eqP cn_yz) ?imG // => codom_y. move: g'_xy; rewrite /g'; move: (imG x) (imG y) => P1 P2. by rewrite (bool_irrelevance P1 codom_x) (bool_irrelevance P2 codom_y). Qed.
imports: mathcomp(all_ssreflect) fourcolor(hypermap geometry color coloring walkup combinatorial4ct cfmap) GraphTheory(edone preliminaries bij digraph sgraph) GraphTheory(connectivity minor hmap_ops smerge hcycle arc)