OAI/AlgebraicGeometry/CharacterVarieties/Cutting/StripForest.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

Finite trails of secondary corners in a realized band.

This formalizes the band reconstruction for filtered surface local systems in Integral points on character varieties of curves.

  1. structure OAI.IntegralCharacterVarieties.OccurrenceIncidence.LayeredTrail line 18

    Source documentation

    The child-seam graph of a half-band: internal seams have distinct ends and strictly increasing layer. This will be constructed from the literal whole- port gallery below, not requested as a lower-diagram hypothesis.

    structure LayeredTrail (N E : Type) where
…
  2. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.LayeredTrail.root line 28
  3. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.LayeredTrail.run line 36
  4. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.LayeredTrail.root_of_source line 46
  5. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.LayeredTrail.root_of_edge line 48
  6. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.LayeredTrail.run_of_sink line 52
  7. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.LayeredTrail.run_of_edge line 54
  8. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.LayeredTrail.root_external line 59
  9. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.LayeredTrail.mem_run_self line 73
  10. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.LayeredTrail.root_eq_of_mem_run line 77
  11. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.LayeredTrail.mem_run_root line 95

    Source documentation

    Every actual corner node belongs to the run of an exposed end.

    lemma mem_run_root (x : N) : x∈T.run (T.root x) := by
…
  12. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.LayeredTrail.external_run_cover line 125
  13. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.LayeredTrail.external_run_unique line 128
  14. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.LayeredTrail.run_level line 133
  15. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.LayeredTrail.run_nodup line 151
  16. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.LayeredTrail.reverse line 176

    Source documentation

    Both endpoints of each literal strip run are exposed.

    def reverse : LayeredTrail N E where
…

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.LayeredTrail

  17. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.LayeredTrail.tip line 183
  18. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.LayeredTrail.tip_external line 185
  19. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.LayeredTrail.tip_of_sink line 186
  20. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.LayeredTrail.tip_of_edge line 187
  21. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.LayeredTrail.tip_mem_run line 189
  22. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.LayeredTrail.tip_eq_of_mem_run line 205
  23. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.LayeredTrail.tip_root line 222
  24. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.LayeredTrail.root_tip line 223
  25. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.LayeredTrail.endsEquiv line 227

    Source documentation

    The open-end matching is produced, bijective, and retains every corner of every path. There are no concealed circular lower strips.

    noncomputable def endsEquiv : {x : N // ¬∃ e,T.target e=x} ≃ {x : N // ¬∃ e,T.source e=x} where
…
  26. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Kind.SecondaryNode line 240

    Source documentation

    One oriented SECONDARY corner of an actual allowed vertex. Removing the principal parent corner is essential: this is the graph of the lower strips.

    def SecondaryNode (k : Kind) :=
…

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Kind

  27. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Kind.inputNode line 244
  28. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Kind.outputNode line 249
  29. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Kind.inputNode_injective line 263
  30. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Kind.outputNode_injective line 267
  31. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Kind.node_not_output line 274
  32. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Kind.node_mate_not_input line 283
  33. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.StripNode line 308
  34. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.StripEdge line 309
  35. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.stripSource line 311
  36. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.stripTarget line 314
  37. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.stripSource_injective line 319
  38. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.stripTarget_injective line 329
  39. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.stripForest line 342

    Source documentation

    Produced from all and only the actual internally sewn child-port occurrences. In particular no transverse branch is treated as internal.

    noncomputable def stripForest : LayeredTrail B.StripNode B.StripEdge where
…

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.LayeredTrail

  40. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.stripColor line 349
  41. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.stripColor_edge line 351
  42. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.stripColor_root line 358
  43. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.strip_runs_cover line 370

    Source documentation

    Every local lower corner is on one and only one actual finite no-repeat strip run, with its original label constant along the entire run.

    theorem strip_runs_cover (x : B.StripNode) :
    ∃ s,(¬∃ e,B.stripTarget e=s) ∧ x∈B.stripForest.run s ∧
      (B.stripForest.run s).Nodup ∧ B.stripColor s=B.stripColor x :=
…
  44. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Kind.node_at_input line 380
  45. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Kind.node_at_output line 389
  46. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.input_predecessor line 409
  47. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.output_successor line 414
  48. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.root_exposed line 421

    Source documentation

    An incoming strip end is either at the first short end or on an actual transverse port. It cannot terminate invisibly inside a running seam.

    lemma root_exposed (x : B.StripNode) (he : ¬∃ e,B.stripTarget e=x) :
    x.2.val.1≠(B.kind x.1).output ∧
      (x.2.val.1≠(B.kind x.1).input ∨ x.1=0) := by
…
  49. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.tip_exposed line 436

    Source documentation

    The outgoing end of a strip is similarly at the final short end or on a transverse port, including every split and merge branch.

    lemma tip_exposed (x : B.StripNode) (he : ¬∃ e,B.stripSource e=x) :
    ((B.kind x.1).table.mate x.2.val).1≠(B.kind x.1).input ∧
      (((B.kind x.1).table.mate x.2.val).1≠(B.kind x.1).output ∨ x.1=Fin.last B.length) := by
…
  50. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.inputStrip line 452
  51. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.outputStrip line 454
  52. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.inputStrip_external line 456
  53. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.outputStrip_external line 461
  54. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.inputStrip_color line 466
  55. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.outputStrip_color line 471
  56. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.no_short_to_short line 481

    Source documentation

    Run colors rather than rank sums rule out a strip joining the two short ends. This is false after forgetting occurrence labels, so proved first on the named band, before attachment to possibly repeated old facets.

    lemma no_short_to_short (h : List.Disjoint a b) (c) (d) :
    B.stripForest.root (B.outputStrip d)≠B.inputStrip c := by
…
  57. lemma OAI.IntegralCharacterVarieties.TwoFlagBand.RankShape.atomic_short_disjoint line 493
  58. lemma OAI.IntegralCharacterVarieties.TwoFlagBand.RankShape.atomic_no_short_to_short line 499