OAI/AlgebraicGeometry/CharacterVarieties/Cutting/BoundaryEnumeration.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

Based boundary enumeration and fresh-facet labels of the refined diagram.

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

  1. lemma OAI.IntegralCharacterVarieties.BasedCycleEnumeration.pow_mem line 17
  2. def OAI.IntegralCharacterVarieties.BasedCycleEnumeration.entry line 23
  3. lemma OAI.IntegralCharacterVarieties.BasedCycleEnumeration.entry_mem line 25
  4. lemma OAI.IntegralCharacterVarieties.BasedCycleEnumeration.entry_injective line 28
  5. lemma OAI.IntegralCharacterVarieties.BasedCycleEnumeration.entry_surjective line 34
  6. lemma OAI.IntegralCharacterVarieties.BasedCycleEnumeration.entry_next line 38
  7. lemma OAI.IntegralCharacterVarieties.BasedCycleEnumeration.enumeration_bijective line 47
  8. def OAI.IntegralCharacterVarieties.BasedCycleEnumeration.enumeration line 62
  9. lemma OAI.IntegralCharacterVarieties.BasedCycleEnumeration.enumeration_apply line 65
  10. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.graftCircleBase line 74
  11. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.graftCircleBase_mem line 79
  12. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.graftCircleEntry line 88
  13. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.graftBoundaryEnumeration line 95

    Source documentation

    The entire actual graft boundary, based at the original old occurrence on EVERY old circle, and at literal mirror/strip occurrences on new circles. Unlike fromPorts, this equivalence retains the old marking and circle labels.

    noncomputable def graftBoundaryEnumeration :
    ((c : D.GraftCircleLabel q B) × Fin (D.graftCircle q B c).card) ≃
      Side (base D.ports q B).Seam (base D.ports q B).seamArity :=
…
  14. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.graftBoundaryEnumeration_apply line 101
  15. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.graftBoundaryEnumeration_next line 104
  16. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.graftBoundaryEnumeration_zero line 111
  17. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.extendedBoundaryCount line 121
  18. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.extendedBoundaryLength line 122
  19. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.extendedBoundarySide line 126
  20. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.extendFacets line 144

    Source documentation

    Add the named fresh facet fibres before their boundary grafting. No old surface, orientation, side, rank or boundary ordering is modified.

    def extendFacets (newRank : G → ℕ) : Diagram (F ⊕ G) S V arity where
…

    Mentions: OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram

  21. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.extendFacets_boundarySet line 165
  22. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.extendFacets_maximal_no_child_parent line 168
  23. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedPreDiagram line 181
  24. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedPreDiagram_rank line 183
  25. abbrev OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.RefinedCircleLabel line 186
  26. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedCircle line 187
  27. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedPreDiagram_no_child line 189
  28. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedBoundaryEnumeration line 198

    Source documentation

    Actual marked inverse-band boundary enumeration. Short-root injection is proved from the atomic row/column topology; exclusion of principal children is derived from the author's proper-seam and maximal-rank hypotheses. No cyclic coverage, unique-strip, or fresh-parent-germ hypothesis is imposed.

    noncomputable def refinedBoundaryEnumeration (hproper : D.Proper)
    (hmax : ∀ f,D.rank f≤D.rank (D.ports.facet ⟨q,none⟩)) :
    ((c : D.RefinedCircleLabel q d) × Fin (D.refinedCircle q d c).card) ≃
      Side (base (D.refinedPreDiagram q d).ports q (D.ports.refinedBandForSeam q d)).Seam
        (base (D.refinedPreDiagram q d).ports q (D.ports.refinedBandForSeam q d)).seamArity := by
…
  29. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.bandEmbedding_color line 212
  30. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.refinedFreshEquiv line 222
  31. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.refinedFresh_original_color line 232
  32. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.extendedBoundaryIndex line 256
  33. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedCircleLabelEquiv line 269
  34. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedMarkedCount line 273
  35. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedMarkedLabel line 275
  36. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedMarkedLength line 280
  37. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedMarkedPositive line 283
  38. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedMarkedSide line 287