proposition: Theorem sub_genus (G : hypermap) (p : pred G) (e n f : sig p -> sig p) (can3enf : cancel3 e n f) : let H := Hypermap can3enf in (forall (x : H), val (edge x) = skip p edge (val x)) -> (forall (x : H), val (node x) = skip p node (val x)) -> genus H <= genus G.
proof: Proof. elim/card_ind : G p e n f can3enf => G IH p e n f can3enf H sameE sameN. case: (boolP [forall x, p x]) => [/forallP all_p|/forallPn [z npz]]. - suff I : hiso H G by rewrite (hiso_genus I). hiso (subT_bij all_p). + move => x /=; rewrite sameE skip1 //; exact: all_p. + move => x /=; rewrite sameN skip1 //; exact: all_p. - pose G' := WalkupF z. apply: (@leq_trans (genus G')); last exact: le_genus_WalkupF. pose p' := (fun x : G' => p (val x)). have skip_edge := @skip_hom _ p' _ (@edgeI G'). have skip_node := @skip_hom _ p' _ (@nodeI G'). pose e' := frestrict skip_edge. pose n' := frestrict skip_node. pose f' := finv n' \o finv e'. have can3enf' : cancel3 e' n' f'. { move => x. rewrite /f'/= finv_f ?f_finv //. - apply/frestrict_inj/skip_inj/(@nodeI G'). - apply/frestrict_inj/skip_inj/(@edgeI G'). } suff I : hiso H (Hypermap can3enf'). { rewrite (hiso_genus I). (apply: leq_trans; last apply: (IH G' _ p' e' n' f' can3enf')) => //. - by rewrite /G' /WalkupF /= (card_S_Walkup z). - by case. - by case. } have fwd_proof1 (x : sig p) : val x != z by apply: contraTneq (valP x) => ->. have fwd_proof2 (x : sig p) : p' (Sub (val x) (fwd_proof1 x)) by exact: (valP x). pose i_fwd (x : sig p) : sig p' := Sub _ (fwd_proof2 x). have bwd_proof (x : sig p') : p (val (val x)) by apply: (valP x). pose i_bwd (x : sig p') : sig p := Sub _ (bwd_proof x). have can_fwd : cancel i_fwd i_bwd by move => x; apply: val_inj. have can_bwd : cancel i_bwd i_fwd by move => x; do 2 apply: val_inj. hiso (Bij can_fwd can_bwd). * case => x px /=. do ! apply: val_inj => /=. rewrite sameE /=. move: (fwd_proof1 _) => /= xDz. exact: skip_skip1. * case => x px /=. do ! apply: val_inj => /=. rewrite sameN /=. move: (fwd_proof1 _) => /= xDz. exact: skip_skip1. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)