OAI/AlgebraicGeometry/CharacterVarieties/Cutting/GraftValues.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Transport values on the old and inserted sides of an inverse-band graft.

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

  1. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.graftLabelArity line 25
  2. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.graftLabelArity_old line 26
  3. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.graftLabelArity_short line 28
  4. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.graft_old_color line 34
  5. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.graft_short_color line 50
  6. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.graftSideEquiv line 67

    Source documentation

    Sides have complete positive-port coordinates. The arity is the ACTUAL arity of that port, not merely a count inferred from endpoint names.

    def graftSideEquiv :
    ((z : S ⊕ (I ⊕ Bool)) × Option (Fin (graftLabelArity A P d q hi hp hm z))) ≃
      Side (W).Seam (W).seamArity :=
…

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.graftLabelArity, OAI.IntegralCharacterVarieties.OccurrenceIncidence.Side

  7. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.FacetUnit line 88
  8. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.graftLabelValues line 90
  9. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.graftSideValues line 115
  10. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.graftSideValues_coord line 122
  11. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.graftSideValues_internal line 150
  12. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.rebaseUnit_cast_facet line 155
  13. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.graftSideValues_old line 161
  14. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.graftSideValues_short line 182
  15. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.bandValues line 216
  16. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.mirrorValue line 221
  17. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.originalValue line 224
  18. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.mirrorValue_last line 228
  19. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.originalValue_zero line 232
  20. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.mirrorValue_castSucc line 236
  21. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.originalValue_succ line 247
  22. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.mirrorValues_word line 260

    Source documentation

    The actual reflected principal circle has precisely the inverse-band inner word, with the mirror orientation (not the unreflected gallery order).

    lemma mirrorValues_word :
    (List.ofFn (fun i : Fin (B.length+1) => mirrorValue A q B rank old short i.rev)).reverse.prod=
      short true none := by
…

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.mirrorValue

  23. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.originalValues_identity line 271
  24. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.graftSideValues_short_identity line 297
  25. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.doubledSideEquiv line 317
  26. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.oldEmbedding_coord line 325
  27. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.bandValues_strip line 343

    Source documentation

    BOTH strips inserted after an old child have identity transports on every literal side, including their short-end child occurrences. This excludes only the two principal short parents, proved disjoint from the actual strip circuit.

    lemma bandValues_strip (hshort : ∀ b i,short b (some i)=1)
    (r : B.StripRoot) (z : Side B.doubleWiring.Seam B.doubleWiring.seamArity)
    (hz : z∈B.stripCycle r.val) :
    bandValues A q B rank old short (bandEmbedding A q B z)=1 := by
…

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.Side, OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.bandValues, OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.bandEmbedding

  28. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.oldEmbedding_color line 389
  29. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.next_pow_color line 397
  30. def OAI.IntegralCharacterVarieties.CutCircleIndex.facet line 406
  31. lemma OAI.IntegralCharacterVarieties.CutCircleIndex.enumeration_facet line 410