proposition: Lemma remove_parallel (D : hypermap) (g : D -> G) (emb_g : embedding g) : exists (D' : hypermap) (g' : D' -> G), [/\ simple_hmap D', embedding g' & genus D' <= genus D].
proof: Proof. elim/card_ind : D g emb_g => D IH g emb_g. pose b := [exists x : D, exists y, [&& x != y, cnode x y & cnode (edge x) (edge y)]]. have [|simpleD] := boolP b; rewrite /b; last first. { exists D, g; split => // x y xDy n_x_y. by move: simpleD => /existsPn /(_ x) /exists_inPn /(_ _ xDy); rewrite n_x_y. } move=> /existsP [x /exists_inP [y xDy /andP[n_x_y n_ex_ey]]]. have plainD : plain D by apply: emb_plain emb_g. have exF : edge x != x by rewrite plain_neq. pose D' := @WalkupE (WalkupF x) (Sub (edge x) exF). pose g' (z : D') := g (val (val z)). suff emb_g' : embedding g'. { have leD : #|D'| < #|D|. by rewrite /D' -card_S_Walkup /WalkupF /= card_sig max_card. have [D'' [g'' [D1 D2 D3]]] := IH _ leD _ emb_g'. exists D'', g''; split => //; apply: leq_trans D3 _. exact: leq_trans (le_genus_WalkupE _) (le_genus_WalkupF _). } rewrite eq_sym in xDy. have plain_eq := plain_eq plainD. have yDex : y != edge x. { apply: contraNneq (emb_loopless emb_g) => y_ex. by apply/existsP; exists x; rewrite -y_ex. } have inDpf (z : D) (zDx : z != x) (zDex : z != edge x) : (Sub z zDx) != Sub (edge x) exF :> WalkupF x by rewrite -val_eqE. pose inD' (z:D) (zDx : z != x) (zDex : z != edge x) : D' := Sub (Sub z zDx) (inDpf z zDx zDex). have plainD' : plain D'. { apply/plainP => u _; case: u => [[u U1] U2']. have U2 : @edge D u != x by rewrite -!val_eqE /= -(inj_eq edgeI) /= plain_eq in U2'. split. + do 2 apply: val_inj; rewrite /= ![sval (if _ then _ else _)]fun_if. rewrite -!val_eqE /= ![sval (if _ then _ else _)]fun_if. rewrite plain_eq !eqxx /=. by rewrite (negbTE U2) plain_eq (negbTE U1). + rewrite -!val_eqE /= ![sval (if _ then _ else _)]fun_if /=. by rewrite -!val_eqE /= plain_eq !eqxx (negbTE U2) plain_neq. } split => //. - move=> v; have [z g_z] := codomP (emb_surj emb_g v). have [xVex|] := boolP (z \in pred2 x (edge x)). + case/pred2P : xVex => ?; subst z v; apply/codomP. * by exists (inD' _ xDy yDex); apply/eqP; rewrite -(emb_vertex emb_g). * rewrite -(inj_eq edgeI) in xDy; rewrite -(inj_eq edgeI) plain_eq in yDex. by exists (inD' _ yDex xDy); apply/eqP; rewrite -(emb_vertex emb_g). + rewrite !inE negb_or => /andP [zDx zDex]. by apply/codomP; exists (inD' _ zDx zDex). - move => u v. by rewrite !walkup.fconnect_skip /= (emb_vertex emb_g). - move => u v. have edge_val (z : D') : @edge D (val (val z)) = val (val (edge z)). { rewrite /= ![sval (if _ then _ else _)]fun_if /= -!val_eqE /=. rewrite !plain_eq !eqxx ifF // -(inj_eq edgeI) plain_eq. by move: (valP z); rewrite -val_eqE => /=/negbTE->. } suff -> : adjn u v = @adjn D (val (val u)) (val (val v)) by apply: emb_edge. apply/exists_inP/exists_inP => -[z]; rewrite !inE. + by rewrite !walkup.fconnect_skip; exists (val (val z)); rewrite // edge_val. + have [xVex|] := boolP (z \in pred2 x (edge x)). * wlog -> : z u v {xVex} / z = x => [W|]. { case/pred2P : xVex => z_ex ; first exact: W. move=> n_u n_v. move: (W (edge z) v u); rewrite {1}z_ex !plain_eq. case => // z'. exists (edge z') => //. by rewrite (geometry.plain_eq plainD'). } exists (inD' _ xDy yDex); rewrite !inE !walkup.fconnect_skip //=. exact: connect_trans n_x_y. rewrite fun_if -val_eqE /= plain_eq !eqxx -(inj_eq edgeI) plain_eq (negbTE yDex). exact: connect_trans n_ex_ey. * rewrite inE negb_or => /andP[zDx zDex] n_u_z n_v_ez. by exists (inD' _ zDx zDex); rewrite !inE !walkup.fconnect_skip // -edge_val. 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)