text_formalization/hypermap/summary.hl

   1 (*
   2 Notes on the hypermap chapter.
   3
   4 new type: hypermap
   5
   6 infixes: POWER, belong, iso.
   7
   8 key definitions: orbit_map f x (the orbit of x under f),
   9   edge x (edge map orbit of x), node x, face x.
  10   edge_map, face_map, node_map (the permutations)
  11
  12
  13
  14
  15 *)
  16
  17 (*
  18 Notes by Tom Hales in a conversation with TNT on Sep 9, 2010.
  19
  20   TNT has completed essentially everything up the section with title "transform"
  21   The main theorem in the "transform" section is called AQIUNPP (markup transform).
  22   It is a long proof that is  complete except for (flag1) and (flag2).  TNT promises
  23   to send the completed proof of AQIUNPP on Sep 12, 2010.
  24
  25   TNT's general naming convention is lemmaABC for the lemma with guid
  26   ABC.  In particular,
  27   lemmaZHQCZLX; lemmaFKSNTKR; lemmaHOZKXVW; lemmaTGJISOK; lemmaIUCLZYI;
  28   lemmaBISHKQW; lemmaFOAGLPA; lemmaSGCOSXK; lemmaQZTPGJV; lemmaKDAEDEX;
  29   lemmaLIPYTUI; lemmaILTXRQD; lemmaICJHAOQ; lemmaJMKRXLA;
  30   lemmaHQYMRTX; lemmaQRDYXYJ.
  31
  32   [Note: 2/15/2012
  33   *On HYQMRTX, the furthermore clause in the flypaper hasn't been included in lemmaHQYMRTX.
  34   *I can't find lemmaQRDYXY. It must not have been uploaded.
  35   *Also found lemmaSTKBEPH.  This is the algorithm termination; once there are sufficiently many
  36      loops in a normal family, it must be the collection of faces.  This seems to have been deleted
  37      from flypaper.pdf.
  38   ]
  39
  40
  41   RDW. Reverse double walkup. This is not implemented as of Sep 2010.
  42   He plans to do it in two cases. The special case that does not add
  43   any new nodes and the general case.  HLT needs the special case in
  44   the fans chapter.
  45
  46 *)
  47
  48 (*
  49
  50   KHGAQRG.  Not done as a separate lemma, but instead it appears many
  51   times as a subgoal.  If you have a restricted hypermap and and f step,
  52   then you get a singleton.  compare set_one_point,
  53   lemma_singleton_atom, .
  54
  55   YBGABWW. Equivalent but not identical to theorems in TNT.
  56
  57   PKRQTKP. There are many orbit theorems in hypermap.hl
  58
  59   ZJIOZB (def of merge and split), ZMFKZNH (merge-split).  Both TNT
  60   and Gonthier reverse things so that the lemma serves as a definition
  61   and the def is proved as a lemma.
  62
  63   ZMFKZNH breaks into several formal lemmas: lemma_face_merge,
  64   lemma_edge_merge, lemma_node_merge.
  65
  66   IUCLZYI. This has been formalized, but it is not used directly
  67   elsewhere.  Instead, a number of smaller preliminary lemmas get
  68   used.
  69
  70   EUXPBPO = lemmaThreeDarts //
  71
  72   WIRLCNL. Something equivalent gets done in lemma_cycle_is_face and
  73   lemmaQuotientFace.
  74
  75   UDJNSHH. Not formalized. Instead the proofs that rely on it go back
  76   to definitions instead.
  77
  78   KSRDPTZ = lemmaQuotientNoDoubleJoints //
  79
  80   PYOVATA = lemmaNodalFixedPoint (not exactly the same, the hypotheses
  81   are different)
  82
  83   Note May 2012.
  84   QQYVCFM. Not formalized.  dih2k defined in such a way to avoid lemma.
  85   WRGCVDR_CIZMRRH.hl defines dih2k in terms of the properties
  86   of QQYVCHEM.  So it appears that QQYVCFM is not needed.
  87   cyclic_hypermap.hl and related notions are dead code, never used.
  88
  89   KHGAQRG. Not formalized because TNT never needs to use it.
  90
  91 *)
  92
  93 (* Notes by Hales Feb 12, 2012.
  94
  95    There are over 600 lemmas in the file.
  96
  97    TNT has 108 definitions in his file, which makes it hard to
  98    understand the statements and how they related to the
  99    flypaper. Here is an informal summary of definitions.
 100
 101    infixes: POWER, belong, iso
 102
 103    Types:
 104    (A)hypermap  with extraction functions
 105    dart (H:(A)hypermap ->
 106    edge_map
 107    node_map
 108    face_map
 109
 110    edge H x ; edge orbit of dart x
 111    node H x ; node orbit of dart x
 112    face H x ; face orbit of dart x
 113
 114    (A)loop with extraction functions.  A loop is an unordered set (of darts) together with a permutation
 115    that acts transitively on he set.  (This is what gets called torsor in flypaper.pdf.)
 116    dart_of ; dart set of loop
 117    next ; successor function
 118    back ; inverse of successor function
 119    belong ; in dart set
 120    size ; card of dart set
 121    top ; PRE(CARD dart_of L)
 122    is_loop H L ; x IN L ==>one_step_contour H x (next L x)
 123    loop_path L x k ;  ((next L) POWER k) x; path out of loop starting at x.
 124    index L x y ; (specification) smallest i such that y = next^i x.
 125
 126    Informal definitions:
 127    POWER : nth iterate of a function.
 128    orbit_map (f:A->A)  (x:A)         orbit of x under f
 129    go_one_step H x y <=> y is the image of dart x under e,n, or f.
 130    is_path H (p:num->A) (n:num) ;  (p 0) ... (p n) is a dart path in H.
 131    is_in_component H x y ; darts x and y are in the same path component of H
 132    comb_component H x ; (same as is_in_component H x)
 133    set_of_orbits D f = set of orbits in D of f
 134    number_of_orbits D f = card of set_of_orbits
 135
 136    edge_set H = set_of_orbits (dart H) (edge_map H)
 137    node_set H = set_of_orbits (dart H) (node_map H)
 138    face_set H = set_of_orbits (dart H) (face_map H)
 139    set_components H D = set of combinatorial components of all darts x in D
 140    set_part_components H D = same as set_components H D
 141    set_of_components H = set_components H (dart H)
 142
 143    number_of_edges H = Klar
 144    number_of_nodes H = Klar
 145    number_of_faces H = Klar
 146    number_of_components H = Klar
 147    connected_hypermpa H = Klar
 148
 149    plain_hypermap H
 150    planar_hypermap H
 151    simple_hypermap H
 152    is_no_double_joins H
 153
 154    dart_degenerate H x;  the dart x is fixed by e,n, or f.
 155    dart_nondegenerate H x; negation
 156    is_edge_nondegenerate
 157    is_node_nondegenerate
 158    is_face_nondegenerate
 159    isolated_dart ; x = f x = n x = e x.
 160    is_edge_degenerate ; x = e x but x != n x, x != f x.
 161    is_node_degenerate
 162    is_face_degenerae
 163
 164    ***
 165    **   lists as functions p:num->A: ** :
 166
 167    is_inj_list (p:num->A) n ;  (p is 1-1 on 0..n)
 168    support_list (p:num->A) n ; { p i | i <= n}
 169    in_list p n ; i IN (support_list p n)
 170    is_disjoint p q
 171    glue p q n ; list concatenation.
 172    is_glueing p q n m ;  This states roughly that no member of (q,m) is in (p,n), except (p n = q 0).
 173    Used to concatenate injective lists (p,n) @ (q,m).
 174    join p q n ; list concatenation, swallowing head of q.
 175
 176    edge_path H x i   =  ((edge_map H) POWER i) x
 177    node_path H x i  =  similar
 178    face_path H x i =  similar
 179
 180    samsara  p n x = the successor to x in list (p,n), wrapping to the beginning if necessary.
 181
 182    *** contours
 183
 184    one_step_contour H x y ;   y = f x or n^{-1} x
 185    is_contour H p n ; (p,n) is a contour path
 186    node_contour H x i ;  ((inverse (node_map H)) POWER i) x
 187    face_contour H x i ; ((face_map H) POWER i) x
 188    is_inj_contour H p n ; (p,n) is an injective contour path
 189
 190
 191    *** walkup
 192
 193    shift H ; rotates (e,n,f) -> (n,f,e) triality of H.
 194    edge_walkup H x ; new hypermap after edge_walkup of H at x.
 195    node_walkup H x
 196    face_walkup H x
 197    double_edge_walkup H x y
 198    double_node_walkup H x y
 199    double_face_walkup H x y
 200
 201    *** more on orbits
 202
 203    power_list f x = \i. (f POWER i) x
 204    inj_orbit f x n ; the power_list of f x is an inj list (p,n)
 205
 206    order_permutation ; the order of a permutation of finite order.
 207
 208    *** merge
 209
 210    is_edge_merge H x.
 211    is_node_merge
 212    is_face_merge
 213    is_edge_split
 214    is_node_split
 215    is_face_split
 216
 217    is_splitting_component H x ;  n x and e^{-1} x are in the same comb component of (edge_walkup H x)
 218    is_Moebius_contour H p k ; (p,k) is an (injective) Moebius contour
 219
 220    shift_path p i ; \j. p (j + i)
 221
 222    *** complements
 223
 224    ind H x n ;
 225    mirror H x k n ;
 226    complement H x n  =mirror H x n n ; implements complementary loop of  face contour
 227
 228    *** misc
 229
 230    res (f:A->A) s ; restriction of function f to s, extension by identity.
 231
 232    planar_ind H ; planar index iota
 233
 234    iso H H' ; isomorphism of hypermap
 235
 236    *** cyclic hypermap
 237
 238    cyclic_hypermap ;  darts two sets of k, cyc_emap, cyc_nmap, cyc_fmap.
 239
 240    cyc_emap
 241    cyc_nmap
 242    cyc_fmap  face map on cyclic hypermap
 243
 244
 245    *** quotients
 246
 247    is_node_going H L x y ;  n^{-1} steps from dart x to y in loop L
 248    atom H L x = the "atom" [ .... x;n^{-1} x ....] of x in loop L
 249    is_normal H NF ; NF is a normal family of loops.
 250    quotient_darts H NF ; set of atoms from loops in NF.
 251    support_darts NF ; darts visiting NF
 252    fmap ; face map on atoms
 253    emap ; edge map on atoms
 254    nmap ;  node map on atoms
 255    quotient H NF ; quotient hypermap by a normal family NF.
 256    cycle H L ; set of atoms of L
 257    support_node H NF a ; set of darts of H at the node containing the atom a
 258
 259    choice H NF x ; the atom containing x in the normal family.
 260    head H NF x; head of  atom containing dart x.
 261    tail ; tail of a atom containing dart x
 262
 263
 264    face_loop H x ;  returns the loop on the face of x.
 265    face_collection H ; the set of face loops.
 266
 267    canon_loop H NF ;  this says that every atom in NF has size 1.
 268    canon H NF ; the set of loops that are canonical
 269    canon_darts ; the set of darts of loops that are canonical
 270
 271    canon_flag H NF ; this is not quite the way it is presented in flypaper.
 272    flag H NF L x ;
 273
 274    *** m,p,q,x,y,z:
 275
 276    minside H L x ; specification m st.  next^i x = f^i x.
 277    mAdd H L x ; specification p st.  f^{p+1} in support of NF.
 278    mRoute H L x ; specification q st ...
 279
 280    dart_inside H NF L x.   { f^i x | 1<= i <= m}
 281    heading H NF L x ; I think this is the dart y = f^{m+1} x.
 282    attach H NF L x ; I think this is the dart z = f^{p+1} y.
 283
 284    *** restricted hypermaps
 285
 286    is_restricted H
 287
 288    is_split_condition H NF L x ; long list of hypotheses; needed to split a loop into two
 289
 290    is_marked H NF L x; defines marked hypermap
 291
 292    *** transform of hypermap
 293
 294    genex H NF L x;   glues "attach" dart to "heading" dart
 295    tpx H NF L x;  I think this is the size of the new face?
 296    geney  NF L x; glues "heading" dart to "attach" dart
 297    tpy H NF L x; again size of new face?
 298    dnax H NF L x ; new loop X
 299    dnay H NF L x = new loop Y
 300
 301    genesis H NF L x = new set of loops, deleting L, adding two new loops.
 302
 303 *)