OAI/AlgebraicGeometry/CharacterVarieties/Cutting/MarkedDiagram.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The marked inverse-band diagram and its facet colours.

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

  1. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedCircleBase_color line 17
  2. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedMarkedBase_color line 35
  3. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedMarkedSide_apply line 43
  4. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedMarkedSide_color line 50
  5. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedMarkedSide_next line 70
  6. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedMarkedDiagram line 83

    Source documentation

    The marked actual inverse-band diagram, retaining the order and starting occurrence of every old boundary circle. Its mirror boundary is appended at the selected parent; every fresh strip is precisely one genus-zero disk. Exhaustion and incidence come from the literal graft successor, not an arbitrary template.

    noncomputable def refinedMarkedDiagram := ({
…
  7. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedMarkedDiagram_count_old line 95
  8. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedMarkedDiagram_count_fresh line 98
  9. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedMarkedDiagram_genus_fresh line 100
  10. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedMarkedDiagram_genus_selected line 102
  11. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedMarkedDiagram_rank_inl line 106
  12. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedMarkedDiagram_rank_fresh_lt line 108